diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml index 470a941ff0..b42140080c 100644 --- a/src/incremental/compareCIL.ml +++ b/src/incremental/compareCIL.ml @@ -16,49 +16,61 @@ type changed_global = { diff: nodes_diff option } +module VarinfoSet = Set.Make(CilType.Varinfo) + type change_info = { mutable changed: changed_global list; mutable unchanged: global list; mutable removed: global list; - mutable added: global list + mutable added: global list; + mutable force_reanalyze: VarinfoSet.t; + (** Set of functions that are to be force-reanalyzed. + These functions are additionally included in the [changed] field, among the other changed globals. *) } let empty_change_info () : change_info = - {added = []; removed = []; changed = []; unchanged = []} + {added = []; removed = []; changed = []; unchanged = []; force_reanalyze = VarinfoSet.empty} + +type change_status = Unchanged | Changed | ForceReanalyze of Cil.fundec + +(** Given a boolean that indicates whether the code object is identical to the previous version, returns the corresponding [change_status]*) +let unchanged_to_change_status = function + | true -> Unchanged + | false -> Changed (* If some CFGs of the two functions to be compared are provided, a fine-grained CFG comparison is done that also determines which * nodes of the function changed. If on the other hand no CFGs are provided, the "old" AST comparison on the CIL.file is * used for functions. Then no information is collected regarding which parts/nodes of the function changed. *) -let eqF (a: Cil.fundec) (b: Cil.fundec) (cfgs : (cfg * cfg) option) = +let eqF (old: Cil.fundec) (current: Cil.fundec) (cfgs : (cfg * cfg) option) = let unchangedHeader = try - eq_varinfo a.svar b.svar && - List.for_all2 eq_varinfo a.sformals b.sformals + eq_varinfo old.svar current.svar && + List.for_all2 eq_varinfo old.sformals current.sformals with Invalid_argument _ -> false in - let identical, diffOpt = - if List.mem a.svar.vname (GobConfig.get_string_list "incremental.force-reanalyze.funs") then - false, None + let change_status, diffOpt = + if List.mem current.svar.vname (GobConfig.get_string_list "incremental.force-reanalyze.funs") then + ForceReanalyze current, None else try - let sameDef = unchangedHeader && List.for_all2 eq_varinfo a.slocals b.slocals in + let sameDef = unchangedHeader && List.for_all2 eq_varinfo old.slocals current.slocals in match cfgs with - | None -> sameDef && eq_block (a.sbody, a) (b.sbody, b), None + | None -> unchanged_to_change_status (sameDef && eq_block (old.sbody, old) (current.sbody, current)), None | Some (cfgOld, cfgNew) -> let module CfgOld : MyCFG.CfgForward = struct let next = cfgOld end in let module CfgNew : MyCFG.CfgForward = struct let next = cfgNew end in - let matches, diffNodes1, diffNodes2 = compareFun (module CfgOld) (module CfgNew) a b in - if not sameDef then (false, None) - else if diffNodes1 = [] && diffNodes2 = [] then (true, None) - else (false, Some {unchangedNodes = matches; primObsoleteNodes = diffNodes1; primNewNodes = diffNodes2}) + let matches, diffNodes1, diffNodes2 = compareFun (module CfgOld) (module CfgNew) old current in + if not sameDef then (Changed, None) + else if diffNodes1 = [] && diffNodes2 = [] then (Changed, None) + else (Changed, Some {unchangedNodes = matches; primObsoleteNodes = diffNodes1; primNewNodes = diffNodes2}) with Invalid_argument _ -> (* The combine failed because the lists have differend length *) - false, None in - identical, unchangedHeader, diffOpt + Changed, None in + change_status, unchangedHeader, diffOpt -let eq_glob (a: global) (b: global) (cfgs : (cfg * cfg) option) = match a, b with +let eq_glob (old: global) (current: global) (cfgs : (cfg * cfg) option) = match old, current with | GFun (f,_), GFun (g,_) -> eqF f g cfgs - | GVar (x, init_x, _), GVar (y, init_y, _) -> eq_varinfo x y, false, None (* ignore the init_info - a changed init of a global will lead to a different start state *) - | GVarDecl (x, _), GVarDecl (y, _) -> eq_varinfo x y, false, None - | _ -> ignore @@ Pretty.printf "Not comparable: %a and %a\n" Cil.d_global a Cil.d_global b; false, false, None + | GVar (x, init_x, _), GVar (y, init_y, _) -> unchanged_to_change_status (eq_varinfo x y), false, None (* ignore the init_info - a changed init of a global will lead to a different start state *) + | GVarDecl (x, _), GVarDecl (y, _) -> unchanged_to_change_status (eq_varinfo x y), false, None + | _ -> ignore @@ Pretty.printf "Not comparable: %a and %a\n" Cil.d_global old Cil.d_global current; Changed, false, None let compareCilFiles (oldAST: file) (newAST: file) = let cfgs = if GobConfig.get_string "incremental.compare" = "cfg" @@ -79,10 +91,17 @@ let compareCilFiles (oldAST: file) (newAST: file) = (try let old_global = GlobalMap.find ident map in (* Do a (recursive) equal comparison ignoring location information *) - let identical, unchangedHeader, diff = eq_glob old_global global cfgs in - if identical - then changes.unchanged <- global :: changes.unchanged - else changes.changed <- {current = global; old = old_global; unchangedHeader; diff} :: changes.changed + let change_status, unchangedHeader, diff = eq_glob old_global global cfgs in + let append_to_changed () = + changes.changed <- {current = global; old = old_global; unchangedHeader; diff} :: changes.changed + in + match change_status with + | Changed -> append_to_changed () + | Unchanged -> changes.unchanged <- global :: changes.unchanged + | ForceReanalyze f -> + changes.force_reanalyze <- VarinfoSet.add f.svar changes.force_reanalyze; + append_to_changed (); + with Not_found -> ()) with NoGlobalIdentifier _ -> () (* Global was no variable or function, it does not belong into the map *) in let checkExists map global = diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 5011333a44..f65891539f 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -627,22 +627,39 @@ module WP = ) in + let reluctant = GobConfig.get_bool "incremental.reluctant.on" in + let reanalyze_entry f = + (* destabilize the entry points of a changed function when reluctant is off, + or the function is to be force-reanalyzed *) + (not reluctant) || CompareCIL.VarinfoSet.mem f.svar S.increment.changes.force_reanalyze + in let obsolete_ret = HM.create 103 in let obsolete_entry = HM.create 103 in let obsolete_prim = HM.create 103 in + + (* When reluctant is on: + Only add function entry nodes to obsolete_entry if they are in force-reanalyze *) List.iter (fun f -> - mark_node obsolete_entry f (FunctionEntry f); - mark_node obsolete_ret f (Function f); + if reanalyze_entry f then + (* collect function entry for eager destabilization *) + mark_node obsolete_entry f (FunctionEntry f) + else + (* collect function return for reluctant analysis *) + mark_node obsolete_ret f (Function f) ) changed_funs; - List.iter (fun (f, pn, _) -> - List.iter (fun n -> - mark_node obsolete_prim f n - ) pn; - mark_node obsolete_ret f (Function f); - ) part_changed_funs; + (* Unknowns from partially changed functions need only to be collected for eager destabilization when reluctant is off *) + (* We utilize that force-reanalyzed functions are always considered as completely changed (and not partially changed) *) + if not reluctant then ( + List.iter (fun (f, pn, _) -> + List.iter (fun n -> + mark_node obsolete_prim f n + ) pn; + mark_node obsolete_ret f (Function f); + ) part_changed_funs; + ); let old_ret = HM.create 103 in - if GobConfig.get_bool "incremental.reluctant.on" then ( + if reluctant then ( (* save entries of changed functions in rho for the comparison whether the result has changed after a function specific solve *) HM.iter (fun k v -> if HM.mem rho k then ( @@ -651,20 +668,19 @@ module WP = HM.replace old_ret k (old_rho, old_infl) ) ) obsolete_ret; - ) else ( - (* If reluctant destabilization is turned off we need to destabilize all nodes in completely changed functions - and the primary obsolete nodes of partly changed functions *) - print_endline "Destabilizing changed functions and primary old nodes ..."; - HM.iter (fun k _ -> - if HM.mem stable k then - destabilize k - ) obsolete_entry; - HM.iter (fun k _ -> - if HM.mem stable k then - destabilize k - ) obsolete_prim; ); + if not (HM.is_empty obsolete_entry) || not (HM.is_empty obsolete_prim) then + print_endline "Destabilizing changed functions and primary old nodes ..."; + HM.iter (fun k _ -> + if HM.mem stable k then + destabilize k + ) obsolete_entry; + HM.iter (fun k _ -> + if HM.mem stable k then + destabilize k + ) obsolete_prim; + (* We remove all unknowns for program points in changed or removed functions from rho, stable, infl and wpoint *) let marked_for_deletion = HM.create 103 in @@ -672,14 +688,14 @@ module WP = (* not the same as in CFG, but compares equal because of sid *) Node.Statement ({Cil.dummyStmt with sid = CfgTools.get_pseudo_return_id f}) in - let add_nodes_of_fun (functions: fundec list) withEntry = + let add_nodes_of_fun (functions: fundec list) (withEntry: fundec -> bool) = let add_stmts (f: fundec) = List.iter (fun s -> mark_node marked_for_deletion f (Statement s) ) f.sallstmts in List.iter (fun f -> - if withEntry then + if withEntry f then mark_node marked_for_deletion f (FunctionEntry f); mark_node marked_for_deletion f (Function f); add_stmts f; @@ -687,8 +703,8 @@ module WP = ) functions; in - add_nodes_of_fun changed_funs (not (GobConfig.get_bool "incremental.reluctant.on")); - add_nodes_of_fun removed_funs true; + add_nodes_of_fun changed_funs reanalyze_entry; + add_nodes_of_fun removed_funs (fun _ -> true); (* it is necessary to remove all unknowns for changed pseudo-returns because they have static ids *) let add_pseudo_return f un = let pseudo = dummy_pseudo_return_node f in @@ -798,7 +814,7 @@ module WP = (* TODO: reluctant doesn't call destabilize on removed functions or old copies of modified functions (e.g. after removing write), so those globals don't get restarted *) - if GobConfig.get_bool "incremental.reluctant.on" then ( + if reluctant then ( (* solve on the return node of changed functions. Only destabilize the function's return node if the analysis result changed *) print_endline "Separately solving changed functions..."; let op = if GobConfig.get_string "incremental.reluctant.compare" = "leq" then S.Dom.leq else S.Dom.equal in diff --git a/tests/incremental/01-force-reanalyze/01-int-reluctant.c b/tests/incremental/01-force-reanalyze/01-int-reluctant.c new file mode 100644 index 0000000000..38187f1c06 --- /dev/null +++ b/tests/incremental/01-force-reanalyze/01-int-reluctant.c @@ -0,0 +1,17 @@ +#include + +int f(int in){ + while(in < 17) { + in++; + } + assert(in == 17); //UNKNOWN + return in; +} + +int main() { + int a = 0; + assert(a); // FAIL! + a = f(a); + assert(a == 17); //UNKNOWN + return 0; +} diff --git a/tests/incremental/01-force-reanalyze/01-int-reluctant.json b/tests/incremental/01-force-reanalyze/01-int-reluctant.json new file mode 100644 index 0000000000..d58c2254bc --- /dev/null +++ b/tests/incremental/01-force-reanalyze/01-int-reluctant.json @@ -0,0 +1,21 @@ +{ + "annotation" : { + "int" : { + "enabled" : true + } + }, + "ana" : { + "int" : { + "refinement" : "fixpoint" + } + }, + "incremental" : { + "force-reanalyze" : { + "funs": ["f"] + }, + "reluctant" : { + "on": true + }, + "verify": false + } +} diff --git a/tests/incremental/01-force-reanalyze/01-int-reluctant.patch b/tests/incremental/01-force-reanalyze/01-int-reluctant.patch new file mode 100644 index 0000000000..0cf9fee4ba --- /dev/null +++ b/tests/incremental/01-force-reanalyze/01-int-reluctant.patch @@ -0,0 +1,37 @@ +diff --git tests/incremental/01-force-reanalyze/01-int-reluctant.c tests/incremental/01-force-reanalyze/01-int-reluctant.c +index 38187f1c0..6126fe8cf 100644 +--- tests/incremental/01-force-reanalyze/01-int-reluctant.c ++++ tests/incremental/01-force-reanalyze/01-int-reluctant.c +@@ -4,7 +4,7 @@ int f(int in){ + while(in < 17) { + in++; + } +- assert(in == 17); //UNKNOWN ++ assert(in == 17); + return in; + } + +@@ -12,6 +12,6 @@ int main() { + int a = 0; + assert(a); // FAIL! + a = f(a); +- assert(a == 17); //UNKNOWN ++ assert(a == 17); + return 0; + } +diff --git tests/incremental/01-force-reanalyze/01-int-reluctant.json tests/incremental/01-force-reanalyze/01-int-reluctant.json +index d58c2254b..8834d182d 100644 +--- tests/incremental/01-force-reanalyze/01-int-reluctant.json ++++ tests/incremental/01-force-reanalyze/01-int-reluctant.json +@@ -2,6 +2,11 @@ + "annotation" : { + "int" : { + "enabled" : true ++ }, ++ "goblint_precision": { ++ "interval": [ ++ "f" ++ ] + } + }, + "ana" : { diff --git a/tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c b/tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c new file mode 100644 index 0000000000..38187f1c06 --- /dev/null +++ b/tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c @@ -0,0 +1,17 @@ +#include + +int f(int in){ + while(in < 17) { + in++; + } + assert(in == 17); //UNKNOWN + return in; +} + +int main() { + int a = 0; + assert(a); // FAIL! + a = f(a); + assert(a == 17); //UNKNOWN + return 0; +} diff --git a/tests/incremental/03-precision-annotation/02-reluctant-int-annotation.json b/tests/incremental/03-precision-annotation/02-reluctant-int-annotation.json new file mode 100644 index 0000000000..60d4692176 --- /dev/null +++ b/tests/incremental/03-precision-annotation/02-reluctant-int-annotation.json @@ -0,0 +1,18 @@ +{ + "annotation": { + "int": { + "enabled": true + } + }, + "ana": { + "int": { + "refinement": "fixpoint" + } + }, + "incremental": { + "reluctant": { + "on": true + }, + "verify": false + } +} diff --git a/tests/incremental/03-precision-annotation/02-reluctant-int-annotation.patch b/tests/incremental/03-precision-annotation/02-reluctant-int-annotation.patch new file mode 100644 index 0000000000..715a2530b9 --- /dev/null +++ b/tests/incremental/03-precision-annotation/02-reluctant-int-annotation.patch @@ -0,0 +1,25 @@ +diff --git tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c +index 38187f1c0..698e45b62 100644 +--- tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c ++++ tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c +@@ -1,10 +1,11 @@ + #include + ++int f(int in) __attribute__ ((goblint_precision("def_exc", "interval"))); + int f(int in){ + while(in < 17) { + in++; + } +- assert(in == 17); //UNKNOWN ++ assert(in == 17); + return in; + } + +@@ -12,6 +13,6 @@ int main() { + int a = 0; + assert(a); // FAIL! + a = f(a); +- assert(a == 17); //UNKNOWN ++ assert(a == 17); + return 0; + } diff --git a/tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.c b/tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.c new file mode 100644 index 0000000000..30391cdf61 --- /dev/null +++ b/tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.c @@ -0,0 +1,24 @@ +#include + +typedef int int_to_int_fun (int); + +int f(int in){ + while(in < 17) { + in++; + } + assert(in == 17); //UNKNOWN + return in; +} + +int_to_int_fun *get_fun(){ + return &f; +} + +int main() { + int_to_int_fun *fun = get_fun(); + int a = 0; + assert(a); // FAIL! + a = fun(a); + assert(a == 17); //UNKNOWN + return 0; +} diff --git a/tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.json b/tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.json new file mode 100644 index 0000000000..60d4692176 --- /dev/null +++ b/tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.json @@ -0,0 +1,18 @@ +{ + "annotation": { + "int": { + "enabled": true + } + }, + "ana": { + "int": { + "refinement": "fixpoint" + } + }, + "incremental": { + "reluctant": { + "on": true + }, + "verify": false + } +} diff --git a/tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.patch b/tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.patch new file mode 100644 index 0000000000..224fd6554e --- /dev/null +++ b/tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.patch @@ -0,0 +1,26 @@ +diff --git tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.c tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.c +index 30391cdf6..4d2620e84 100644 +--- tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.c ++++ tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.c +@@ -2,11 +2,12 @@ + + typedef int int_to_int_fun (int); + ++int f(int in) __attribute__ ((goblint_precision("def_exc", "interval"))); + int f(int in){ + while(in < 17) { + in++; + } +- assert(in == 17); //UNKNOWN ++ assert(in == 17); + return in; + } + +@@ -19,6 +20,6 @@ int main() { + int a = 0; + assert(a); // FAIL! + a = fun(a); +- assert(a == 17); //UNKNOWN ++ assert(a == 17); + return 0; + }