Cleanup: Only have one query for must-equality between expressions

src/analyses/arinc.ml

@@ -636,7 +636,7 @@ struct
       if Pri.is_int d.pri then
         `Int (Option.get @@ Pri.to_int d.pri)
       else if Pri.is_top d.pri then `Top else `Bot
-    (* | Queries.IsPublic _ -> *)
+    (* | Queries.MayBePublic _ -> *)
     (*   `Bool ((PrE.to_int d.pre = Some 0L || PrE.to_int d.pre = None) && (not (mode_is_init d.pmo))) *)
     | _ -> Queries.Result.top ()
 

src/analyses/base.ml

@@ -19,7 +19,7 @@ module CArrays = ValueDomain.CArrays
 module BI = IntOps.BigIntOps
 
 let is_global (a: Q.ask) (v: varinfo): bool =
-  v.vglob || match a (Q.MayEscape v) with `Bool tv -> tv | _ -> false
+  v.vglob || match a (Q.MayEscape v) with `MayBool tv -> tv | _ -> false
 
 let is_static (v:varinfo): bool = v.vstorage == Static
 
@@ -30,7 +30,7 @@ let privatization = ref false
 let is_private (a: Q.ask) (_,_) (v: varinfo): bool =
   !privatization &&
   (not (ThreadFlag.is_multi a) && is_precious_glob v ||
-   match a (Q.IsPublic v) with `Bool tv -> not tv | _ ->
+   match a (Q.MayBePublic v) with `MayBool tv -> not tv | _ ->
    if M.tracing then M.tracel "osek" "isPrivate yields top(!!!!)";
    false)
 
@@ -286,10 +286,10 @@ struct
   let eval_rv_pre (ask: Q.ask) exp pr =
     let binop op e1 e2 =
       let equality () =
-        match ask (Q.ExpEq (e1,e2)) with
-        | `Bool x ->
-          if M.tracing then M.tracel "query" "ExpEq (%a, %a) = %b\n" d_exp e1 d_exp e2 x;
-          Some x
+        match ask (Q.MustBeEqual (e1,e2)) with
+        | `MustBool true ->
+          if M.tracing then M.tracel "query" "MustBeEqual (%a, %a) = %b\n" d_exp e1 d_exp e2 true;
+          Some true
         | _ -> None
       in
       let ptrdiff_ikind = match !ptrdiffType with TInt (ik,_) -> ik | _ -> assert false in
@@ -946,10 +946,10 @@ struct
         match e1_val, e2_val with
         | `Int i1, `Int i2 -> begin
             match ID.to_int i1, ID.to_int i2 with
-            | Some i1', Some i2' when i1' = i2' -> `Bool(true)
-            | _ -> Q.Result.top ()
+            | Some i1', Some i2' when i1' = i2' -> `MustBool true
+            | _ -> `MustBool false
             end
-        | _ -> Q.Result.top ()
+        | _ -> `MustBool false
       end
     | Q.MayBeEqual (e1, e2) -> begin
         (* Printf.printf "---------------------->  may equality check for %s and %s \n" (ExpDomain.short 20 (`Lifted e1)) (ExpDomain.short 20 (`Lifted e2)); *)
@@ -964,11 +964,11 @@ struct
             if ID.is_bot (ID.meet (ID.cast_to ik i1) (ID.cast_to ik i2)) then
               begin
                 (* Printf.printf "----------------------> NOPE may equality check for %s and %s \n" (ExpDomain.short 20 (`Lifted e1)) (ExpDomain.short 20 (`Lifted e2)); *)
-                `Bool(false)
+                `MayBool false
               end
-            else Q.Result.top ()
+            else `MayBool true
           end
-        | _ -> Q.Result.top ()
+        | _ -> `MayBool true
       end
     | Q.MayBeLess (e1, e2) -> begin
         (* Printf.printf "----------------------> may check for %s < %s \n" (ExpDomain.short 20 (`Lifted e1)) (ExpDomain.short 20 (`Lifted e2)); *)
