Use Queries.eval_bool elsewhere

Author: sim642

src/analyses/abortUnless.ml

@@ -30,12 +30,10 @@ struct
     if man.local then
       match f.sformals with
       | [arg] when isIntegralType arg.vtype ->
-        (match man.ask (EvalInt (Lval (Var arg, NoOffset))) with (* TODO: Queries.eval_bool? *)
-         | v when Queries.ID.is_bot v -> false
-         | v ->
-           match Queries.ID.to_bool v with
-           | Some b -> b
-           | None -> false)
+        (match Queries.eval_bool (Analyses.ask_of_man man) (Lval (Var arg, NoOffset)) with
+         | `Bot -> false
+         | `Lifted b -> b
+         | `Top -> false)
       | _ ->
         (* should not happen, man.local should always be false in this case *)
         false

src/analyses/memLeak.ml

@@ -228,19 +228,16 @@ struct
       warn_for_multi_threaded_due_to_abort man;
       state
     | Assert { exp; refine = true; _ } ->
-      begin match man.ask (Queries.EvalInt exp) with (* TODO: Queries.eval_bool? *)
-        | a when Queries.ID.is_bot a -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp
-        | a ->
-          begin match Queries.ID.to_bool a with
-            | Some true -> ()
-            | Some false ->
-              (* If we know for sure that the expression in "assert" is false => need to check for memory leaks *)
-              warn_for_multi_threaded_due_to_abort man;
-              check_for_mem_leak man
-            | None ->
-              warn_for_multi_threaded_due_to_abort man;
-              check_for_mem_leak man ~assert_exp_imprecise:true ~exp:(Some exp)
-          end
+      begin match Queries.eval_bool (Analyses.ask_of_man man) exp with
+        | `Bot -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp
+        | `Lifted true -> ()
+        | `Lifted false ->
+          (* If we know for sure that the expression in "assert" is false => need to check for memory leaks *)
+          warn_for_multi_threaded_due_to_abort man;
+          check_for_mem_leak man
+        | `Top ->
+          warn_for_multi_threaded_due_to_abort man;
+          check_for_mem_leak man ~assert_exp_imprecise:true ~exp:(Some exp)
       end;
       state
     | ThreadExit _ ->

src/analyses/unassumeAnalysis.ml

@@ -261,7 +261,7 @@ struct
       let e = List.fold_left (fun a {exp = b; _} -> Cil.(BinOp (LAnd, a, b, intType))) x.exp xs in
       M.info ~category:Witness "unassume invariant: %a" CilType.Exp.pretty e;
       if not !AnalysisState.postsolving then (
-        if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (man.ask (EvalInt e)) = Some false) then ( (* TODO: Queries.eval_bool? *)
+        if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.eval_bool (Analyses.ask_of_man man) e = `Lifted false) then (
           let tokens = x.token :: List.map (fun {token; _} -> token) xs in
           man.emit (Unassume {exp = e; tokens});
           List.iter WideningTokenLifter.add tokens
@@ -280,9 +280,8 @@ struct
   let body man fd =
     let pres = FH.find_all fun_pres fd in
     let st = List.fold_left (fun acc pre ->
-        let v = man.ask (EvalInt pre) in (* TODO: Queries.eval_bool? *)
         (* M.debug ~category:Witness "%a precondition %a evaluated to %a" CilType.Fundec.pretty fd CilType.Exp.pretty pre Queries.ID.pretty v; *)
-        if Queries.ID.to_bool v = Some true then
+        if Queries.eval_bool (Analyses.ask_of_man man) pre = `Lifted true then
           D.add pre acc
         else
           acc

src/domains/queries.ml

@@ -559,7 +559,7 @@ let may_be_less = eval_int_binop (module MayBool) Lt
 let eval_bool (ask: ask) e: BoolDomain.FlatBool.t =
   let e' = CastE (TInt (IBool, []), e) in
   match ask.f (EvalInt e') with
-  | v when ID.is_bot v -> `Bot
+  | v when ID.is_bot v || ID.is_bot_ikind v -> `Bot
   | v ->
     match ID.to_bool v with
     | Some b -> `Lifted b

src/transform/expressionEvaluation.ml

@@ -125,16 +125,10 @@ struct
                 value_after
 
       method private try_ask location expression =
-        match ~? (fun () -> (ask location).Queries.f (Queries.EvalInt expression)) with (* TODO: Queries.eval_bool? *)
-        (* Inapplicable: Unreachable *)
-        | Some x when Queries.ID.is_bot_ikind x -> None
-        | Some x ->
-          begin match Queries.ID.to_int x with
-            (* Evaluable: Definite *)
-            | Some i -> Some (Some (not (Z.equal i Z.zero)))
-            (* Evaluable: Inconclusive *)
-            | None -> Some None
-          end
+        match ~? (fun () -> Queries.eval_bool (ask location) expression) with
+        | Some `Bot -> None (* Inapplicable: Unreachable *)
+        | Some (`Lifted b) -> Some (Some b) (* Evaluable: Definite *)
+        | Some `Top -> Some None (* Evaluable: Inconclusive *)
         (* Inapplicable: Unlisted *)
         | None
         | exception Not_found -> None

src/witness/yamlWitness.ml

@@ -454,14 +454,15 @@ struct
                   | `Lifted c_inv ->
                     (* Collect all start states that may satisfy the invariant of current_c *)
                     List.iter (fun c ->
-                        let x = R.ask_local (c.node, c.context) ~local:c.state (Queries.EvalInt c_inv) in (* TODO: Queries.eval_bool? *)
-                        if Queries.ID.is_bot x || Queries.ID.is_bot_ikind x then (* dead code *)
+                        match Queries.eval_bool {f = (fun (type a) (q: a Queries.t) -> R.ask_local (c.node, c.context) ~local:c.state q)} c_inv with
+                        | `Bot -> (* dead code *)
                           failwith "Bottom not expected when querying context state" (* Maybe this is reachable, failwith for now so we see when this happens *)
-                        else if Queries.ID.to_bool x = Some false then () (* Nothing to do, the c does definitely not satisfy the predicate of current_c *)
-                        else begin
+                        | `Lifted false ->
+                          () (* Nothing to do, the c does definitely not satisfy the predicate of current_c *)
+                        | `Lifted true
+                        | `Top ->
                           (* Insert c into the list of weaker contexts of f *)
-                          FCMap.modify_def [] (f, current_c.context) (fun cs -> c::cs) fc_map;
-                        end
+                          FCMap.modify_def [] (f, current_c.context) (fun cs -> c::cs) fc_map
                       ) con_invs;
                   | `Bot | `Top ->
                     (* If the context invariant is None, we will not generate a precondition invariant. Nothing to do here. *)
@@ -747,15 +748,12 @@ struct
 
               let result: VR.result = match InvariantParser.parse_cil inv_parser ~fundec ~loc inv_cabs with
                 | Ok inv_exp ->
-                  let x = ask_local lvar (Queries.EvalInt inv_exp) in (* TODO: Queries.eval_bool? *)
-                  if Queries.ID.is_bot x || Queries.ID.is_bot_ikind x then (* dead code *)
-                    Option.get (VR.result_of_enum (VR.bot ()))
-                  else (
-                    match Queries.ID.to_bool x with
-                    | Some true -> Confirmed
-                    | Some false -> Refuted
-                    | None -> Unconfirmed
-                  )
+                  begin match Queries.eval_bool {f = (fun (type a) (q: a Queries.t) -> ask_local lvar q)} inv_exp with
+                    | `Bot -> Option.get (VR.result_of_enum (VR.bot ())) (* dead code *)
+                    | `Lifted true -> Confirmed
+                    | `Lifted false -> Refuted
+                    | `Top -> Unconfirmed
+                  end
                 | Error e ->
                   ParseError
               in
@@ -859,14 +857,11 @@ struct
 
                 match InvariantParser.parse_cil inv_parser ~fundec ~loc pre_cabs with
                 | Ok pre_exp ->
-                  let x = ask_local pre_lvar (Queries.EvalInt pre_exp) in (* TODO: Queries.eval_bool? *)
-                  if Queries.ID.is_bot x || Queries.ID.is_bot_ikind x then (* dead code *)
-                    true
-                  else (
-                    match Queries.ID.to_bool x with
-                    | Some b -> b
-                    | None -> false
-                  )
+                  begin match Queries.eval_bool {f = (fun (type a) (q: a Queries.t) -> ask_local pre_lvar q)} pre_exp with
+                    | `Bot -> true (* dead code *)
+                    | `Lifted b -> b
+                    | `Top -> false
+                  end
                 | Error e ->
                   M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse precondition: %s" pre;
                   M.info ~category:Witness ~loc:msgLoc "precondition has undefined variables or side effects: %s" pre;