Merge pull request #841 from goblint/fix-incr-tests-with-cfg-comp

Fixes for the incremental analysis with cfg comparison

.github/workflows/locked.yml

@@ -67,6 +67,9 @@ jobs:
       - name: Test incremental regression
         run: ruby scripts/update_suite.rb -i
 
+      - name: Test incremental regression with cfg comparison
+        run: ruby scripts/update_suite.rb -c
+
   extraction:
     if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
 

.github/workflows/unlocked.yml

@@ -95,6 +95,9 @@ jobs:
       - name: Test incremental regression
         run: ruby scripts/update_suite.rb -i
 
+      - name: Test incremental regression with cfg comparison
+        run: ruby scripts/update_suite.rb -c
+
   lower-bounds-downgrade:
     # use external 0install solver to downgrade: https://github.com/ocaml-opam/opam-0install-solver
     # TODO: will be built in in opam 2.2: https://github.com/ocaml/opam/pull/4909
@@ -174,6 +177,9 @@ jobs:
       - name: Test incremental regression
         run: ruby scripts/update_suite.rb -i
 
+      - name: Test incremental regression with cfg comparison
+        run: ruby scripts/update_suite.rb -c
+
   lower-bounds-docker:
     # use builtin-0install solver to remove and downgrade, opam normally compiled without, Docker images have it compiled
 
@@ -265,3 +271,6 @@ jobs:
 
       - name: Test incremental regression
         run: ruby scripts/update_suite.rb -i
+
+      - name: Test incremental regression with cfg comparison
+        run: ruby scripts/update_suite.rb -c

docs/developer-guide/testing.md

@@ -33,7 +33,8 @@ incrementally (activating the option `incremental.load`) with some changes to th
 configuration. The respective `asserts` and expected results are checked in both runs.
 
 ### Running
-The incremental tests can be run with `./scripts/update_suite.rb -i`.
+The incremental tests can be run with `./scripts/update_suite.rb -i`. With `./scripts/update_suite.rb -c` the
+incremental tests are run using the more fine-grained cfg-based change detection.
 
 ### Writing
 An incremental test case consists of three files with the same file name: the `.c` file with the initial program, a

scripts/update_suite.rb

@@ -62,7 +62,8 @@ def clearline
 $dump = ARGV.last == "-d" && ARGV.pop
 sequential = ARGV.last == "-s" && ARGV.pop
 marshal = ARGV.last == "-m" && ARGV.pop
-incremental = ARGV.last == "-i" && ARGV.pop
+cfg = ARGV.last == "-c" && ARGV.pop
+incremental = (ARGV.last == "-i" && ARGV.pop) || cfg
 report = ARGV.last == "-r" && ARGV.pop
 only = ARGV[0] unless ARGV[0].nil?
 if marshal || incremental then
@@ -519,7 +520,7 @@ def run ()
     next if not has_linux_headers and lines[0] =~ /kernel/
     if incremental then
       config_path = File.expand_path(f[0..-3] + ".json", grouppath)
-      params = "--conf #{config_path}"
+      params = if cfg then "--conf #{config_path} --set incremental.compare cfg" else "--conf #{config_path}" end
     else
       lines[0] =~ /PARAM: (.*)$/
       if $1 then params = $1 else params = "" end

src/solvers/td3.ml

@@ -520,16 +520,18 @@ module WP =
               (* collect function return for reluctant analysis *)
               mark_node obsolete_ret f (Function f)
           ) changed_funs;
-        (* Unknowns from partially changed functions need only to be collected for eager destabilization when reluctant is off *)
+        (* Primary changed unknowns from partially changed functions need only to be collected for eager destabilization when reluctant is off *)
+        (* The return nodes of partially changed functions are collected in obsolete_ret for reluctant analysis *)
         (* We utilize that force-reanalyzed functions are always considered as completely changed (and not partially changed) *)
-        if not reluctant then (
-          List.iter (fun (f, pn, _) ->
+        List.iter (fun (f, pn, _) ->
+            if not reluctant then (
               List.iter (fun n ->
                   mark_node obsolete_prim f n
                 ) pn;
+            ) else (
               mark_node obsolete_ret f (Function f);
-            ) part_changed_funs;
-        );
+            )
+          ) part_changed_funs;
 
         let old_ret = HM.create 103 in
         if reluctant then (