From 8214807e0d4366fece13eff43c16c4c78ad84aab Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 11 Oct 2024 10:10:58 +0300 Subject: [PATCH 1/2] Replace most physical equality on immutable types It's implementation-defined behavior that differs between bytecode and native OCaml compilers. --- src/analyses/uninit.ml | 2 +- src/common/util/cilfacade.ml | 8 ++++---- src/domain/boolDomain.ml | 4 ++-- src/domain/lattice.ml | 10 +++++----- src/incremental/compareAST.ml | 2 +- src/incremental/compareCFG.ml | 2 +- src/incremental/compareCIL.ml | 2 +- src/util/loopUnrolling.ml | 4 ++-- src/witness/myARG.ml | 1 + 9 files changed, 18 insertions(+), 17 deletions(-) diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml index a385d0a1cd..8c217cda4e 100644 --- a/src/analyses/uninit.ml +++ b/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) diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 344d29d246..6e86701858 100644 --- a/src/common/util/cilfacade.ml +++ b/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 diff --git a/src/domain/boolDomain.ml b/src/domain/boolDomain.ml index 18399365a5..9298460c6a 100644 --- a/src/domain/boolDomain.ml +++ b/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 = (||) diff --git a/src/domain/lattice.ml b/src/domain/lattice.ml index f29cb8217d..37a4a2fef5 100644 --- a/src/domain/lattice.ml +++ b/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 ()) diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml index 5ac7a90706..59adfe00be 100644 --- a/src/incremental/compareAST.ml +++ b/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 diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml index 84b120b8e3..6c314ef7c9 100644 --- a/src/incremental/compareCFG.ml +++ b/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 diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml index ea22e02a56..837bd65589 100644 --- a/src/incremental/compareCIL.ml +++ b/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 diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 905cc39e6a..26aaaa79e1 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -68,7 +68,7 @@ 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 @@ -76,7 +76,7 @@ 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 diff --git a/src/witness/myARG.ml b/src/witness/myARG.ml index a4ab524a0e..6273ecdbd5 100644 --- a/src/witness/myARG.ml +++ b/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 From 8f5a891bedf6d029aedf00c02907f16b580756c0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 11 Oct 2024 12:11:01 +0300 Subject: [PATCH 2/2] Add parentheses to BoolDomain.leq-s to make precedence explicit It was already correct, but not obvious without looking up OCaml operator precedence. --- src/domain/boolDomain.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/domain/boolDomain.ml b/src/domain/boolDomain.ml index 9298460c6a..77fcf7e108 100644 --- a/src/domain/boolDomain.ml +++ b/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 = (||)