Merge pull request #1597 from goblint/physical-equality

Replace most physical equality on immutable types

src/analyses/uninit.ml

@@ -135,7 +135,7 @@ struct
     in
     let utar, uoth = unrollType target, unrollType other in
     match ofs, utar, uoth with
-    |     `NoOffset,              _ ,               _ when utar == uoth  -> [v, rev cx]
+    |     `NoOffset,              _ ,               _ when CilType.Typ.equal utar uoth  -> [v, rev cx]
     |     `NoOffset,              _ ,    TComp (c2,_) when not c2.cstruct ->
       (* unroll other (union) *)
       List.concat (List.rev_map (fun oth_f -> get_pfx v (`Field (oth_f, cx)) ofs utar oth_f.ftype) c2.cfields)

src/common/util/cilfacade.ml

@@ -474,8 +474,8 @@ let rec pretty_typsig_like_typ (nameOpt: Pretty.doc option) () ts =
     (* ignore the const attribute for arrays *)
     let a' = dropAttributes [ "pconst" ] a in
     let name' =
-      if a' == [] then name else
-      if nameOpt == None then printAttributes a' else
+      if a' = [] then name else
+      if nameOpt = None then printAttributes a' else
         text "(" ++ printAttributes a' ++ name ++ text ")"
     in
     pretty_typsig_like_typ
@@ -488,8 +488,8 @@ let rec pretty_typsig_like_typ (nameOpt: Pretty.doc option) () ts =
 
   | TSFun (restyp, args, isvararg, a) ->
     let name' =
-      if a == [] then name else
-      if nameOpt == None then printAttributes a else
+      if a = [] then name else
+      if nameOpt = None then printAttributes a else
         text "(" ++ printAttributes a ++ name ++ text ")"
     in
     pretty_typsig_like_typ

src/domain/boolDomain.ml

@@ -45,7 +45,7 @@ struct
   let is_bot x = x = false
   let top () = true
   let is_top x = x = true
-  let leq x y = x == y || y
+  let leq x y = (x = y) || y
   let join = (||)
   let widen = (||)
   let meet = (&&)
@@ -67,7 +67,7 @@ struct
   let is_bot x = x = true
   let top () = false
   let is_top x = x = false
-  let leq x y = x == y || x
+  let leq x y = (x = y) || x
   let join = (&&)
   let widen = (&&)
   let meet = (||)

src/domain/lattice.ml

@@ -153,11 +153,11 @@ struct
   include Printable.HConsed (Base)
 
   let lift_f2 f x y = f (unlift x) (unlift y)
-  let narrow x y = if Arg.assume_idempotent && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.narrow x y)
-  let widen x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.widen x y)
-  let meet x y = if Arg.assume_idempotent && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.meet x y)
-  let join x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.join x y)
-  let leq x y = (x.BatHashcons.tag == y.BatHashcons.tag) || lift_f2 Base.leq x y
+  let narrow x y = if Arg.assume_idempotent && x.BatHashcons.tag = y.BatHashcons.tag then x else lift (lift_f2 Base.narrow x y)
+  let widen x y = if x.BatHashcons.tag = y.BatHashcons.tag then x else lift (lift_f2 Base.widen x y)
+  let meet x y = if Arg.assume_idempotent && x.BatHashcons.tag = y.BatHashcons.tag then x else lift (lift_f2 Base.meet x y)
+  let join x y = if x.BatHashcons.tag = y.BatHashcons.tag then x else lift (lift_f2 Base.join x y)
+  let leq x y = (x.BatHashcons.tag = y.BatHashcons.tag) || lift_f2 Base.leq x y
   let is_top = lift_f Base.is_top
   let is_bot = lift_f Base.is_bot
   let top () = lift (Base.top ())

src/incremental/compareAST.ml

@@ -91,7 +91,7 @@ and eq_exp (a: exp) (b: exp) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ
   | AlignOf typ1, AlignOf typ2 -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc
   | AlignOfE exp1, AlignOfE exp2 -> eq_exp exp1 exp2 ~rename_mapping ~acc
   | UnOp (op1, exp1, typ1), UnOp (op2, exp2, typ2) ->
-    ((op1 == op2), rename_mapping) &&>> eq_exp exp1 exp2 ~acc &&>> eq_typ_acc typ1 typ2 ~acc
+    (CilType.Unop.equal op1 op2, rename_mapping) &&>> eq_exp exp1 exp2 ~acc &&>> eq_typ_acc typ1 typ2 ~acc
   | BinOp (op1, left1, right1, typ1), BinOp (op2, left2, right2, typ2) ->  (op1 = op2, rename_mapping) &&>> eq_exp left1 left2 ~acc &&>> eq_exp right1 right2 ~acc &&>> eq_typ_acc typ1 typ2 ~acc
   | CastE (typ1, exp1), CastE (typ2, exp2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> eq_exp exp1 exp2 ~acc
   | AddrOf lv1, AddrOf lv2 -> eq_lval lv1 lv2 ~rename_mapping ~acc

src/incremental/compareCFG.ml

@@ -18,7 +18,7 @@ let (&&<>) (prev_result: bool * rename_mapping) f : bool * rename_mapping =
 let eq_node (x, fun1) (y, fun2) ~rename_mapping =
   let isPseudoReturn f sid =
     let pid = Cilfacade.get_pseudo_return_id f in
-    sid == pid in
+    sid = pid in
   match x,y with
   | Statement s1, Statement s2 ->
     let p1 = isPseudoReturn fun1 s1.sid in

src/incremental/compareCIL.ml

@@ -19,7 +19,7 @@ let name_of_global_col gc = match gc.def with
     | None -> raise (Failure "empty global record")
 
 let compare_global_col gc1 gc2 = compare (name_of_global_col gc1) (name_of_global_col gc2)
-let equal_name_global_col gc1 gc2 = compare_global_col gc1 gc2 == 0
+let equal_name_global_col gc1 gc2 = compare_global_col gc1 gc2 = 0
 
 let get_varinfo gc = match gc.decls, gc.def with
   | _, Some (Var v) -> v

src/util/loopUnrolling.ml

@@ -68,15 +68,15 @@ class isPointedAtVisitor(var) = object
   inherit nopCilVisitor
 
   method! vexpr = function
-    | AddrOf (Var info, NoOffset) when info.vid == var.vid -> raise Found
+    | AddrOf (Var info, NoOffset) when CilType.Varinfo.equal info var -> raise Found
     | _ -> DoChildren
 end
 
 class hasAssignmentVisitor(var) = object
   inherit nopCilVisitor
 
   method! vinst = function
-    | Set ((Var info, NoOffset),_,_,_) when info.vid == var.vid -> raise Found
+    | Set ((Var info, NoOffset),_,_,_) when CilType.Varinfo.equal info var -> raise Found
     | _ -> SkipChildren
 end
 

src/witness/myARG.ml

@@ -283,6 +283,7 @@ let partition_if_next if_next_n =
 module UnCilLogicIntra (Arg: SIntraOpt): SIntraOpt =
 struct
   open Cil
+  (* TODO: questionable (=) and (==) use here *)
 
   let is_equiv_stmtkind sk1 sk2 = match sk1, sk2 with
     | Instr is1, Instr is2 -> GobList.equal (=) is1 is2