Unassume witness invariants during solving

scripts/suite-result-witness-evals.py

@@ -0,0 +1,42 @@
+#!/usr/bin/python3
+
+# checks evals count changes after ./scripts/update_suite.rb -w
+
+
+from pathlib import Path
+import re
+
+
+suite_result_path = Path("./tests/suite_result")
+
+def extract_evals(path):
+    with path.open() as f:
+        s = f.read()
+        m = re.search(r"evals = (\d+)", s)
+        if m is not None:
+            return int(m.group(1))
+        else:
+            return None
+
+count_same = 0
+count_better = 0
+count_worse = 0
+
+for after_path in suite_result_path.glob("*/*.warn.txt2"):
+    before_path = after_path.with_suffix(".txt")
+    print(after_path, end=" ")
+    before_evals = extract_evals(before_path)
+    after_evals = extract_evals(after_path)
+    print(before_evals, after_evals)
+    if before_evals is not None and after_evals is not None:
+        if before_evals == after_evals:
+            count_same += 1
+        elif before_evals > after_evals:
+            count_better += 1
+        else:
+            count_worse += 1
+            print(f"WORSE! by {after_evals - before_evals}")
+
+print(f"same: {count_same}")
+print(f"better: {count_better}")
+print(f"worse: {count_worse}")

scripts/update_suite.rb

@@ -62,10 +62,11 @@ def clearline
 $dump = ARGV.last == "-d" && ARGV.pop
 sequential = ARGV.last == "-s" && ARGV.pop
 marshal = ARGV.last == "-m" && ARGV.pop
+witness = ARGV.last == "-w" && ARGV.pop
 incremental = ARGV.last == "-i" && ARGV.pop
 report = ARGV.last == "-r" && ARGV.pop
 only = ARGV[0] unless ARGV[0].nil?
-if marshal || incremental then
+if marshal || witness || incremental then
   sequential = true
 end
 if marshal && incremental then
@@ -481,6 +482,23 @@ def run ()
     end
 end
 
+class ProjectWitness < Project
+  def create_test_set(lines)
+    super(lines)
+    @testset.p = self
+  end
+  def run ()
+    filename = File.basename(@path)
+    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile}0 --enable dbg.debug --set printstats true --enable witness.yaml.enabled --set goblint-dir .goblint-#{@id.sub('/','-')}-witness1 2>#{@testset.statsfile}0"
+    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set ana.activated[+] unassume --enable dbg.debug --set printstats true --set witness.yaml.unassume witness.yml --set goblint-dir .goblint-#{@id.sub('/','-')}-witness2 2>#{@testset.statsfile}"
+    starttime = Time.now
+    run_testset(@testset, cmd1, starttime)
+    starttime = Time.now
+    run_testset(@testset, cmd2, starttime)
+    FileUtils.rm_f('witness.yml')
+    end
+end
+
 #processing the file information
 projects = []
 project_ids = Set.new
@@ -528,6 +546,8 @@ def run ()
           ProjectIncr.new(id, testname, groupname, path, params, patch_path, conf_path)
         elsif marshal then
           ProjectMarshal.new(id, testname, groupname, path, params)
+        elsif witness then
+          ProjectWitness.new(id, testname, groupname, path, params)
         else
           Project.new(id, testname, groupname, path, params)
         end

src/analyses/apron/apronAnalysis.apron.ml

