Fix CompareAST and CompareCFG indentation (PR #622)

goblint · Mar 8, 2022 · 6958d4b · 6958d4b
1 parent a18289a
commit 6958d4b
Show file tree

Hide file tree

Showing 2 changed files with 48 additions and 48 deletions.
diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
@@ -56,40 +56,40 @@ and pretty_length () l = Pretty.num (List.length l)
 
 and eq_typ_acc (a: typ) (b: typ) (acc: (typ * typ) list) =
   if Messages.tracing then Messages.tracei "compareast" "eq_typ_acc %a vs %a (%a, %a)\n" d_type a d_type b pretty_length acc pretty_length !global_typ_acc; (* %a makes List.length calls lazy if compareast isn't being traced *)
-  let r = (match a, b with
-        | TPtr (typ1, attr1), TPtr (typ2, attr2) -> eq_typ_acc typ1 typ2 acc && GobList.equal eq_attribute attr1 attr2
-        | TArray (typ1, (Some lenExp1), attr1), TArray (typ2, (Some lenExp2), attr2) -> eq_typ_acc typ1 typ2 acc && eq_exp lenExp1 lenExp2 &&  GobList.equal eq_attribute attr1 attr2
-        | TArray (typ1, None, attr1), TArray (typ2, None, attr2) -> eq_typ_acc typ1 typ2 acc && GobList.equal eq_attribute attr1 attr2
-        | TFun (typ1, (Some list1), varArg1, attr1), TFun (typ2, (Some list2), varArg2, attr2)
-          ->  eq_typ_acc typ1 typ2 acc && GobList.equal (eq_args acc) list1 list2 && varArg1 = varArg2 &&
-              GobList.equal eq_attribute attr1 attr2
-        | TFun (typ1, None, varArg1, attr1), TFun (typ2, None, varArg2, attr2)
-          ->  eq_typ_acc typ1 typ2 acc && varArg1 = varArg2 &&
-              GobList.equal eq_attribute attr1 attr2
-        | TNamed (typinfo1, attr1), TNamed (typeinfo2, attr2) -> eq_typ_acc typinfo1.ttype typeinfo2.ttype acc && GobList.equal eq_attribute attr1 attr2 (* Ignore tname, treferenced *)
-        | TNamed (tinf, attr), b -> eq_typ_acc tinf.ttype b acc (* Ignore tname, treferenced. TODO: dismiss attributes, or not? *)
-        | a, TNamed (tinf, attr) -> eq_typ_acc a tinf.ttype acc (* Ignore tname, treferenced . TODO: dismiss attributes, or not? *)
-        (* The following two lines are a hack to ensure that anonymous types get the same name and thus, the same typsig *)
-        | TComp (compinfo1, attr1), TComp (compinfo2, attr2) ->
-          if mem_typ_acc a b acc || mem_typ_acc a b !global_typ_acc then (
-            if Messages.tracing then Messages.trace "compareast" "in acc\n";
-            true
-          )
-          else (
-            let acc = (a, b) :: acc in
-            let res = eq_compinfo compinfo1 compinfo2 acc && GobList.equal eq_attribute attr1 attr2 in
-            if res && compinfo1.cname <> compinfo2.cname then
-              compinfo2.cname <- compinfo1.cname;
-            if res then
-              global_typ_acc := (a, b) :: !global_typ_acc;
-            res
-          )
-        | TEnum (enuminfo1, attr1), TEnum (enuminfo2, attr2) -> let res = eq_enuminfo enuminfo1 enuminfo2 && GobList.equal eq_attribute attr1 attr2 in (if res && enuminfo1.ename <> enuminfo2.ename then enuminfo2.ename <- enuminfo1.ename); res
-        | TBuiltin_va_list attr1, TBuiltin_va_list attr2 -> GobList.equal eq_attribute attr1 attr2
-        | TVoid attr1, TVoid attr2 -> GobList.equal eq_attribute attr1 attr2
-        | TInt (ik1, attr1), TInt (ik2, attr2) -> ik1 = ik2 && GobList.equal eq_attribute attr1 attr2
-        | TFloat (fk1, attr1), TFloat (fk2, attr2) -> fk1 = fk2 && GobList.equal eq_attribute attr1 attr2
-        | _, _ -> false)
+  let r = match a, b with
+    | TPtr (typ1, attr1), TPtr (typ2, attr2) -> eq_typ_acc typ1 typ2 acc && GobList.equal eq_attribute attr1 attr2
+    | TArray (typ1, (Some lenExp1), attr1), TArray (typ2, (Some lenExp2), attr2) -> eq_typ_acc typ1 typ2 acc && eq_exp lenExp1 lenExp2 &&  GobList.equal eq_attribute attr1 attr2
+    | TArray (typ1, None, attr1), TArray (typ2, None, attr2) -> eq_typ_acc typ1 typ2 acc && GobList.equal eq_attribute attr1 attr2
+    | TFun (typ1, (Some list1), varArg1, attr1), TFun (typ2, (Some list2), varArg2, attr2)
+      ->  eq_typ_acc typ1 typ2 acc && GobList.equal (eq_args acc) list1 list2 && varArg1 = varArg2 &&
+          GobList.equal eq_attribute attr1 attr2
+    | TFun (typ1, None, varArg1, attr1), TFun (typ2, None, varArg2, attr2)
+      ->  eq_typ_acc typ1 typ2 acc && varArg1 = varArg2 &&
+          GobList.equal eq_attribute attr1 attr2
+    | TNamed (typinfo1, attr1), TNamed (typeinfo2, attr2) -> eq_typ_acc typinfo1.ttype typeinfo2.ttype acc && GobList.equal eq_attribute attr1 attr2 (* Ignore tname, treferenced *)
+    | TNamed (tinf, attr), b -> eq_typ_acc tinf.ttype b acc (* Ignore tname, treferenced. TODO: dismiss attributes, or not? *)
+    | a, TNamed (tinf, attr) -> eq_typ_acc a tinf.ttype acc (* Ignore tname, treferenced . TODO: dismiss attributes, or not? *)
+    (* The following two lines are a hack to ensure that anonymous types get the same name and thus, the same typsig *)
+    | TComp (compinfo1, attr1), TComp (compinfo2, attr2) ->
+      if mem_typ_acc a b acc || mem_typ_acc a b !global_typ_acc then (
+        if Messages.tracing then Messages.trace "compareast" "in acc\n";
+        true
+      )
+      else (
+        let acc = (a, b) :: acc in
+        let res = eq_compinfo compinfo1 compinfo2 acc && GobList.equal eq_attribute attr1 attr2 in
+        if res && compinfo1.cname <> compinfo2.cname then
+          compinfo2.cname <- compinfo1.cname;
+        if res then
+          global_typ_acc := (a, b) :: !global_typ_acc;
+        res
+      )
+    | TEnum (enuminfo1, attr1), TEnum (enuminfo2, attr2) -> let res = eq_enuminfo enuminfo1 enuminfo2 && GobList.equal eq_attribute attr1 attr2 in (if res && enuminfo1.ename <> enuminfo2.ename then enuminfo2.ename <- enuminfo1.ename); res
+    | TBuiltin_va_list attr1, TBuiltin_va_list attr2 -> GobList.equal eq_attribute attr1 attr2
+    | TVoid attr1, TVoid attr2 -> GobList.equal eq_attribute attr1 attr2
+    | TInt (ik1, attr1), TInt (ik2, attr2) -> ik1 = ik2 && GobList.equal eq_attribute attr1 attr2
+    | TFloat (fk1, attr1), TFloat (fk2, attr2) -> fk1 = fk2 && GobList.equal eq_attribute attr1 attr2
+    | _, _ -> false
   in
   if Messages.tracing then Messages.traceu "compareast" "eq_typ_acc %a vs %a\n" d_type a d_type b;
   r

diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml
@@ -15,7 +15,7 @@ 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 && GobList.equal eq_exp ars1 ars2
   | Proc (Some r1,f1,ars1), Proc (Some r2,f2,ars2) ->
-      eq_lval r1 r2 && eq_exp f1 f2 && GobList.equal eq_exp ars1 ars2
+    eq_lval r1 r2 && eq_exp f1 f2 && GobList.equal 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
@@ -61,18 +61,18 @@ let compareCfgs (module CfgOld : CfgForward) (module CfgNew : CfgForward) fun1 f
         let rec aux remSuc = match remSuc with
           | [] -> NH.replace diff toNode1 ()
           | (locEdgeList2, toNode2)::remSuc' ->
-              let edgeList2 = to_edge_list locEdgeList2 in
-              (* TODO: don't allow pseudo return node to be equal to normal return node, could make function unchanged, but have different sallstmts *)
-              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
+            let edgeList2 = to_edge_list locEdgeList2 in
+            (* TODO: don't allow pseudo return node to be equal to normal return node, could make function unchanged, but have different sallstmts *)
+            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
@@ -90,7 +90,7 @@ let compareCfgs (module CfgOld : CfgForward) (module CfgNew : CfgForward) fun1 f
           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
+      List.iter iterOuts outList1; compareNext () in
 
   let entryNode1, entryNode2 = (FunctionEntry fun1, FunctionEntry fun2) in
   Queue.push (entryNode1,entryNode2) waitingList; compareNext (); (same, diff)