diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml index 8b55608caa..c0300f9e59 100644 --- a/src/incremental/compareAST.ml +++ b/src/incremental/compareAST.ml @@ -1,11 +1,6 @@ open GoblintCil open CilMaps -(* global_type and global_t are implicitly used by GlobalMap to keep GVarDecl apart from GVar and GFun, so do not remove! *) -type global_type = Fun | Decl | Var - -and global_identifier = {name: string ; global_t: global_type} [@@deriving ord] - module StringMap = Map.Make(String) type method_rename_assumption = {original_method_name: string; new_method_name: string; parameter_renames: string StringMap.t} @@ -23,10 +18,8 @@ let rename_mapping_aware_name_comparison (name1: string) (name2: string) (rename match existingAssumption with | Some now -> - (*Printf.printf "Assumption is: %s -> %s\n" original now;*) now = name2 | None -> - (*Printf.printf "No assumption when %s, %s, %b\n" name1 name2 (name1 = name2);*) name1 = name2 (*Var names differ, but there is no assumption, so this can't be good*) let rename_mapping_to_string (rename_mapping: rename_mapping) = @@ -39,18 +32,6 @@ let rename_mapping_to_string (rename_mapping: rename_mapping) = String.concat ", " in "(local=" ^ local_string ^ "; methods=[" ^ methods_string ^ "])" -let identifier_of_global glob = - match glob with - | GFun (fundec, l) -> {name = fundec.svar.vname; global_t = Fun} - | GVar (var, init, l) -> {name = var.vname; global_t = Var} - | GVarDecl (var, l) -> {name = var.vname; global_t = Decl} - | _ -> raise Not_found - -module GlobalMap = Map.Make(struct - type t = global_identifier [@@deriving ord] - end) - - (* hack: CIL generates new type names for anonymous types - we want to ignore these *) let compare_name (a: string) (b: string) = let anon_struct = "__anonstruct_" in @@ -170,7 +151,6 @@ and eq_attribute ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) (a: | Attr (name1, params1), Attr (name2, params2) -> name1 = name2 && GobList.equal (eq_attrparam ~rename_mapping ~acc ) params1 params2 and eq_varinfo (a: varinfo) (b: varinfo) ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) = - (*Printf.printf "Comp %s with %s\n" a.vname b.vname;*) let (_, method_rename_mappings) = rename_mapping in @@ -201,10 +181,7 @@ and eq_varinfo (a: varinfo) (b: varinfo) ~(acc: (typ * typ) list) ~(rename_mapp let typeCheck = eq_typ_acc a.vtype b.vtype ~rename_mapping:typ_rename_mapping ~acc in let attrCheck = GobList.equal (eq_attribute ~rename_mapping ~acc ) a.vattr b.vattr in - let result = isNamingOk && typeCheck && attrCheck && - a.vstorage = b.vstorage && a.vglob = b.vglob && a.vaddrof = b.vaddrof in - - result + isNamingOk && typeCheck && attrCheck && a.vstorage = b.vstorage && a.vglob = b.vglob && a.vaddrof = b.vaddrof (* Ignore the location, vid, vreferenced, vdescr, vdescrpure, vinline *) (* Accumulator is needed because of recursive types: we have to assume that two types we already encountered in a previous step of the recursion are equivalent *) diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml index 881c707a14..a96a65e004 100644 --- a/src/incremental/compareCIL.ml +++ b/src/incremental/compareCIL.ml @@ -4,20 +4,31 @@ open CilMaps include CompareAST include CompareCFG +module GlobalMap = Map.Make(String) + +type global_def = Var of varinfo | Fun of fundec +type global_col = {decls: varinfo option; def: global_def option} + +let name_of_global g = match g with + | GVar (v,_,_) -> v.vname + | GFun (f,_) -> f.svar.vname + | GVarDecl (v,_) -> v.vname + | _ -> failwith "global constructor not supported" + type nodes_diff = { unchangedNodes: (node * node) list; primObsoleteNodes: node list; (** primary obsolete nodes -> all obsolete nodes are reachable from these *) } type unchanged_global = { - old: global; - current: global + old: global_col; + current: global_col } (** For semantically unchanged globals, still keep old and current version of global for resetting current to old. *) type changed_global = { - old: global; - current: global; + old: global_col; + current: global_col; unchangedHeader: bool; diff: nodes_diff option } @@ -27,8 +38,8 @@ module VarinfoSet = Set.Make(CilType.Varinfo) type change_info = { mutable changed: changed_global list; mutable unchanged: unchanged_global list; - mutable removed: global list; - mutable added: global list; + mutable removed: global_col list; + mutable added: global_col list; mutable exclude_from_rel_destab: 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. *) @@ -104,98 +115,98 @@ let eqF (old: Cil.fundec) (current: Cil.fundec) (cfgs : (cfg * (cfg * cfg)) opti if diffNodes1 = [] then (Unchanged, None) else (Changed, Some {unchangedNodes = matches; primObsoleteNodes = diffNodes1}) -let eq_glob (old: global) (current: global) (cfgs : (cfg * (cfg * cfg)) option) (global_rename_mapping: method_rename_assumptions) = match old, current with - | GFun (f,_), GFun (g,_) -> eqF f g cfgs global_rename_mapping - | GVar (x, init_x, _), GVar (y, init_y, _) -> unchanged_to_change_status (eq_varinfo x y ~rename_mapping:(StringMap.empty, VarinfoMap.empty)), 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 ~rename_mapping:(StringMap.empty, VarinfoMap.empty)), None - | _ -> ignore @@ Pretty.printf "Not comparable: %a and %a\n" Cil.d_global old Cil.d_global current; Changed, None +let eq_glob (old: global_col) (current: global_col) (cfgs : (cfg * (cfg * cfg)) option) (global_rename_mapping: method_rename_assumptions) = + match old.def, current.def with + | Some (Var x), Some (Var y) -> unchanged_to_change_status (eq_varinfo x y ~rename_mapping:(StringMap.empty, VarinfoMap.empty)), None (* ignore the init_info - a changed init of a global will lead to a different start state *) + | Some (Fun f), Some (Fun g) -> eqF f g cfgs global_rename_mapping + | None, None -> (match old.decls, current.decls with + | Some x, Some y -> unchanged_to_change_status (eq_varinfo x y ~rename_mapping:(StringMap.empty, VarinfoMap.empty)), None + | _, _ -> failwith "should never collect any empty entries in GlobalMap") + | _, _ -> Changed, None (* it is considered to be changed (not added or removed) because a global collection only exists in the map + if there is at least one declaration or definition for this global *) let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) = let cfgs = if GobConfig.get_string "incremental.compare" = "cfg" then Some (CfgTools.getCFG oldAST |> fst, CfgTools.getCFG newAST) else None in - let generate_global_rename_mapping map global = + let addGlobal map global = try - let ident = identifier_of_global global in - let old_global = GlobalMap.find ident map in + let name, col = match global with + | GVar (v,_,_) -> v.vname, {decls = None; def = Some (Var v)} + | GFun (f,_) -> f.svar.vname, {decls = None; def = Some (Fun f)} + | GVarDecl (v,_) -> v.vname, {decls = Some v; def = None} + | _ -> raise Not_found in + let merge_d def1 def2 = match def1, def2 with + | Some d, None -> Some d + | None, Some d -> Some d + | None, None -> None + | _ -> failwith "there can only be one definition and one declaration per global" in + let merge_global_col entry = match entry with + | None -> Some col + | Some col' -> Some {decls = merge_d col.decls col'.decls; def = merge_d col.def col'.def} in + GlobalMap.update name merge_global_col map; + with + Not_found -> map + in - match old_global, global with - | GFun(f, _), GFun (g, _) -> - let renamed_params: string StringMap.t = if (List.length f.sformals) = (List.length g.sformals) then - let mappings = List.combine f.sformals g.sformals |> + (* Store a map from functionNames in the old file to the function definition*) + let oldMap = Cil.foldGlobals oldAST addGlobal GlobalMap.empty in + let newMap = Cil.foldGlobals newAST addGlobal GlobalMap.empty in + + let generate_global_rename_mapping name current_global = + try + let old_global = GlobalMap.find name oldMap in + match old_global.def, current_global.def with + | Some (Fun f1), Some (Fun f2) -> + let renamed_params: string StringMap.t = if (List.length f1.sformals) = (List.length f2.sformals) then + let mappings = List.combine f1.sformals f2.sformals |> List.filter (fun (original, now) -> not (original.vname = now.vname)) |> List.map (fun (original, now) -> (original.vname, now.vname)) |> List.to_seq in - StringMap.add_seq mappings StringMap.empty else StringMap.empty in - - if not (f.svar.vname = g.svar.vname) || (StringMap.cardinal renamed_params) > 0 then - Some (f.svar, {original_method_name=f.svar.vname; new_method_name=g.svar.vname; parameter_renames=renamed_params}) + if not (f1.svar.vname = f2.svar.vname) || (StringMap.cardinal renamed_params) > 0 then + Some (f1.svar, {original_method_name = f1.svar.vname; new_method_name = f2.svar.vname; parameter_renames = renamed_params}) else None | _, _ -> None with Not_found -> None in - let addGlobal map global = - try - let gid = identifier_of_global global in - let gid_to_string gid = match gid.global_t with - | Var -> "Var " ^ gid.name - | Decl -> "Decl " ^ gid.name - | Fun -> "Fun " ^ gid.name in - if GlobalMap.mem gid map then failwith ("Duplicate global identifier: " ^ gid_to_string gid) else GlobalMap.add gid global map - with - Not_found -> map - in + let global_rename_mapping: method_rename_assumptions = GlobalMap.fold (fun name global_col current_global_rename_mapping -> + match generate_global_rename_mapping name global_col with + | Some (funVar, rename_mapping) -> VarinfoMap.add funVar rename_mapping current_global_rename_mapping + | None -> current_global_rename_mapping + ) newMap VarinfoMap.empty in let changes = empty_change_info () in global_typ_acc := []; - let findChanges map global global_rename_mapping = + let findChanges map name current_global global_rename_mapping = try - let ident = identifier_of_global global in - let old_global = GlobalMap.find ident map in + let old_global = GlobalMap.find name map in (* Do a (recursive) equal comparison ignoring location information *) - let change_status, diff = eq old_global global cfgs global_rename_mapping in + let change_status, diff = eq old_global current_global cfgs global_rename_mapping in let append_to_changed ~unchangedHeader = - changes.changed <- {current = global; old = old_global; unchangedHeader; diff} :: changes.changed + changes.changed <- {current = current_global; old = old_global; unchangedHeader; diff} :: changes.changed in match change_status with | Changed -> append_to_changed ~unchangedHeader:true - | Unchanged -> changes.unchanged <- {current = global; old = old_global} :: changes.unchanged + | Unchanged -> changes.unchanged <- {current = current_global; old = old_global} :: changes.unchanged | ChangedFunHeader f | ForceReanalyze f -> changes.exclude_from_rel_destab <- VarinfoSet.add f.svar changes.exclude_from_rel_destab; append_to_changed ~unchangedHeader:false; - with Not_found -> () (* Global was no variable or function, it does not belong into the map *) - in - let checkExists map global = - match identifier_of_global global with - | name -> GlobalMap.mem name map - | exception Not_found -> true (* return true, so isn't considered a change *) - in - (* Store a map from functionNames in the old file to the function definition*) - let oldMap = Cil.foldGlobals oldAST addGlobal GlobalMap.empty in - let newMap = Cil.foldGlobals newAST addGlobal GlobalMap.empty in - - let global_rename_mapping: method_rename_assumptions = Cil.foldGlobals newAST (fun (current_global_rename_mapping: method_rename_assumption VarinfoMap.t) global -> - match generate_global_rename_mapping oldMap global with - | Some (funVar, rename_mapping) -> VarinfoMap.add funVar rename_mapping current_global_rename_mapping - | None -> current_global_rename_mapping - ) VarinfoMap.empty + with Not_found -> changes.removed <- current_global::changes.removed (* Global could not be found in old map -> added *) in (* For each function in the new file, check whether a function with the same name already existed in the old version, and whether it is the same function. *) - Cil.iterGlobals newAST - (fun glob -> findChanges oldMap glob global_rename_mapping); + GlobalMap.iter (fun name glob_col -> findChanges oldMap name glob_col global_rename_mapping) newMap; (* We check whether functions have been added or removed *) - Cil.iterGlobals newAST (fun glob -> if not (checkExists oldMap glob) then changes.added <- (glob::changes.added)); - Cil.iterGlobals oldAST (fun glob -> if not (checkExists newMap glob) then changes.removed <- (glob::changes.removed)); + GlobalMap.iter (fun name glob -> if not (GlobalMap.mem name newMap) then changes.removed <- (glob::changes.removed)) oldMap; changes (** Given an (optional) equality function between [Cil.global]s, an old and a new [Cil.file], this function computes a [change_info], diff --git a/src/incremental/updateCil.ml b/src/incremental/updateCil.ml index d7fe25f438..2f9628b4c1 100644 --- a/src/incremental/updateCil.ml +++ b/src/incremental/updateCil.ml @@ -52,11 +52,12 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change in let reset_globals (glob: unchanged_global) = try - match glob.current, glob.old with - | GFun (nw, _), GFun (old, _) -> reset_fun nw old - | GVar (nw, _, _), GVar (old, _, _) -> reset_var nw old - | GVarDecl (nw, _), GVarDecl (old, _) -> reset_var nw old - | _ -> () + match glob.current.def, glob.old.def with + | Some (Fun nw), Some (Fun old) -> reset_fun nw old + | Some (Var nw), Some (Var old) -> reset_var nw old + | _, _ -> match glob.current.decls, glob.old.decls with + | Some nw, Some old -> reset_var nw old + | _, _ -> () with Failure m -> () in let assign_same_id fallstmts (old_n, n) = match old_n, n with @@ -88,9 +89,16 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change List.iter (reset_changed_stmt (List.map snd d.unchangedNodes)) f.sallstmts; List.iter (assign_same_id f.sallstmts) d.unchangedNodes in + let update_var (v: varinfo) = + v.vid <- make_vid () + in let reset_changed_globals (changed: changed_global) = - match (changed.current, changed.old) with - | GFun (nw, _), GFun (old, _) -> reset_changed_fun nw old changed.unchangedHeader changed.diff + match (changed.current.def, changed.old.def) with + | Some (Fun nw), Some (Fun old) -> reset_changed_fun nw old changed.unchangedHeader changed.diff + | Some (Var nw), Some (Var old) -> update_var nw + | None, None -> (match (changed.current.decls, changed.old.decls) with + | Some nw, Some old -> update_var nw + | _ -> ()) | _ -> () in let update_fun (f: fundec) = @@ -99,16 +107,14 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change List.iter (fun f -> f.vid <- make_vid ()) f.sformals; List.iter (fun s -> s.sid <- make_sid ()) f.sallstmts; in - let update_var (v: varinfo) = - v.vid <- make_vid () - in - let update_globals (glob: global) = + let update_globals (glob: global_col) = try - match glob with - | GFun (nw, _) -> update_fun nw - | GVar (nw, _, _) -> update_var nw - | GVarDecl (nw, _) -> update_var nw - | _ -> () + match glob.def with + | Some (Fun nw) -> update_fun nw + | Some (Var nw) -> update_var nw + | _ -> match glob.decls with + | Some v1 -> update_var v1 + | _ -> () with Failure m -> () in List.iter reset_globals changes.unchanged; diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 0eccc5c679..05a0f3a7ce 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -472,21 +472,21 @@ module WP = destabilize_normal; let changed_funs = List.filter_map (function - | {old = GFun (f, _); diff = None; _} -> + | {old = {def = Some (Fun f); _}; diff = None; _} -> print_endline ("Completely changed function: " ^ f.svar.vname); Some f | _ -> None ) S.increment.changes.changed in let part_changed_funs = List.filter_map (function - | {old = GFun (f, _); diff = Some nd; _} -> + | {old = {def = Some (Fun f); _}; diff = Some nd; _} -> print_endline ("Partially changed function: " ^ f.svar.vname); Some (f, nd.primObsoleteNodes, nd.unchangedNodes) | _ -> None ) S.increment.changes.changed in let removed_funs = List.filter_map (function - | GFun (f, _) -> + | {def = Some (Fun f); _} -> print_endline ("Removed function: " ^ f.svar.vname); Some f | _ -> None diff --git a/src/util/server.ml b/src/util/server.ml index 580cbc9d84..885e2c0ebf 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -157,8 +157,8 @@ let reparse (s: t) = (* Only called when the file has not been reparsed, so we can skip the expensive CFG comparison. *) let virtual_changes file = - let eq (glob: Cil.global) _ _ _ = match glob with - | GFun (fdec, _) when CompareCIL.should_reanalyze fdec -> CompareCIL.ForceReanalyze fdec, None + let eq (glob: CompareCIL.global_col) _ _ _ = match glob.def with + | Some (Fun fdec) when CompareCIL.should_reanalyze fdec -> CompareCIL.ForceReanalyze fdec, None | _ -> Unchanged, None in CompareCIL.compareCilFiles ~eq file file