Changes for Pull Request bench#85: Automatic Generation of Test Cases for Incremental Static Analysis

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 <br> 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

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

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

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])

tests/incremental/.gitignore

@@ -0,0 +1,2 @@
+# Do not consider temporary files for the running of the "Test Automation for Incremental Analysis"
+99-temp

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);
   }
 

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 <goblint.h>
 

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);
   }
 

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);
   }