@@ -542,6 +542,22 @@ struct
       Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st
     | Events.Escape escaped ->
       Priv.escape ctx.node (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st escaped
+    | Events.Unassume e ->
+      let apr = AD.bot () in (* empty env *)
+      (* add only relevant vars to env *)
+      let vars = Basetype.CilExp.get_vars e |> List.unique ~eq:CilType.Varinfo.equal |> List.filter AD.varinfo_tracked in
+      if List.for_all (fun v -> not v.vglob) vars then (
+        let apr = AD.add_vars apr (List.map V.local vars) in
+        let apr = List.fold_left assert_type_bounds apr vars in (* add type bounds to avoid overflow in top state *)
+        let apr = AD.assert_inv apr e false in
+        let apr' = AD.join ctx.local.apr apr in
+        M.info ~category:Witness "apron unassumed invariant: %a" d_exp e;
+        {ctx.local with apr = apr'}
+      )
+      else (
+        M.info ~category:Witness "apron didn't unassume invariant: %a" d_exp e;
+        ctx.local (* TODO: support unassume with globals *)
+      )
     | _ ->
       st
 

src/analyses/base.ml

@@ -1773,6 +1773,11 @@ struct
         if M.tracing then M.tracel "inv" "Unhandled operator %a\n" d_binop op;
         (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *)
         a, b
+      | LAnd ->
+        if ID.to_bool c = Some true then
+          meet_bin c c
+        else
+          a, b
       | op ->
         if M.tracing then M.tracel "inv" "Unhandled operator %a\n" d_binop op;
         a, b
@@ -1805,7 +1810,7 @@ struct
         | `Int a, `Int b ->
           let ikind = Cilfacade.get_ikind_exp e1 in (* both operands have the same type (except for Shiftlt, Shiftrt)! *)
           let a', b' = inv_bin_int (a, b) ikind c op in
-          if M.tracing then M.tracel "inv" "binop: %a, a': %a, b': %a\n" d_exp e ID.pretty a' ID.pretty b';
+          if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a\n" d_exp e ID.pretty c ID.pretty a' ID.pretty b';
           let st' = inv_exp a' e1 st in
           let st'' = inv_exp b' e2 st' in
           st''
@@ -1829,7 +1834,9 @@ struct
            if is_some_bot v then raise Deadcode
            else (
              if M.tracing then M.tracel "inv" "improve variable %a from %a to %a (c = %a, c' = %a)\n" d_varinfo var VD.pretty oldv VD.pretty v ID.pretty c VD.pretty c';
-             set' (Var var,NoOffset) v st
+             let r = set' (Var var,NoOffset) v st in
+             if M.tracing then M.tracel "inv" "st from %a to %a\n" D.pretty st D.pretty r;
+             r
            )
          | Mem _, _ ->
            (* For accesses via pointers, not yet *)
@@ -2569,6 +2576,52 @@ struct
     (* D.join ctx.local @@ *)
     ctx.local
 
+  let unassume (ctx: (D.t, _, _, _) ctx) e =
+    let e_cpa = CPA.bot () in
+    let vars = Basetype.CilExp.get_vars e |> List.unique ~eq:CilType.Varinfo.equal in
+    if List.for_all (fun v -> not v.vglob) vars then (
+      let e_cpa = List.fold_left (fun e_cpa v ->
+          CPA.add v (VD.top_value v.vtype) e_cpa
+        ) e_cpa vars
+      in
+      (* TODO: structural unassume instead of invariant hack *)
+      let e_d =
+        (* The usual recursion trick for ctx. *)
+        (* Must change ctx used by ask to also use new st (not ctx.local), otherwise recursive EvalInt queries use outdated state. *)
+        (* Note: query is just called on base, but not any other analyses. Potentially imprecise, but seems to be sufficient for now. *)
+        let local: D.t = {ctx.local with cpa = e_cpa} in
+        let rec ctx' asked =
+          { ctx with
+            ask = (fun (type a) (q: a Queries.t) -> query' asked q)
+          ; local
+          }
+        and query': type a. Queries.Set.t -> a Queries.t -> a Queries.result = fun asked q ->
+          let anyq = Queries.Any q in
+          if Queries.Set.mem anyq asked then
+            Queries.Result.top q (* query cycle *)
+          else (
+            let asked' = Queries.Set.add anyq asked in
+            match q with
+            | MayEscape _ -> false (* HACK: avoids get_var in inv_exp thinking non-first var is global *)
+            | _ ->
+              query (ctx' asked') q
+          )
+        in
+        let ctx = ctx' Queries.Set.empty in
+        if M.tracing then M.traceli "unassume" "base unassuming\n";
+        let r = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local e true in
+        if M.tracing then M.traceu "unassume" "base unassumed\n";
+        r
+      in
+      M.info ~category:Witness "base unassumed invariant: %a" d_exp e;
+      M.debug ~category:Witness "base unassumed state: %a" D.pretty e_d;
+      D.join ctx.local e_d
+    )
+    else (
+      M.info ~category:Witness "base didn't unassume invariant: %a" d_exp e;
+      ctx.local (* TODO: support unassume with globals *)
+    )
+
   let event ctx e octx =
     let st: store = ctx.local in
     match e with
@@ -2586,6 +2639,8 @@ struct
     | Events.AssignSpawnedThread (lval, tid) ->
       (* TODO: is this type right? *)
       set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (`Thread (ValueDomain.Threads.singleton tid))
+    | Events.Unassume e ->
+      unassume ctx e
     | _ ->
       ctx.local
 end