@@ -981,12 +981,12 @@ struct
               if i1' >= i2' then
                 begin
                   (* Printf.printf "----------------------> NOPE may check for %s < %s \n" (ExpDomain.short 20 (`Lifted e1)) (ExpDomain.short 20 (`Lifted e2)); *)
-                  `Bool(false)
+                  `MayBool false
                 end
-              else Q.Result.top ()
-            | _ -> Q.Result.top ()
+              else `MayBool true
+            | _ -> `MayBool true
           end
-        | _ -> Q.Result.top ()
+        | _ -> `MayBool true
       end
     | _ -> Q.Result.top ()
 
@@ -1035,7 +1035,7 @@ struct
       let t = match t_override with
         | Some t -> t
         | None ->
-          let is_heap_var = match a (Q.IsHeapVar x) with `Bool(true) -> true | _ -> false in
+          let is_heap_var = match a (Q.IsHeapVar x) with `MayBool(true) -> true | _ -> false in
           if is_heap_var then
             (* the vtype of heap vars will be TVoid, so we need to trust the pointer we got to this to be of the right type *)
             (* i.e. use the static type of the pointer here *)
@@ -1093,7 +1093,7 @@ struct
           let movement_for_expr l' r' currentE' =
             let are_equal e1 e2 =
               match a (Q.MustBeEqual (e1, e2)) with
-              | `Bool t -> Q.BD.to_bool t = Some true
+              | `MustBool true -> true
               | _ -> false
             in
             let ik = Cilfacade.get_ikind (typeOf currentE') in

src/analyses/expRelation.ml

@@ -46,39 +46,44 @@ struct
         end
       | x -> x
 
+  let isFloat e =
+    match Cil.unrollTypeDeep (Cil.typeOf e) with
+    | TFloat _ -> true
+    | _ -> false
+
   let query ctx (q:Queries.t) : Queries.Result.t =
     let lvalsEq l1 l2 = Expcompare.compareExp (Lval l1) (Lval l2) in (* == would be wrong here *)
     match q with
-    | Queries.MustBeEqual (e1, e2) ->
+    | Queries.MustBeEqual (e1, e2) when not (isFloat e1) ->
       begin
         if Expcompare.compareExp (canonize e1) (canonize e2) then
-          `Bool (true)
+          `MustBool true
         else
-          Queries.Result.top()
+          `MustBool false
       end
-    | Queries.MayBeLess (e1, e2) ->
+    | Queries.MayBeLess (e1, e2) when not (isFloat e1) ->
       begin
         match e1, e2 with
         | BinOp(PlusA, Lval l1, Const(CInt64(i,_,_)), _), Lval l2 when (lvalsEq l1 l2 && Int64.compare i Int64.zero > 0) ->
-            `Bool(false)   (* c > 0 => (! x+c < x) *)
+            `MayBool false  (* c > 0 => (! x+c < x) *)
         | Lval l1, BinOp(PlusA, Lval l2, Const(CInt64(i,_,_)), _) when (lvalsEq l1 l2 && Int64.compare i Int64.zero < 0) ->
-            `Bool(false)   (* c < 0 => (! x < x+c )*)
+            `MayBool false  (* c < 0 => (! x < x+c )*)
         | BinOp(MinusA, Lval l1, Const(CInt64(i,_,_)), _), Lval l2 when (lvalsEq l1 l2 && Int64.compare i Int64.zero < 0) ->
-            `Bool(false)   (* c < 0 => (! x-c < x) *)
+            `MayBool false  (* c < 0 => (! x-c < x) *)
         | Lval l1, BinOp(MinusA, Lval l2, Const(CInt64(i,_,_)), _) when (lvalsEq l1 l2 && Int64.compare i Int64.zero > 0) ->
-            `Bool(false)   (* c < 0 => (! x < x-c) *)
+            `MayBool false  (* c < 0 => (! x < x-c) *)
         | _ ->
