Merge branch 'master' into incremental_benchmarking_scripts

jerhard · jerhard · commit d4a2d8e46fab · 2022-12-30T12:28:47.000+01:00
diff --git a/Pthread.set b/Pthread.set
@@ -0,0 +1 @@
+pthread/*_comb.yml
diff --git a/gobpie-demos/chrony/chrony-4.2.json b/gobpie-demos/chrony/chrony-4.2.json
@@ -3,7 +3,7 @@
   "ana": {
     "activated": [
       "expRelation", "base", "threadid", "threadflag", "threadreturn",
-      "escape", "mutexEvents", "mutex", "access", "mallocWrapper", "mhp",
+      "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp",
       "symb_locks", "var_eq", "mallocFresh", "threadJoins"
     ],
     "ctx_insens": [
diff --git a/gobpie-demos/silver-searcher/goblint.json b/gobpie-demos/silver-searcher/goblint.json
diff --git a/gobpie-demos/silver-searcher/gobpie.json b/gobpie-demos/silver-searcher/gobpie.json
@@ -1,3 +1,3 @@
 {
-    "goblintConf": "goblint.json"
+    "goblintConf": "the_silver_searcher.json"
 }
diff --git a/gobpie-demos/silver-searcher/the_silver_searcher.json b/gobpie-demos/silver-searcher/the_silver_searcher.json
@@ -1,8 +1,9 @@
 {
+  "files": ["the_silver_searcher"],
   "ana": {
     "activated": [
       "expRelation", "base", "threadid", "threadflag", "threadreturn",
-      "escape", "mutexEvents", "mutex", "access", "mallocWrapper", "mhp",
+      "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp",
       "mallocFresh"
     ],
     "base": {
diff --git a/gobpie-demos/smtprc/smtprc.json b/gobpie-demos/smtprc/smtprc.json
@@ -3,7 +3,7 @@
   "ana": {
     "activated": [
       "expRelation", "base", "threadid", "threadflag", "threadreturn",
-      "escape", "mutexEvents", "mutex", "access", "mallocWrapper", "mhp",
+      "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp",
       "symb_locks", "var_eq", "mallocFresh", "threadJoins"
     ],
     "ctx_insens": [
@@ -12,7 +12,9 @@
     "base": {
       "privatization": "none",
       "context": {
-        "non-ptr": false
+        "non-ptr": false,
+        "int": false,
+        "interval": false
       }
     },
     "thread": {
@@ -69,10 +71,12 @@
     "cast": false,
     "race": true,
     "deadlock": false,
-    "deadcode": true,
+    "deadcode": false,
     "analyzer": false,
     "unsound": false,
     "imprecise": false,
-    "unknown": false
+    "unknown": false,
+    "race-threshold": 110,
+    "info": false
   }
 }
diff --git a/juliet/README.md b/juliet/README.md
@@ -0,0 +1,13 @@
+# Juliet Suite
+
+Assuming goblint is located at `../../analyzer/goblint`, this script should work out of the box.
+It downloads Juliet suite if not already available. By default it runs everything, but the result parsing only works for a few things...
+
+For race detection, try `python3 juliet_summary.py C/testcases/CWE366_Race_Condition_Within_Thread`.
+
+This simply runs the Juliet suite by executing commands for the positive and negative cases. These can also be called manually, such as:
+* `goblint C/testcases/CWE366_Race_Condition_Within_Thread/CWE366_Race_Condition_Within_Thread__global_int_01.c C/testcasesupport/*.c -I C/testcasesupport --sets "mainfun[+]" CWE366_Race_Condition_Within_Thread__global_int_01_good`
+* `goblint C/testcases/CWE366_Race_Condition_Within_Thread/CWE366_Race_Condition_Within_Thread__global_int_01.c C/testcasesupport/*.c -I C/testcasesupport --sets "mainfun[+]" CWE366_Race_Condition_Within_Thread__global_int_01_bad`
+
+The script creates a summary table in this root directory, 
+and the result files are stored inside `C/juliet_summary_fileoutputs/`.
diff --git a/juliet/juliet_summary.py b/juliet/juliet_summary.py
@@ -6,7 +6,7 @@
 import zipfile
 
 # Used to access Juliet Suite or to confirm its existence in the current dir
-juliet_url = 'https://samate.nist.gov/SRD/testsuites/juliet/Juliet_Test_Suite_v1.3_for_C_Cpp.zip'
+juliet_url = 'https://samate.nist.gov/SARD/downloads/test-suites/2017-10-01-juliet-test-suite-for-c-cplusplus-v1-3.zip'
 juliet_path = 'C/testcases'
 
 # Checking if the testcases path exists, if not the script will download the Juliet Suite
@@ -74,7 +74,7 @@ def check_path(filepath):
 # '_good' or '_bad' determined by input parameter 'mode'
 def goblint_cmd(filepath, filename, mode):
 	func = re.sub('a?\.c$', mode, filename) # File ending is cut and replaced by mode
-	cmd = goblint_path + ' ' + filepath + ' ' + testsupport_files + ' -I ' + testsupport_path + ' --sets "mainfun[+]" ' + func + ' --enable dbg.debug --enable dbg.timing.enabled'
+	cmd = goblint_path + ' ' + filepath + ' ' + testsupport_files + ' -I ' + testsupport_path + ' --set "mainfun[+]" ' + func + ' --set ana.malloc.unique_address_count 1 --enable dbg.debug --enable dbg.timing.enabled'
 	print(filename + ' -- ' + mode[1:] + '     ', end='\r')
 	process = subprocess.run(cmd, shell=True, check=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, universal_newlines=True)
 	#title = '#####################\n' + mode.upper() + '\n#####################\n\n'
@@ -135,7 +135,7 @@ def files_output_to_HTML(testcases, filepath, html_table):
 # # # MAIN PROCEDURES # # #
 
 # Regex string that is used to confirm that vulnerabilities were detected
-v_detection = 'is dead!|Summary for all memory locations:'
+v_detection = 'is dead!|\[Warning\]\[Race\]'
 
 # Blanks for HTML content
 # '' - empty string for HTML table that will contain results from Goblint
diff --git a/pthread/aget_comb.yml b/pthread/aget_comb.yml
@@ -0,0 +1,3 @@
+format_version: '2.0'
+
+input_files: 'aget_comb.c'
diff --git a/pthread/ctrace_comb.yml b/pthread/ctrace_comb.yml
@@ -0,0 +1,3 @@
+format_version: '2.0'
+
+input_files: 'ctrace_comb.c'
diff --git a/pthread/knot_comb.yml b/pthread/knot_comb.yml
@@ -0,0 +1,3 @@
+format_version: '2.0'
+
+input_files: 'knot_comb.c'
diff --git a/pthread/pfscan_comb.yml b/pthread/pfscan_comb.yml
@@ -0,0 +1,5 @@
+format_version: '2.0'
+
+input_files:
+  - 'pfscan_comb.c'
+  - 'pfscan_ftw.c'
diff --git a/pthread/smtprc_comb.yml b/pthread/smtprc_comb.yml
@@ -0,0 +1,3 @@
+format_version: '2.0'
+
+input_files: 'smtprc_comb.c'
diff --git a/pthread/ypbind_comb.yml b/pthread/ypbind_comb.yml
@@ -0,0 +1,3 @@
+format_version: '2.0'
+
+input_files: 'ypbind_comb.c'
diff --git a/scripts/generate_asserts_coreutils.py b/scripts/generate_asserts_coreutils.py
@@ -0,0 +1,82 @@
+# Generate asserts, as well as corresponding *.i, and *.yml files for sv-comp for the programs in bench/coreutils/.
+
+# Execute with:
+# python3 scripts/generate_assert_coreutils.py
+import os
+
+# Directory to dump created files
+outdir = "goblint-coreutils/"
+
+goblint = "../analyzer/goblint"
+
+out_file_name="instrumented_"
+outfile_setting="--set trans.output"
+cmd = goblint + " --set pre.cppflags[+] \"--std=gnu89\" --set ana.ctx_insens \"['base', 'mallocWrapper']\" --disable witness.invariant.full --set trans.activated[+] \"assert\" "
+directory = "./coreutils/"
+
+header = """// This file is part of the SV-Benchmarks collection of verification tasks:
+// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
+// SPDX-FileCopyrightText: 1985-2011 Free Software Foundation, Inc.
+// SPDX-FileCopyrightText: 2011-2022 University of Tartu & Technische Universität München
+//
+// SPDX-License-Identifier: GPL-3.0-only
+"""
+
+start_string = header + """#include <assert.h>
+extern void abort(void);
+void reach_error() { assert(0); }
+#define __VERIFIER_assert(cond) { if(!(cond)) { reach_error(); abort(); } }
+"""
+
+def prepend(file, pre):
+    f = open(file, "r")
+    contents = f.read()
+    f.close()
+
+    f = open(file, "w")
+    f.write(pre)
+    f.write(contents)
+    f.close()
+
+def gernerat_yml(i_file):
+    text = """format_version: '2.0'
+input_files: '"""+ i_file + """'
+
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: LP64
+"""
+    outfile = i_file.replace(".i", ".yml")
+    outfile = outdir + outfile
+
+    f = open(outfile, "w")
+    f.write(text)
+    f.close()
+
+def run_configuration(config, additional_prefix):
+    for f in os.listdir(directory):
+        if not os.path.isdir(outdir):
+            os.mkdir(outdir)
+        if f.endswith(".c"):
+            filename = os.fsdecode(f)
+            infile = directory + f
+            outfile = outdir + out_file_name + additional_prefix + filename
+            command = cmd + " " + config + " " + infile + " " + outfile_setting + " " + outfile
+            print("Executing command: " + command)
+            os.system(command)
+            if not os.path.exists(outfile):
+                continue
+            prepend(outfile, start_string)
+
+            outfile_prep = outfile.replace(".c", ".i");
+            preprocess = "gcc -m64 -P -E " + outfile + " > " + outfile_prep
+            os.system(preprocess)
+            prepend(outfile_prep, header)
+            gernerat_yml(os.path.basename(outfile_prep))
+
+run_configuration("", "")
+run_configuration(" --enable ana.int.interval ", "interval_")

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,3 @@`
`1`	`1`	`{`
`2`		`- "goblintConf": "goblint.json"`
	`2`	`+ "goblintConf": "the_silver_searcher.json"`
`3`	`3`	`}`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+format_version: '2.0'`
	`2`	`+`
	`3`	`+input_files: 'aget_comb.c'`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+format_version: '2.0'`
	`2`	`+`
	`3`	`+input_files: 'ctrace_comb.c'`