diff --git a/docs/developer-guide/testing.md b/docs/developer-guide/testing.md index 0854e4f33d..87c97cc5d1 100644 --- a/docs/developer-guide/testing.md +++ b/docs/developer-guide/testing.md @@ -53,6 +53,7 @@ Comments at the end of other lines indicate the behavior on that line: | `DEADLOCK` | Deadlock warning | Deadlock is possible | Soundness | | `NOWARN` | No warning | — | Precision | | `WARN` | Some warning | — | Soundness | +| `NOFAIL` | Assertion is unknown
or succeeds | Everything except fail | Incremental analysis | #### Other Other useful constructs are the following: @@ -136,6 +137,9 @@ git diff --no-prefix relative/path/to/test.c relative/path/to/test.json > relati The comparison input and the metadata in the patch headers are not necessary and can be removed. +### Test Automation for Incremental Analysis - TAIA +The "Test Automation for Incremental Analysis" in the bench repository (`bench/incremental-analysis-test-toolchain`) enables you to generate and run incremental tests based on one single c file as input. You find more details in the readme file in the repository (`bench/incremental-analysis-test-toolchain/README.md`). + ## Unit tests ### Running diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb index 2722b3ddb5..3668bdaaee 100755 --- a/scripts/update_suite.rb +++ b/scripts/update_suite.rb @@ -221,6 +221,8 @@ def compare_warnings check.call warnings[idx] != "race" when "nodeadlock" check.call warnings[idx] != "deadlock" + when "nofail" + check.call(warnings[idx] != "fail") end end end @@ -300,33 +302,43 @@ def parse_tests (lines) i = $1.to_i - 1 end next if obj =~ /^\s*\/\// || obj =~ /^\s*\/\*([^*]|\*+[^*\/])*\*\/$/ - todo << i if obj =~ /TODO|SKIP/ + todo << i if obj =~ /(\b|\/)(TODO|SKIP)/ tests_line[i] = obj - if obj =~ /RACE/ then - tests[i] = if obj =~ /NORACE/ then "norace" else "race" end - elsif obj =~ /DEADLOCK/ then - tests[i] = if obj =~ /NODEADLOCK/ then "nodeadlock" else "deadlock" end - elsif obj =~ /WARN/ then - tests[i] = if obj =~ /NOWARN/ then "nowarn" else "warn" end - elsif obj =~ /SUCCESS/ then + if obj =~ /(\b|\/)NOFAIL/ then + tests[i] = "nofail" + elsif obj =~ /(\b|\/)RACE/ then + tests[i] = "race" + elsif obj =~ /(\b|\/)NORACE/ then + tests[i] = "norace" + elsif obj =~ /(\b|\/)DEADLOCK/ then + tests[i] = "deadlock" + elsif obj =~ /(\b|\/)NODEADLOCK/ then + tests[i] = "nodeadlock" + elsif obj =~ /(\b|\/)WARN/ then + tests[i] = "warn" + elsif obj =~ /(\b|\/)NOWARN/ then + tests[i] = "nowarn" + elsif obj =~ /(\b|\/)SUCCESS/ then tests[i] = "success" - elsif obj =~ /FAIL/ then + elsif obj =~ /(\b|\/)FAIL/ then tests[i] = "fail" - elsif obj =~ /NONTERMLOOP/ then + elsif obj =~ /(\b|\/)NONTERMLOOP/ then tests[i] = "loop" - elsif obj =~ /NONTERMGOTO/ then + elsif obj =~ /(\b|\/)NONTERMGOTO/ then tests[i] = "goto" - elsif obj =~ /NONTERMFUNDEC/ then + elsif obj =~ /(\b|\/)NONTERMFUNDEC/ then tests[i] = "fundec" - elsif obj =~ /UNKNOWN/ then + elsif obj =~ /(\b|\/)UNKNOWN/ then tests[i] = "unknown" - elsif obj =~ /(assert|__goblint_check).*\(/ then - if obj =~ /FAIL/ then - tests[i] = "fail" - elsif obj =~ /UNKNOWN/ then - tests[i] = "unknown" - else - tests[i] = "assert" + elsif obj =~ /(\b|\/)(assert|__goblint_check).*\(/ then + unless obj =~ /^\s*extern\b/ + if obj =~ /(\b|\/)FAIL/ then + tests[i] = "fail" + elsif obj =~ /(\b|\/)UNKNOWN/ then + tests[i] = "unknown" + else + tests[i] = "assert" + end end end end @@ -376,6 +388,7 @@ def run_testset (testset, cmd, starttime) lastline = (File.readlines testset.warnfile).last() filename = File.basename(@path) puts lastline.strip().sub filename, relpath(@path).to_s unless lastline.nil? + puts "Content of the warn-file: \n #{File.read(testset.warnfile)}" puts stats[0..9].itemize elsif status == 3 then warn = File.readlines testset.warnfile @@ -565,9 +578,10 @@ def run () config_path = File.expand_path(f[0..-3] + ".json", grouppath) 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 + params = "" end + lines[0] =~ /PARAM: (.*)$/ + if $1 then params << " #{$1}" else params << "" end # always enable debugging so that the warnings would work params << " --set warn.debug true" p = if incremental then diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 4d9546a9ca..ba43953fea 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1526,6 +1526,20 @@ "description": "Output filename for transformations that output a transformed file.", "type":"string", "default": "transformed.c" + }, + "assert" : { + "title": "trans.assert", + "type": "object", + "properties": { + "goblint-check": { + "title": "trans.assert.goblint-check", + "description": + "Write __goblint_check(exp) in the file instead of __VERIFIER_assert(exp).", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false } }, "additionalProperties": false diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml index 91bdb82ce1..a8d8e5d087 100644 --- a/src/transform/evalAssert.ml +++ b/src/transform/evalAssert.ml @@ -26,8 +26,11 @@ module EvalAssert = struct (* should asserts be surrounded by __VERIFIER_atomic_{begin,end}? *) let surroundByAtomic = true + (* variable for generating __goblint_check(exp) instead of __VERIFIER_assert(exp) *) + let goblintCheck () = GobConfig.get_bool "trans.assert.goblint-check" + (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *) - let ass = makeVarinfo true "__VERIFIER_assert" (TVoid []) + let ass () = if goblintCheck () then makeVarinfo true "__goblint_check" (TVoid []) else makeVarinfo true "__VERIFIER_assert" (TVoid []) let atomicBegin = makeVarinfo true "__VERIFIER_atomic_begin" (TVoid []) let atomicEnd = makeVarinfo true "__VERIFIER_atomic_end" (TVoid []) @@ -59,8 +62,8 @@ module EvalAssert = struct match (ask ~node loc).f (Queries.Invariant context) with | `Lifted e -> let es = WitnessUtil.InvariantExp.process_exp e in - let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv ass); ("exp", Fe e)]) es in - if surroundByAtomic then + let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv (ass ())); ("exp", Fe e)]) es in + if surroundByAtomic && not (goblintCheck ()) then let abegin = (cInstr ("%v:__VERIFIER_atomic_begin();") loc [("__VERIFIER_atomic_begin", Fv atomicBegin)]) in let aend = (cInstr ("%v:__VERIFIER_atomic_end();") loc [("__VERIFIER_atomic_end", Fv atomicEnd)]) in abegin :: (asserts @ [aend]) diff --git a/tests/incremental/.gitignore b/tests/incremental/.gitignore new file mode 100644 index 0000000000..76d849fa56 --- /dev/null +++ b/tests/incremental/.gitignore @@ -0,0 +1,2 @@ +# Do not consider temporary files for the running of the "Test Automation for Incremental Analysis" +99-temp diff --git a/tests/regression/36-apron/86-branched-thread-creation.c b/tests/regression/36-apron/86-branched-thread-creation.c index cac0a881a6..91a5411e8f 100644 --- a/tests/regression/36-apron/86-branched-thread-creation.c +++ b/tests/regression/36-apron/86-branched-thread-creation.c @@ -40,7 +40,7 @@ int main(void) { if(!mt) { pthread_mutex_lock(&mutex); - __goblint_check(g==h); //MAYFAIL + __goblint_check(g==h); //FAIL pthread_mutex_unlock(&mutex); } diff --git a/tests/regression/46-apron2/26-autotune.c b/tests/regression/46-apron2/26-autotune.c index 96c5c85278..ec8f55fe19 100644 --- a/tests/regression/46-apron2/26-autotune.c +++ b/tests/regression/46-apron2/26-autotune.c @@ -1,4 +1,4 @@ -//SKIP PARAM: --enable ana.int.interval --sets sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled +//SKIP PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled // Check that autotuner disables context for apron as well for recursive calls #include diff --git a/tests/regression/58-base-mm-tid/15-branched-thread-creation.c b/tests/regression/58-base-mm-tid/15-branched-thread-creation.c index 3292182adc..c7bb43519f 100644 --- a/tests/regression/58-base-mm-tid/15-branched-thread-creation.c +++ b/tests/regression/58-base-mm-tid/15-branched-thread-creation.c @@ -41,7 +41,7 @@ int main(void) { if(!mt) { pthread_mutex_lock(&mutex); - __goblint_check(g==h); //MAYFAIL + __goblint_check(g==h); //FAIL pthread_mutex_unlock(&mutex); } diff --git a/tests/regression/67-interval-sets-two/16-branched-thread-creation.c b/tests/regression/67-interval-sets-two/16-branched-thread-creation.c index c309ec8ffd..d97f800621 100644 --- a/tests/regression/67-interval-sets-two/16-branched-thread-creation.c +++ b/tests/regression/67-interval-sets-two/16-branched-thread-creation.c @@ -41,7 +41,7 @@ int main(void) { if(!mt) { pthread_mutex_lock(&mutex); - __goblint_check(g==h); //MAYFAIL + __goblint_check(g==h); //FAIL pthread_mutex_unlock(&mutex); }