diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml index d2d969c6e2..d5a496b834 100644 --- a/.github/workflows/locked.yml +++ b/.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' }} diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml index 29e120c69b..445e7e04d2 100644 --- a/.github/workflows/unlocked.yml +++ b/.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 diff --git a/docs/developer-guide/testing.md b/docs/developer-guide/testing.md index 2460bfe871..6c25492faa 100644 --- a/docs/developer-guide/testing.md +++ b/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 diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb index c461530e46..6b97c28f17 100755 --- a/scripts/update_suite.rb +++ b/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 diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 05a0f3a7ce..ea25757435 100644 --- a/src/solvers/td3.ml +++ b/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 (