-            Queries.Result.top ()
+            `MayBool true
       end
-    | Queries.MayBeEqual (e1,e2) ->
+    | Queries.MayBeEqual (e1,e2) when not (isFloat e1) ->
       begin
         match e1,e2 with
         | BinOp(PlusA, Lval l1, Const(CInt64(i,_,_)), _), Lval l2
         | Lval l2, BinOp(PlusA, Lval l1, Const(CInt64(i,_,_)), _)
         | BinOp(MinusA, Lval l1, Const(CInt64(i,_,_)), _), Lval l2
         | Lval l2, BinOp(MinusA, Lval l1, Const(CInt64(i,_,_)), _) when (lvalsEq l1 l2) && Int64.compare i Int64.zero <> 0  ->
-            `Bool(false)
-        | _ -> Queries.Result.top ()
+            `MayBool false
+        | _ -> `MayBool true
       end
     | _ -> Queries.Result.top ()
 

src/analyses/mCP.ml

@@ -528,7 +528,7 @@ struct
     in
     let has_escaped g =
       match ctx.ask (Queries.MayEscape g) with
-      | `Bool false -> false
+      | `MayBool false -> false
       | _ -> true
     in
     (* The following function adds accesses to the lval-set ls

src/analyses/mallocWrapperAnalysis.ml

@@ -75,7 +75,7 @@ struct
       | _ -> MyCFG.getLoc ctx.node in
       `Varinfo (`Lifted (get_heap_var loc))
     | Q.IsHeapVar v ->
-      `Bool (Hashtbl.mem heap_vars v.vid)
+      `MayBool (Hashtbl.mem heap_vars v.vid)
     | _ -> `Top
 
     let init () =

src/analyses/mutexAnalysis.ml

@@ -155,16 +155,16 @@ struct
 
   let query ctx (q:Queries.t) : Queries.Result.t =
     match q with
-    | Queries.IsPublic _ when Lockset.is_bot ctx.local -> `Bool false
-    | Queries.IsPublic v ->
+    | Queries.MayBePublic _ when Lockset.is_bot ctx.local -> `MayBool false
+    | Queries.MayBePublic v ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ctx.local) in
       if Mutexes.mem verifier_atomic held_locks then
-        `Bool false
+        `MayBool false
       else
         let lambda_v = ctx.global v in
         let intersect = Mutexes.inter held_locks lambda_v in
         let tv = Mutexes.is_empty intersect in
-        `Bool tv
+        `MayBool tv
     | _ -> Queries.Result.top ()
 
   let may_race (ctx1,ac1) (ctx,ac2) =

src/analyses/octagon.ml

@@ -334,22 +334,22 @@ struct
         | _, Some(x) ->
           begin
             match OctagonDomain.INV.to_int x with
-            | (Some i) -> `Bool (BI.equal BI.zero i)
-            | _ -> Queries.Result.top ()
+            | (Some i) -> `MustBool (BI.equal BI.zero i)
+            | _ -> `MustBool false
           end
-        | _ -> Queries.Result.top ()
+        | _ -> `MustBool false
       end
     | Queries.MayBeEqual (exp1,exp2) ->
       begin
         match getSumAndDiffForVars exp1 exp2 with
         | _, Some(x) ->
           begin
             if OctagonDomain.INV.is_bot (OctagonDomain.INV.meet x (OctagonDomain.INV.of_int oct_ik BI.zero)) then
-              `Bool (false)
+              `MayBool false
             else
-              Queries.Result.top ()
+              `MayBool true
           end
-        | _ -> Queries.Result.top ()
+        | _ -> `MayBool true
       end
     | Queries.MayBeLess (exp1, exp2) ->
       (* TODO: Here the order of arguments actually matters, be careful *)
@@ -359,37 +359,16 @@ struct
           begin
             match OctagonDomain.INV.minimal x with
             | Some i when BI.compare i BI.zero >= 0 ->
-              `Bool(false)
-            | _ -> Queries.Result.top ()
+              `MayBool false
+            | _ -> `MayBool true
           end
