Incremental TD3: incrementalize analysis within functions

scripts/incremental.sh

@@ -53,7 +53,8 @@ trap finish EXIT
 
 outp=$out/$(basename $repo_path)
 
-rm -rf "$outp"
+rm -r "$outp"
+rm -r "incremental_data"
 function log {
   echo "$*" | tee -a $outp/incremental.log
 }
@@ -65,7 +66,7 @@ loc=$(git -C $repo_path diff --shortstat 4b825dc642cb6eb9a060e54bf8d69288fbee490
 git -C $repo_path checkout $start_commit
 i=1
 prev_commit=''
-echo -e "index\tcommit\tl_ins\tl_del\tl_max\ttime\tvars\tevals\tchanged\tadded\tremoved\tchanged_start\tnew_start" >> $outp/incremental_runtime.log
+echo -e "index\tcommit\tl_ins\tl_del\tl_max\ttime\ttime(internally)\tvars\tevals\tchanged\tadded\tremoved\tchanged_start\tnew_start" >> $outp/incremental_runtime.log
 while
   commit=$(git -C $repo_path rev-parse HEAD)
   if [ "$commit" = "$prev_commit" ]; then
@@ -96,6 +97,7 @@ while
   end=$(echo "scale=3; $(date +%s%3N) /1000" | bc)
   runtime=$(echo "$end-$start" | bc)
   log "  Goblint ran $runtime seconds"
+  internal_runtime=$(grep 'TOTAL' $outc/analyzer.log | tr -s ' ' | cut -d" " -f2 | cut -d"s" -f1)
   vars=$(grep 'vars = ' $outc/analyzer.log | cut -d" " -f3)
   evals=$(grep 'evals = ' $outc/analyzer.log | cut -d" " -f9)
   changed=$(grep 'change_info = { ' $outc/analyzer.log | cut -d" " -f9 | cut -d";" -f1)
@@ -120,7 +122,7 @@ while
   else
     l_max=$l_ins
   fi
-  echo -e "$i\t$commit\t$l_ins\t$l_del\t$l_max\t$runtime\t$vars\t$evals\t$changed\t$added\t$removed\t$changed_start\t$new_start" >> $outp/incremental_runtime.log
+  echo -e "$i\t$commit\t$l_ins\t$l_del\t$l_max\t$runtime\t$internal_runtime\t$vars\t$evals\t$changed\t$added\t$removed\t$changed_start\t$new_start" >> $outp/incremental_runtime.log
   log "  $(grep 'evals = ' $outc/analyzer.log)"
   log "  $(grep 'change_info = ' $outc/analyzer.log)"
   log "  Obsolete functions: $(grep 'Obsolete function' $outc/analyzer.log | wc -l)"

src/framework/analyses.ml

@@ -386,13 +386,13 @@ type analyzed_data = {
 type increment_data = {
   old_data: analyzed_data option;
   new_file: Cil.file;
-  changes: CompareAST.change_info
+  changes: CompareCIL.change_info
 }
 
 let empty_increment_data file = {
   old_data = None;
   new_file = file;
-  changes = CompareAST.empty_change_info ()
+  changes = CompareCIL.empty_change_info ()
 }
 
 (** A side-effecting system. *)

src/framework/cfgTools.ml

@@ -257,7 +257,7 @@ let createCFG (file: file) =
         let pseudo_return = lazy (
           let newst = mkStmt (Return (None, fd_loc)) in
           newst.sid <- get_pseudo_return_id fd;
-          fd.sallstmts <- fd.sallstmts @ [newst]; (* TODO: anything bad happen from changing sallstmts? should also update smaxid? *)
+          Cilfacade.StmtH.add Cilfacade.pseudo_return_to_fun newst fd;
           let newst_node = Statement newst in
           addEdge newst_node (fd_loc, Ret (None, fd)) (Function fd);
           newst_node

src/framework/node.ml

@@ -68,7 +68,7 @@ let location (node: t) =
   | Function fd -> fd.svar.vdecl
   | FunctionEntry fd -> fd.svar.vdecl
 
-(** Find [fundec] which the node is in. *)
+(** Find [fundec] which the node is in. In an incremental run this might yield old fundecs for pseudo-return nodes from the old file. *)
 let find_fundec (node: t) =
   match node with
   | Statement stmt -> Cilfacade.find_stmt_fundec stmt

src/incremental/compareAST.ml

@@ -1,20 +1,5 @@
 open Cil
 
-type changed_global = {
-  old: global;
-  current: global;
-  unchangedHeader: bool
-}
-
-type change_info = {
-  mutable changed: changed_global list;
-  mutable unchanged: global list;
-  mutable removed: global list;
-  mutable added: global list
-}
-
-let empty_change_info () : change_info = {added = []; removed = []; changed = []; unchanged = []}
-
 type global_type = Fun | Decl | Var | Other
 
 and global_identifier = {name: string ; global_t: global_type} [@@deriving ord]
@@ -160,8 +145,8 @@ and eq_attribute (a: attribute) (b: attribute) = match a, b with
     Attr (name1, params1), Attr (name2, params2) -> name1 = name2 && eq_list eq_attrparam params1 params2
 
 and eq_varinfo (a: varinfo) (b: varinfo) = a.vname = b.vname && eq_typ a.vtype b.vtype && eq_list eq_attribute a.vattr b.vattr &&
-                                           a.vstorage = b.vstorage && a.vglob = b.vglob && a.vinline = b.vinline && a.vaddrof = b.vaddrof
-(* Ignore the location, vid, vreferenced, vdescr, vdescrpure *)
+                                           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 *)
 and eq_compinfo (a: compinfo) (b: compinfo) (acc: (typ * typ) list) =
@@ -191,6 +176,7 @@ let eq_instr (a: instr) (b: instr) = match a, b with
   | Call (Some lv1, f1, args1, _l1), Call (Some lv2, f2, args2, _l2) -> eq_lval lv1 lv2 && eq_exp f1 f2 && eq_list eq_exp args1 args2
   | Call (None, f1, args1, _l1), Call (None, f2, args2, _l2) -> eq_exp f1 f2 && eq_list eq_exp args1 args2
   | Asm (attr1, tmp1, ci1, dj1, rk1, l1), Asm (attr2, tmp2, ci2, dj2, rk2, l2) -> eq_list String.equal tmp1 tmp2 && eq_list(fun (x1,y1,z1) (x2,y2,z2)-> x1 = x2 && y1 = y2 && eq_lval z1 z2) ci1 ci2 && eq_list(fun (x1,y1,z1) (x2,y2,z2)-> x1 = x2 && y1 = y2 && eq_exp z1 z2) dj1 dj2 && eq_list String.equal rk1 rk2(* ignore attributes and locations *)
+  | VarDecl (v1, _l1), VarDecl (v2, _l2) -> eq_varinfo v1 v2
   | _, _ -> false
 
 let eq_label (a: label) (b: label) = match a, b with
@@ -205,46 +191,35 @@ let eq_stmt_with_location ((a, af): stmt * fundec) ((b, bf): stmt * fundec) =
   let offsetB = b.sid - (List.hd bf.sallstmts).sid in
   eq_list eq_label a.labels b.labels && offsetA = offsetB
 
-let rec eq_stmtkind ((a, af): stmtkind * fundec) ((b, bf): stmtkind * fundec) =
-  let eq_block' = fun x y -> eq_block (x, af) (y, bf) in
+(* cfg_comp: blocks need only be compared in the AST comparison. For cfg comparison of functions one instead walks
+   through the cfg and only compares the currently visited node (The cil blocks inside an if statement should not be
+   compared together with its condition to avoid a to early and not precise detection of a changed node inside).
+   Switch, break and continue statements are removed during cfg preparation and therefore need not to be handeled *)
+let rec eq_stmtkind ?(cfg_comp = false) ((a, af): stmtkind * fundec) ((b, bf): stmtkind * fundec) =
+  let eq_block' = fun x y -> if cfg_comp then true else eq_block (x, af) (y, bf) in
   match a, b with
   | Instr is1, Instr is2 -> eq_list eq_instr is1 is2
   | Return (Some exp1, _l1), Return (Some exp2, _l2) -> eq_exp exp1 exp2
   | Return (None, _l1), Return (None, _l2) -> true
   | Return _, Return _ -> false
   | Goto (st1, _l1), Goto (st2, _l2) -> eq_stmt_with_location (!st1, af) (!st2, bf)
-  | Break _, Break _ -> true
-  | Continue _, Continue _ -> true
+  | Break _, Break _ -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else true
+  | Continue _, Continue _ -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else true
   | If (exp1, then1, else1, _l1), If (exp2, then2, else2, _l2) -> eq_exp exp1 exp2 && eq_block' then1 then2 && eq_block' else1 else2
-  | Switch (exp1, block1, stmts1, _l1), Switch (exp2, block2, stmts2, _l2) -> eq_exp exp1 exp2 && eq_block' block1 block2 && eq_list (fun a b -> eq_stmt (a,af) (b,bf)) stmts1 stmts2
+  | Switch (exp1, block1, stmts1, _l1), Switch (exp2, block2, stmts2, _l2) -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else eq_exp exp1 exp2 && eq_block' block1 block2 && eq_list (fun a b -> eq_stmt (a,af) (b,bf)) stmts1 stmts2
   | Loop (block1, _l1, _con1, _br1), Loop (block2, _l2, _con2, _br2) -> eq_block' block1 block2
   | Block block1, Block block2 -> eq_block' block1 block2
   | TryFinally (tryBlock1, finallyBlock1, _l1), TryFinally (tryBlock2, finallyBlock2, _l2) -> eq_block' tryBlock1 tryBlock2 && eq_block' finallyBlock1 finallyBlock2
   | TryExcept (tryBlock1, exn1, exceptBlock1, _l1), TryExcept (tryBlock2, exn2, exceptBlock2, _l2) -> eq_block' tryBlock1 tryBlock2 && eq_block' exceptBlock1 exceptBlock2
   | _, _ -> false
 
-and eq_stmt ((a, af): stmt * fundec) ((b, bf): stmt * fundec) =
+and eq_stmt ?(cfg_comp = false) ((a, af): stmt * fundec) ((b, bf): stmt * fundec) =
   List.for_all (fun (x,y) -> eq_label x y) (List.combine a.labels b.labels) &&
-  eq_stmtkind (a.skind, af) (b.skind, bf)
+  eq_stmtkind ~cfg_comp (a.skind, af) (b.skind, bf)
 
 and eq_block ((a, af): Cil.block * fundec) ((b, bf): Cil.block * fundec) =
   a.battrs = b.battrs && List.for_all (fun (x,y) -> eq_stmt (x, af) (y, bf)) (List.combine a.bstmts b.bstmts)
 
-let eqF (a: Cil.fundec) (b: Cil.fundec) =
-  let unchangedHeader =
-    try
-      eq_varinfo a.svar b.svar &&
-      List.for_all (fun (x, y) -> eq_varinfo x y) (List.combine a.sformals b.sformals)
-    with Invalid_argument _ -> false in
-  let identical =
-    try
-      unchangedHeader &&
-      List.for_all (fun (x, y) -> eq_varinfo x y) (List.combine a.slocals b.slocals) &&
-      eq_block (a.sbody, a) (b.sbody, b)
-    with Invalid_argument _ -> (* The combine failed because the lists have differend length *)
-      false in
-  identical, unchangedHeader
-
 let rec eq_init (a: init) (b: init) = match a, b with
   | SingleInit e1, SingleInit e2 -> eq_exp e1 e2
   | CompoundInit (t1, l1), CompoundInit (t2, l2) -> eq_typ t1 t2 && eq_list (fun (o1, i1) (o2, i2) -> eq_offset o1 o2 && eq_init i1 i2) l1 l2
@@ -254,50 +229,3 @@ let eq_initinfo (a: initinfo) (b: initinfo) = match a.init, b.init with
   | (Some init_a), (Some init_b) -> eq_init init_a init_b
   | None, None -> true
   | _, _ -> false
-
-let eq_glob (a: global) (b: global) = match a, b with
-  | GFun (f,_), GFun (g,_) -> eqF f g
-  | GVar (x, init_x, _), GVar (y, init_y, _) -> (eq_varinfo x y, false) (* 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)
-  | _ -> print_endline @@ "Not comparable: " ^ (Pretty.sprint ~width:100 (Cil.d_global () a)) ^ " and " ^ (Pretty.sprint ~width:100 (Cil.d_global () a)); (false, false)
-
-(* Returns a list of changed functions *)
-let compareCilFiles (oldAST: Cil.file) (newAST: Cil.file) =
-  let addGlobal map global  =
-    try
-      GlobalMap.add (identifier_of_global global) global map
-    with
-      e -> map
-  in
-  let changes = empty_change_info () in
-  global_typ_acc := [];
-  let checkUnchanged map global =
-    try
-      let ident = identifier_of_global global in
-      (try
-         let old_global = GlobalMap.find ident map in
-         (* Do a (recursive) equal comparision ignoring location information *)
-         let identical, unchangedHeader = eq_glob old_global global in
-         if identical
-         then changes.unchanged <- global :: changes.unchanged
-         else changes.changed <- {current = global; old = old_global; unchangedHeader = unchangedHeader} :: changes.changed
-       with Not_found -> ())
-    with NoGlobalIdentifier _ -> () (* Global was no variable or function, it does not belong into the map *)
-  in
-  let checkExists map global =
-    let name = identifier_of_global global in
-    GlobalMap.mem name map
-  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
-  (*  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. *)
-  let module StringSet = Set.Make (String) in
-  Cil.iterGlobals newAST
-    (fun glob -> checkUnchanged oldMap glob);
-
-  (* We check whether functions have been added or removed *)
-  Cil.iterGlobals newAST (fun glob -> try if not (checkExists oldMap glob) then changes.added <- (glob::changes.added) with e -> ());
-  Cil.iterGlobals oldAST (fun glob -> try if not (checkExists newMap glob) then changes.removed <- (glob::changes.removed) with e -> ());
-  changes

src/incremental/compareCFG.ml

@@ -0,0 +1,135 @@
+open MyCFG
+open Queue
+open Cil
+include CompareAST
+
+let eq_node (x, fun1) (y, fun2) =
+  match x,y with
+  | Statement s1, Statement s2 -> (try eq_stmt ~cfg_comp:true (s1, fun1) (s2, fun2) with Invalid_argument _ -> false)
+  | Function f1, Function f2 -> eq_varinfo f1.svar f2.svar
+  | FunctionEntry f1, FunctionEntry f2 -> eq_varinfo f1.svar f2.svar
+  | _ -> false
+
+(* TODO: compare ASMs properly instead of simply always assuming that they are not the same *)
+let eq_edge x y = match x, y with
+  | Assign (lv1, rv1), Assign (lv2, rv2) -> eq_lval lv1 lv2 && eq_exp rv1 rv2
+  | Proc (None,f1,ars1), Proc (None,f2,ars2) -> eq_exp f1 f2 && eq_list eq_exp ars1 ars2
+  | Proc (Some r1,f1,ars1), Proc (Some r2,f2,ars2) ->
+      eq_lval r1 r2 && eq_exp f1 f2 && eq_list eq_exp ars1 ars2
+  | Entry f1, Entry f2 -> eq_varinfo f1.svar f2.svar
+  | Ret (None,fd1), Ret (None,fd2) -> eq_varinfo fd1.svar fd2.svar
+  | Ret (Some r1,fd1), Ret (Some r2,fd2) -> eq_exp r1 r2 && eq_varinfo fd1.svar fd2.svar
+  | Test (p1,b1), Test (p2,b2) -> eq_exp p1 p2 && b1 = b2
+  | ASM _, ASM _ -> false
+  | Skip, Skip -> true
+  | VDecl v1, VDecl v2 -> eq_varinfo v1 v2
+  | SelfLoop, SelfLoop -> true
+  | _ -> false
+
+(* The order of the edges in the list is relevant. Therefore compare them one to one without sorting first *)
+let eq_edge_list xs ys = eq_list eq_edge xs ys
+
+let to_edge_list ls = List.map (fun (loc, edge) -> edge) ls
+
+module NH = Hashtbl.Make(Node)
+module NTH = Hashtbl.Make(
+  struct
+    type t = Node.t * Node.t
+    [@@deriving eq]
+    let hash (n1,n2) = (Node.hash n1 * 13) + Node.hash n2
+  end)
+
+(* This function compares two CFGs by doing a breadth-first search on the old CFG. Matching node tuples are stored in same,
+ * nodes from the old CFG for which no matching node can be found are added to diff. For each matching node tuple
+ * (fromNode1, fromNode2) found, one iterates over the successors of fromNode1 from the old CFG and checks for a matching node
+ * in the succesors of fromNode2 in the new CFG. Matching node tuples are added to the waitingList to repeat the matching
+ * process on their successors. If a node from the old CFG can not be matched, it is added to diff and no further
+ * comparison is done for its successors. The two function entry nodes make up the tuple to start the comparison from. *)
+let compareCfgs (module CfgOld : CfgForward) (module CfgNew : CfgForward) fun1 fun2 =
+  let diff = NH.create 113 in
+  let same = NTH.create 113 in
+  let waitingList : (node * node) t = Queue.create () in
+
+  let rec compareNext () =
+    if Queue.is_empty waitingList then ()
+    else
+      let fromNode1, fromNode2 = Queue.take waitingList in
+      let outList1 = CfgOld.next fromNode1 in
+      let outList2 = CfgNew.next fromNode2 in
+
+      (* Find a matching edge and successor node for (edgeList1, toNode1) in the list of successors of fromNode2.
+       * If successful, add the matching node tuple to same, else add toNode1 to the differing nodes. *)
+      let findMatch (edgeList1, toNode1) =
+        let rec aux remSuc = match remSuc with
+          | [] -> NH.replace diff toNode1 ()
+          | (locEdgeList2, toNode2)::remSuc' ->
+              let edgeList2 = to_edge_list locEdgeList2 in
+              if eq_node (toNode1, fun1) (toNode2, fun2) && eq_edge_list edgeList1 edgeList2 then
+                begin
+                  let notInSame = not (NTH.mem same (toNode1, toNode2)) in
+                  let matchedAlready = NTH.fold (fun (toNode1', toNode2') _ acc ->
+                      acc || (Node.equal toNode1 toNode1' && not (Node.equal toNode2 toNode2'))) same false in
+                  if matchedAlready then NH.replace diff toNode1 ()
+                  else NTH.replace same (toNode1, toNode2) ();
+                  if notInSame then Queue.add (toNode1, toNode2) waitingList
+                end
+              else aux remSuc' in
+        aux outList2 in
+      (* For a toNode1 from the list of successors of fromNode1, check whether it might have duplicate matches.
+       * In that case declare toNode1 as differing node. Else, try finding a match in the list of successors
+       * of fromNode2 in the new CFG using findMatch. *)
+      let iterOuts (locEdgeList1, toNode1) =
+        let edgeList1 = to_edge_list locEdgeList1 in
+        (* Differentiate between a possibly duplicate Test(1,false) edge and a single occurence. In the first
+         * case the edge is directly added to the diff set to avoid undetected ambiguities during the recursive
+         * call. *)
+        let testFalseEdge edge = match edge with
+          | Test (p,b) -> p = Cil.one && b = false
+          | _ -> false in
+        let posAmbigEdge edgeList = let findTestFalseEdge (ll,_) = testFalseEdge (snd (List.hd ll)) in
+          let numDuplicates l = List.length (List.find_all findTestFalseEdge l) in
+          testFalseEdge (List.hd edgeList) && (numDuplicates outList1 > 1 || numDuplicates outList2 > 1) in
+        if posAmbigEdge edgeList1 then NH.replace diff toNode1 ()
+        else findMatch (edgeList1, toNode1) in
+    List.iter iterOuts outList1; compareNext () in
+
+  let entryNode1, entryNode2 = (FunctionEntry fun1, FunctionEntry fun2) in
+  Queue.push (entryNode1,entryNode2) waitingList; compareNext (); (same, diff)
+
+(* This is the second phase of the CFG comparison of functions. It removes the nodes from the matching node set 'same'
+ * that have an incoming backedge in the new CFG that can be reached from a differing new node. This is important to
+ * recognize new dependencies between unknowns that are not contained in the infl from the previous run. *)
+let reexamine f1 f2 (same : unit NTH.t) (diffNodes1 : unit NH.t) (module CfgOld : CfgForward) (module CfgNew : CfgForward) =
+  NTH.filter_map_inplace (fun (n1,n2) _ -> if NH.mem diffNodes1 n1 then None else Some ()) same;
+  NTH.add same (FunctionEntry f1, FunctionEntry f2) ();
+  let vis = NH.create 103 in
+  let diffNodes2 = NH.create 103 in
+
+  let asSndInSame k = NTH.fold (fun (n1,n2) _ acc -> acc || Node.equal n2 k) same false in
+  (* remove all nodes that are affected by a primary new node from same, add the first reached tuple to the primary differing node sets *)
+  let rec refine_same firstReached k =
+    if NH.mem vis k then ()
+    else begin
+      NH.add vis k ();
+      if asSndInSame k then begin
+        NTH.filter_map_inplace (fun (n1,n2) _ -> if Node.equal n2 k then (if not firstReached then (NH.replace diffNodes1 n1 (); NH.replace diffNodes2 n2 ()); None) else Some ()) same;
+        dfs2 k (refine_same true) end
+      else if firstReached || NH.mem diffNodes2 k then ()
+      else dfs2 k (refine_same firstReached) end
+  (* find the primary new nodes, the first non-classified nodes in the new cfg (correspond to the primary obsolete nodes) *)
+  and classify_prim_new k =
+    if NH.mem vis k then ()
+    else begin
+      NH.replace vis k ();
+      if asSndInSame k then dfs2 k classify_prim_new
+      else (NH.add diffNodes2 k (); NH.clear vis; dfs2 k (refine_same false)) end
+  and dfs2 node f =
+    let succ = List.map snd (CfgNew.next node) in
+    List.iter f succ in
+  dfs2 (FunctionEntry f2) classify_prim_new;
+  (NTH.to_seq_keys same, NH.to_seq_keys diffNodes1, NH.to_seq_keys diffNodes2)
+
+let compareFun (module CfgOld : CfgForward) (module CfgNew : CfgForward) fun1 fun2 =
+  let same, diff = compareCfgs (module CfgOld) (module CfgNew) fun1 fun2 in
+  let unchanged, diffNodes1, diffNodes2 = reexamine fun1 fun2 same diff (module CfgOld) (module CfgNew) in
+  List.of_seq unchanged, List.of_seq diffNodes1, List.of_seq diffNodes2