Extract Cilfacade.exp_is_boolean

Author: sim642

src/analyses/baseInvariant.ml

@@ -870,15 +870,9 @@ struct
     in
     if eval_bool exp st = Some (not tv) then contra st (* we already know that the branch is dead *)
     else
-      (* C11 6.5.13, 6.5.14, 6.5.3.3: LAnd, LOr and LNot also return 0 or 1 *)
-      let is_cmp = function
-        | UnOp (LNot, _, _)
-        | BinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _, _) -> true
-        | _ -> false
-      in
       match Cilfacade.get_ikind_exp exp with
       | ik ->
-        let itv = if not tv || is_cmp exp then (* false is 0, but true can be anything that is not 0, except for comparisons which yield 1 *)
+        let itv = if not tv || Cilfacade.exp_is_boolean exp then (* false is 0, but true can be anything that is not 0, except for comparisons which yield 1 *)
             ID.of_bool ik tv (* this will give 1 for true which is only ok for comparisons *)
           else
             ID.of_excl_list ik [Z.zero] (* Lvals, Casts, arithmetic operations etc. should work with true = non_zero *)

src/cdomains/apron/sharedFunctions.apron.ml

@@ -544,18 +544,12 @@ struct
   module Tracked = Tracked
   module Convert = Convert (V) (Bounds) (Arg) (Tracked)
 
-  (* TODO: deduplicate with BaseInvariant is_cmp *)
-  let exp_is_constraint = function
-    | UnOp (LNot, _, _)
-    | BinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _, _) -> true
-    | _ -> false
-
   (* TODO: move logic-handling assert_constraint from Apron back to here, after fixing affeq bot-bot join *)
 
   (** Assert any expression. *)
   let assert_inv ask d e negate no_ov =
     let e' =
-      if exp_is_constraint e then
+      if Cilfacade.exp_is_boolean e then
         e
       else
         (* convert non-constraint expression, such that we assert(e != 0) *)
@@ -588,8 +582,8 @@ struct
     | exception Invalid_argument _ ->
       ID.top () (* real top, not a top of any ikind because we don't even know the ikind *)
     | ik ->
-      if M.tracing then M.trace "relation" "eval_int: exp_is_constraint %a = %B" d_plainexp e (exp_is_constraint e);
-      if exp_is_constraint e then
+      if M.tracing then M.trace "relation" "eval_int: exp_is_constraint %a = %B" d_plainexp e (Cilfacade.exp_is_boolean e);
+      if Cilfacade.exp_is_boolean e then
         match check_assert ask d e no_ov with
         | `True -> ID.of_bool ik true
         | `False -> ID.of_bool ik false

src/common/util/cilfacade.ml

@@ -441,6 +441,14 @@ let makeBinOp binop e1 e2 =
   let (_, e) = Cabs2cil.doBinOp binop e1 t1 e2 t2 in
   e
 
+(** Is effectively boolean-returning operation?
+    These operations have type [int], but only have values 0 or 1. *)
+let exp_is_boolean = function
+  (* C11 6.5.13, 6.5.14, 6.5.3.3: LAnd, LOr and LNot also return 0 or 1 *)
+  | UnOp (LNot, _, _)
+  | BinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _, _) -> true
+  | _ -> false
+
 let anoncomp_name_regexp = Str.regexp {|^__anon\(struct\|union\)\(_\(.+\)\)?_\([0-9]+\)$|}
 
 let split_anoncomp_name name =