-        | _ -> Queries.Result.top ()
+        | _ -> `MayBool true
       end
-    | Queries.ExpEq (exp1, exp2) ->                           (* TODO: We want to leverage all the additional information we have here *)
-      let inv1, inv2 = evaluate_exp ctx.local exp1,           (* Also, what does ExpEq actually do? Is it must or may equality?        *)
-                       evaluate_exp ctx.local exp2 in
-      if INV.is_int inv1 then
-        if INV.is_bot (INV.meet inv1 inv2) then
-          `Bool false
-        else if INV.compare inv1 inv2 = 0 then
-          `Bool true
-        else
-          `Top
-      else
-        `Top
     | Queries.EvalInt exp ->
       let inv = evaluate_exp ctx.local exp in
       if INV.is_int inv
       then `Int(INV.to_int inv |> Option.get |> BI.to_int64)
       else `Top
-    | Queries.InInterval (exp, inv) ->
-      let linv = evaluate_exp ctx.local exp in
-      let min, max = Tuple2.mapn (BI.of_int64 |> Option.map) (IntDomain.Interval32.(minimal inv, maximal inv)) in
-      (match min, max with
-        | None, _ -> `Bool false
-        | _, None -> `Bool false
-        | Some min, Some max ->
-            let inv = INV.of_interval oct_ik (min, max) in
-            `Bool (INV.leq linv inv))
     | _ -> Queries.Result.top ()
 
   let threadspawn ctx lval f args fctx = D.bot ()

src/analyses/osek.ml

@@ -570,10 +570,10 @@ struct
       let pry = resourceset_to_priority (List.map names (Mutex.Lockset.ReverseAddrSet.elements ctx.local)) in
       `Int (Int64.of_int pry)
     | Queries.Priority vname -> begin try `Int (Int64.of_int (Hashtbl.find offensivepriorities vname) ) with _ -> Queries.Result.top() end
-    | Queries.IsPublic v ->
+    | Queries.MayBePublic v ->
       let pry = resourceset_to_priority (List.map names (Mutex.Lockset.ReverseAddrSet.elements ctx.local)) in
       if pry = min_int then
-        `Bool false
+        `MayBool false
       else
         let off =
           (*         if !FlagModes.Spec.flag_list = [] then begin *)
@@ -585,7 +585,7 @@ struct
           (*             let flagstate = get_flags ctx.presub in *)
           (*             offpry_flags flagstate v *)
           (*           end *)
-        in `Bool (off > pry)
+        in `MayBool (off > pry)
     | _ -> Queries.Result.top ()
 
   let rec conv_offset x =

src/analyses/poly.ml

@@ -133,9 +133,9 @@ struct
         | _, Some s -> `Interval (IntDomain.Interval.ending s)
         | _ -> `Top
       end
-    | ExpEq (e1, e2) ->
-      if D.cil_exp_equals d e1 e2 then `Bool (Queries.BD.of_bool true)
-      else Result.top ()
+    | MustBeEqual (e1, e2) ->
+      if D.cil_exp_equals d e1 e2 then `MustBool true
+      else `MustBool false
     | _ -> Result.top ()
 end
 

src/analyses/spec.ml

@@ -220,12 +220,13 @@ struct
     | `Interval x -> "`Interval"
     | `IntSet x -> "`IntSet"
     | `Str x -> "`Str"
-    | `Bool x -> "`Bool"
     | `LvalSet x -> "`LvalSet"
     | `ExprSet x -> "`ExprSet"
     | `ExpTriples x -> "`ExpTriples"
     | `TypeSet x -> "`TypeSet"
     | `Varinfo x -> "`Varinfo"
