Merge pull request #1904 from goblint/apron-unassume-extra-trivial

Fix `SharedFunctions.AssertionModule.exp_is_constraint`

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,24 +544,17 @@ struct
   module Tracked = Tracked
   module Convert = Convert (V) (Bounds) (Arg) (Tracked)
 
-  let rec exp_is_constraint = function
-    (* constraint *)
-    | BinOp ((Lt | Gt | Le | Ge | Eq | Ne), _, _, _) -> true
-    | BinOp ((LAnd | LOr), e1, e2, _) -> exp_is_constraint e1 && exp_is_constraint e2
-    | UnOp (LNot,e,_) -> exp_is_constraint e
-    (* expression *)
-    | _ -> 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) *)
         BinOp (Ne, e, zero, intType)
+        (* TODO: do this per non-constraint subexpression *)
     in
     assert_constraint ask d e' negate no_ov
 
@@ -589,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 =

tests/regression/56-witness/76-apron-unassume-extra-trivial.c

@@ -0,0 +1,11 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set ana.activated[+] unassume --set witness.yaml.unassume 76-apron-unassume-extra-trivial.yml
+#include <assert.h>
+// Using polyhedra instead of octagon, because the former has no narrowing and really needs the witness.
+int main() {
+  int i = 0;
+  while (i < 100) { // TODO: location invariant before loop doesn't work anymore
+    i++;
+  }
+  assert(i == 100);
+  return 0;
+}

tests/regression/56-witness/76-apron-unassume-extra-trivial.yml

@@ -0,0 +1,46 @@
+- entry_type: invariant_set
+  metadata:
+    format_version: "2.0"
+    uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e
+    creation_time: 2022-07-26T09:11:03Z
+    producer:
+      name: Goblint
+      version: heads/yaml-witness-unassume-0-g48503c690-dirty
+      command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression''
+        ''--html'' ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled''
+        ''76-apron-unassume-extra-trivial.c'''
+    task:
+      input_files:
+      - 76-apron-unassume-extra-trivial.c
+      input_file_hashes:
+        76-apron-unassume-extra-trivial.c: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 76-apron-unassume-extra-trivial.c
+        line: 6
+        column: 3
+        function: main
+      value: 100LL - (long long )i >= 0LL
+      format: c_expression
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 76-apron-unassume-extra-trivial.c
+        line: 6
+        column: 3
+        function: main
+      value: (long long )i >= 0LL
+      format: c_expression
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 76-apron-unassume-extra-trivial.c
+        line: 6
+        column: 3
+        function: main
+      value: '1'
+      format: c_expression

tests/regression/56-witness/dune

@@ -23,7 +23,8 @@
      (run %{update_suite} apron-unassume-precheck -q)
      (run %{update_suite} apron-tracked-global-annot -q)
      (run %{update_suite} apron-unassume-no-strengthening -q)
-     (run %{update_suite} apron-unassume-set-tokens -q)))))
+     (run %{update_suite} apron-unassume-set-tokens -q)
+     (run %{update_suite} apron-unassume-extra-trivial -q)))))
 
 (cram
  (deps (glob_files *.c) (glob_files ??-*.yml) (glob_files strip-ghost-alloc.sh)))