+    | `MustBool x -> "`MustBool"
+    | `MayBool x -> "`MayBool"
     | `Bot -> "`Bot"
 
 
@@ -308,7 +309,6 @@ struct
        (match Queries.ID.to_bool i with
         | Some b when b<>tv -> M.debug_each "EvalInt: `Int bool" (* D.remove k m TODO where to get the key?? *)
         | _ -> M.debug_each "EvalInt: `Int no bool")
-     | `Bool b -> M.debug_each "EvalInt: `Bool"
      | x -> M.debug_each @@ "OTHER RESULT: "^dump_query_result x
     );
     let check a b tv =

src/analyses/symbLocks.ml

@@ -63,8 +63,8 @@ struct
 
   let same_unknown_index ask exp slocks =
     let uk_index_equal i1 i2 =
-      match ask (Queries.ExpEq (i1, i2)) with
-      | `Bot | `Bool true -> true
+      match ask (Queries.MustBeEqual (i1, i2)) with
+      | `Bot | `MustBool true -> true
       | _ -> false
     in
     let lock_index ei ee x xs =

src/analyses/threadAnalysis.ml

@@ -73,17 +73,17 @@ struct
 
   let query ctx (q: Queries.t) =
     match q with
-    | Queries.IsNotUnique -> begin
+    | Queries.MustBeUniqueThread -> begin
         let tid = ThreadId.get_current ctx.ask in
         match tid with
-        | `Lifted tid -> `Bool (is_not_unique ctx tid)
-        | _ -> `Bool (true)
+        | `Lifted tid -> `MustBool (not (is_not_unique ctx tid))
+        | _ -> `MustBool false
       end
-    | Queries.NotSingleThreaded -> begin
+    | Queries.MustBeSingleThreaded -> begin
         let tid = ThreadId.get_current ctx.ask in
         match tid with
-        | `Lifted {vname="main"; _} -> `Bool (not (D.is_empty ctx.local))
-        | _ -> `Bool (true)
+        | `Lifted {vname="main"; _} -> `MustBool (D.is_empty ctx.local)
+        | _ -> `MustBool false
       end
     | _ -> Queries.Result.top ()
 

src/analyses/threadEscape.ml

@@ -17,7 +17,7 @@ struct
   (* queries *)
   let query ctx (q:Queries.t) : Queries.Result.t =
     match q with
-    | Queries.MayEscape v -> `Bool (D.mem v ctx.local)
+    | Queries.MayEscape v -> `MayBool (D.mem v ctx.local)
     | _ -> Queries.Result.top ()
 
   (* transfer functions *)

src/analyses/threadFlag.ml

@@ -7,8 +7,8 @@ open Prelude.Ana
 open Analyses
 
 let is_multi (ask: Queries.ask): bool =
-  match ask Queries.NotSingleThreaded with
-  | `Bool b -> b
+  match ask Queries.MustBeSingleThreaded with
+  | `MustBool x -> not x
   | `Top -> true
   | _ -> failwith "ThreadFlag.is_multi"
 
@@ -60,11 +60,10 @@ struct
 
   let query ctx x =
     match x with
-    | Queries.SingleThreaded -> `Bool (Queries.BD.of_bool (not (Flag.is_multi ctx.local)))
-    | Queries.NotSingleThreaded -> `Bool (Queries.BD.of_bool (Flag.is_multi ctx.local))
-    | Queries.IsNotUnique -> `Bool (Flag.is_bad ctx.local)
+    | Queries.MustBeSingleThreaded -> `MustBool (not (Flag.is_multi ctx.local))
+    | Queries.MustBeUniqueThread -> `MustBool (not (Flag.is_bad ctx.local))
     (* This used to be in base but also commented out. *)
-    (* | Queries.IsPublic _ -> `Bool (Flag.is_multi ctx.local) *)
+    (* | Queries.MayBePublic _ -> `MayBool (Flag.is_multi ctx.local) *)
     | _ -> `Top
 
   let part_access ctx e v w =