diff --git a/doc/man/symtab2gb.1 b/doc/man/symtab2gb.1 index 256ca36f6a1..b324fe25e02 100644 --- a/doc/man/symtab2gb.1 +++ b/doc/man/symtab2gb.1 @@ -19,6 +19,9 @@ https://github.com/model-checking/kani). \fB\-\-out\fR \fIoutfile\fR Specify the filename of the resulting binary (default: a.out) .TP +\fB\-\-goto\-functions\fR \fIfile\fR +Specify a file containing JSON-encoded goto functions +.TP \fB\-\-verbosity\fR # verbosity level .SH ENVIRONMENT diff --git a/jbmc/regression/jdiff/java-properties/test.desc b/jbmc/regression/jdiff/java-properties/test.desc index a7ae85cd3f3..0c2bfcf4177 100644 --- a/jbmc/regression/jdiff/java-properties/test.desc +++ b/jbmc/regression/jdiff/java-properties/test.desc @@ -5,6 +5,6 @@ old.jar --json-ui --show-properties --cover location activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ - "deletedFunctions": \[\n \{\n "name": "java::Test.obsolete:\(\)V",\n "properties": \[\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.obsolete:\(\)V": "18"\n \}\n \},\n "class": "coverage",\n "description": "block 1 \(lines Test.java:java::Test.obsolete:\(\)V:18\)",\n "expression": "false",\n "name": "java::Test.obsolete:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "modifiedFunctions": \[\n \{\n "name": "java::Test.:\(\)V",\n "properties": \[\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.:\(\)V": "6"\n \}\n \},\n "class": "coverage",\n "description": "block 2 \(lines Test.java:java::Test.:\(\)V:6\)",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "6"\n }\n },\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.:\(\)V": "4"\n \}\n \},\n "class": "coverage",\n "description": "block 3 \(lines Test.java:java::Test.:\(\)V:4\)",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.2",\n "sourceLocation": \{\n "bytecodeIndex": "3",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.:\(\)V": "4"\n \}\n \},\n "class": "coverage",\n "description": "block 4 \(lines Test.java:java::Test.:\(\)V:4\)",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.3",\n "sourceLocation": \{\n "bytecodeIndex": "5",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.:\(\)V": "4"\n \}\n \},\n "class": "coverage",\n "description": "block 5 \(lines Test.java:java::Test.:\(\)V:4\)",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.4",\n "sourceLocation": \{\n "bytecodeIndex": "6",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.:\(\)V": "7"\n \}\n \},\n "class": "coverage",\n "description": "block 6 \(lines Test.java:java::Test.:\(\)V:7\)",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.5",\n "sourceLocation": \{\n "bytecodeIndex": "7",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "7"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "6"\n }\n },\n \{\n "name": "java::Test.:\(\)V",\n "properties": \[\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.:\(\)V": "3"\n \}\n \},\n "class": "coverage",\n "description": "block 1 \(lines Test.java:java::Test.:\(\)V:3\)",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "3"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "3"\n }\n }\n ],\n "newFunctions": \[\n \{\n "name": "java::Test.newfun:\(\)V",\n "properties": \[\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.newfun:\(\)V": "18"\n \}\n \},\n "class": "coverage",\n "description": "block 1 \(lines Test.java:java::Test.newfun:\(\)V:18\)",\n "expression": "false",\n "name": "java::Test.newfun:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n +\s*"deletedFunctions": \[\n\s*\{\n\s*"name": "java::Test.obsolete:\(\)V",\n\s*"properties": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.obsolete:\(\)V": "18"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 1 \(lines Test.java:java::Test.obsolete:\(\)V:18\)",\n\s*"expression": "false",\n\s*"name": "java::Test.obsolete:\(\)V.coverage.1",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.obsolete:\(\)V": \{\n\s*"id": "18"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "0",\n\s*"comment": "block 1 \(lines Test.java:java::Test.obsolete:\(\)V:18\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.obsolete:\(\)V",\n\s*"line": "18",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.obsolete:\(\)V.coverage.1"\n\s*\}\n\s*\}\n\s*\],\n\s*"sourceLocation": \{\n\s*"file": "Test.java",\n\s*"function": "java::Test.obsolete:\(\)V",\n\s*"line": "18"\n\s*\}\n\s*\}\n\s*\],\n\s*"modifiedFunctions": \[\n\s*\{\n\s*"name": "java::Test.:\(\)V",\n\s*"properties": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.:\(\)V": "6"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 2 \(lines Test.java:java::Test.:\(\)V:6\)",\n\s*"expression": "false",\n\s*"name": "java::Test.:\(\)V.coverage.1",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.:\(\)V": \{\n\s*"id": "6"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "1",\n\s*"comment": "block 2 \(lines Test.java:java::Test.:\(\)V:6\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.:\(\)V",\n\s*"line": "6",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.:\(\)V.coverage.1"\n\s*\}\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.:\(\)V": "4"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 3 \(lines Test.java:java::Test.:\(\)V:4\)",\n\s*"expression": "false",\n\s*"name": "java::Test.:\(\)V.coverage.2",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.:\(\)V": \{\n\s*"id": "4"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "3",\n\s*"comment": "block 3 \(lines Test.java:java::Test.:\(\)V:4\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.:\(\)V",\n\s*"line": "4",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.:\(\)V.coverage.2"\n\s*\}\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.:\(\)V": "4"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 4 \(lines Test.java:java::Test.:\(\)V:4\)",\n\s*"expression": "false",\n\s*"name": "java::Test.:\(\)V.coverage.3",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.:\(\)V": \{\n\s*"id": "4"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "5",\n\s*"comment": "block 4 \(lines Test.java:java::Test.:\(\)V:4\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.:\(\)V",\n\s*"line": "4",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.:\(\)V.coverage.3"\n\s*\}\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.:\(\)V": "4"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 5 \(lines Test.java:java::Test.:\(\)V:4\)",\n\s*"expression": "false",\n\s*"name": "java::Test.:\(\)V.coverage.4",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.:\(\)V": \{\n\s*"id": "4"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "6",\n\s*"comment": "block 5 \(lines Test.java:java::Test.:\(\)V:4\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.:\(\)V",\n\s*"line": "4",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.:\(\)V.coverage.4"\n\s*\}\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.:\(\)V": "7"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 6 \(lines Test.java:java::Test.:\(\)V:7\)",\n\s*"expression": "false",\n\s*"name": "java::Test.:\(\)V.coverage.5",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.:\(\)V": \{\n\s*"id": "7"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "7",\n\s*"comment": "block 6 \(lines Test.java:java::Test.:\(\)V:7\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.:\(\)V",\n\s*"line": "7",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.:\(\)V.coverage.5"\n\s*\}\n\s*\}\n\s*\],\n\s*"sourceLocation": \{\n\s*"file": "Test.java",\n\s*"function": "java::Test.:\(\)V",\n\s*"line": "6"\n\s*\}\n\s*\},\n\s*\{\n\s*"name": "java::Test.:\(\)V",\n\s*"properties": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.:\(\)V": "3"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 1 \(lines Test.java:java::Test.:\(\)V:3\)",\n\s*"expression": "false",\n\s*"name": "java::Test.:\(\)V.coverage.1",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.:\(\)V": \{\n\s*"id": "3"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "1",\n\s*"comment": "block 1 \(lines Test.java:java::Test.:\(\)V:3\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.:\(\)V",\n\s*"line": "3",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.:\(\)V.coverage.1"\n\s*\}\n\s*\}\n\s*\],\n\s*"sourceLocation": \{\n\s*"file": "Test.java",\n\s*"function": "java::Test.:\(\)V",\n\s*"line": "3"\n\s*\}\n\s*\}\n\s*\],\n\s*"newFunctions": \[\n\s*\{\n\s*"name": "java::Test.newfun:\(\)V",\n\s*"properties": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.newfun:\(\)V": "18"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 1 \(lines Test.java:java::Test.newfun:\(\)V:18\)",\n\s*"expression": "false",\n\s*"name": "java::Test.newfun:\(\)V.coverage.1",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.newfun:\(\)V": \{\n\s*"id": "18"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "0",\n\s*"comment": "block 1 \(lines Test.java:java::Test.newfun:\(\)V:18\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.newfun:\(\)V",\n\s*"line": "18",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.newfun:\(\)V.coverage.1"\n\s*\}\n\s*\}\n\s*\],\n\s*"sourceLocation": \{\n\s*"file": "Test.java",\n\s*"function": "java::Test.newfun:\(\)V",\n\s*"line": "18"\n\s*\}\n\s*\}\n\s*\],\n -- ^warning: ignoring diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index ea9c02a753d..f2632fcf3b0 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -80,7 +80,6 @@ add_subdirectory(goto-cc-multi-file) add_subdirectory(goto-cc-regression-gh-issue-5380) add_subdirectory(linking-goto-binaries) add_subdirectory(symtab2gb) -add_subdirectory(symtab2gb-cbmc) add_subdirectory(solver-hardness) if(NOT WIN32) add_subdirectory(goto-ld) diff --git a/regression/Makefile b/regression/Makefile index 7206f57bf21..010916f58d9 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -53,7 +53,6 @@ DIRS = cbmc-shadow-memory \ goto-cc-regression-gh-issue-5380 \ linking-goto-binaries \ symtab2gb \ - symtab2gb-cbmc \ solver-hardness \ goto-ld \ validate-trace-xml-schema \ diff --git a/regression/cbmc-cover/json-goals1/test.desc b/regression/cbmc-cover/json-goals1/test.desc index cd379f3cf9a..78390209df6 100644 --- a/regression/cbmc-cover/json-goals1/test.desc +++ b/regression/cbmc-cover/json-goals1/test.desc @@ -4,6 +4,6 @@ main.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -\{\n\s*"goals": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\}\n\s*\],\n\s*"goalsCovered": 4,\n\s*"totalGoals": 4\n\s*\} +\{\n\s*"goals": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){22}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){22}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){22}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){22}\},\n\s*"status": "satisfied"\n\s*\}\n\s*\],\n\s*"goalsCovered": 4,\n\s*"totalGoals": 4\n\s*\} -- ^warning: ignoring diff --git a/regression/cbmc/json-interface1/test.desc b/regression/cbmc/json-interface1/test.desc index 3178df58264..5411f269136 100644 --- a/regression/cbmc/json-interface1/test.desc +++ b/regression/cbmc/json-interface1/test.desc @@ -5,8 +5,8 @@ activate-multi-line-match ^EXIT=10$ ^SIGNAL=0$ Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0 -\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "SUCCESS"\n\s*\} -\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "FAILURE",\n\s*"trace": \[ +\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"comment": "assertion 0",\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"pragma":.*\n\s*"propertyClass": "assertion",\n\s*"propertyId": "foo.assertion.\d+",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "SUCCESS"\n\s*\} +\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"comment": "assertion 0",\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"pragma":.*\n\s*"propertyClass": "assertion",\n\s*"propertyId": "foo.assertion.\d+",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "FAILURE",\n\s*"trace": \[ VERIFICATION FAILED -- "property": "foo\.assertion\.2" diff --git a/regression/cbmc/loophead-trace/test-json.desc b/regression/cbmc/loophead-trace/test-json.desc index 9754b659021..52a14cacf3d 100644 --- a/regression/cbmc/loophead-trace/test-json.desc +++ b/regression/cbmc/loophead-trace/test-json.desc @@ -4,7 +4,7 @@ test.c activate-multi-line-match ^EXIT=10$ ^SIGNAL=0$ -\s*\{\n\s* .*\n\s* "sourceLocation": \{\n\s* .*,\n\s* .*,\n\s* "line": "5",\n\s* .*\n\s* \},\n\s* "stepType": "loop-head",\n\s* .*\n\s*\},\n\s*\{\n\s* .*\n\s* "sourceLocation": \{\n\s* .*,\n\s* .*,\n\s* "line": "5",\n\s* .*\n\s* \},\n\s* "stepType": "loop-head",\n\s* .*\n\s*\}, +\s*\{\n\s* .*\n\s* "sourceLocation": \{\n\s* .*,\n\s* .*,\n\s* "line": "5",\n\s* .*,\n\s* .*\n\s* \},\n\s* "stepType": "loop-head",\n\s* .*\n\s*\},\n\s*\{\n\s* .*\n\s* "sourceLocation": \{\n\s* .*,\n\s* .*,\n\s* "line": "5",\n\s* .*,\n\s* .*\n\s* \},\n\s* "stepType": "loop-head",\n\s* .*\n\s*\}, -- -- Ensure even with sliced formulas, we get a location only step for diff --git a/regression/solver-hardness/guards/test.desc b/regression/solver-hardness/guards/test.desc index 6eac38ac4c8..70bacdcb6f2 100644 --- a/regression/solver-hardness/guards/test.desc +++ b/regression/solver-hardness/guards/test.desc @@ -5,9 +5,9 @@ main.c ^SIGNAL=0$ ^\[main.assertion.1\] line 12 should fail: FAILURE$ ^VERIFICATION FAILED$ -\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"goto_symex::\\\\guard#1 ∧ goto_symex::\\\\guard#2","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\} +\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"goto_symex::\\\\guard#1 ∧ goto_symex::\\\\guard#2","Source":\{"file":"main.c","function":"main","line":"\d+","pragma":.*,"propertyClass":.*,"propertyId":.*,"workingDirectory":".*"\}\} -- ^warning: ignoring -\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"true","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\} +\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"true","Source":\{"file":"main.c","function":"main","line":"\d+","pragma":.*,"propertyClass":.*,"propertyId":.*,"workingDirectory":".*"\}\} -- "true" must not yield any clauses. diff --git a/regression/symtab2gb-cbmc/CMakeLists.txt b/regression/symtab2gb-cbmc/CMakeLists.txt deleted file mode 100644 index a8c851843b8..00000000000 --- a/regression/symtab2gb-cbmc/CMakeLists.txt +++ /dev/null @@ -1,3 +0,0 @@ -add_test_pl_tests( - "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $" -) diff --git a/regression/symtab2gb-cbmc/Makefile b/regression/symtab2gb-cbmc/Makefile deleted file mode 100644 index 6e075833eaf..00000000000 --- a/regression/symtab2gb-cbmc/Makefile +++ /dev/null @@ -1,20 +0,0 @@ -default: tests.log - -include ../../src/config.inc -include ../../src/common - -test: - @../test.pl -e -p -c '../chain.sh $(exe) ../../../src/symtab2gb/symtab2gb ../../../src/cbmc/cbmc' - -tests.log: - @../test.pl -e -p -c '../chain.sh $(exe) ../../../src/symtab2gb/symtab2gb ../../../src/cbmc/cbmc' - -clean: - $(RM) tests.log - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - cd "$$dir"; \ - $(RM) *.out *.gb; \ - cd ..; \ - fi \ - done diff --git a/regression/symtab2gb-cbmc/README.md b/regression/symtab2gb-cbmc/README.md deleted file mode 100644 index 5b29572a245..00000000000 --- a/regression/symtab2gb-cbmc/README.md +++ /dev/null @@ -1,4 +0,0 @@ -This directory contains tests based on converting json symtab files to goto -binaries using the symtab2gb binary and then passing the generated goto binary -to cbmc. Additional arguments specified in the `.desc` file will be passed to -the cbmc binary. diff --git a/regression/symtab2gb-cbmc/chain.sh b/regression/symtab2gb-cbmc/chain.sh deleted file mode 100755 index 6d482311674..00000000000 --- a/regression/symtab2gb-cbmc/chain.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash - -set -e - -symtab2gb_exe=$1 -cbmc_exe=$2 -source="${@: -1}" -goto_binary="$source.gb" -cbmc_desc_arguments="${@:3:$#-3}" - -$symtab2gb_exe "$source" --out "$goto_binary" -$cbmc_exe $cbmc_desc_arguments "$goto_binary" diff --git a/regression/symtab2gb/README.md b/regression/symtab2gb/README.md index 2cbc1d83ce8..44cac7ec0ca 100644 --- a/regression/symtab2gb/README.md +++ b/regression/symtab2gb/README.md @@ -1,4 +1,5 @@ This directory contains tests based on converting json symtab files to goto binaries using the symtab2gb binary and then passing the generated goto binary -to cbmc. Additional arguments specified in the `.desc` file will be passed to -the symtab2gb binary. +to cbmc. Additional arguments specified in the `.desc` file up until a possible +`_` will be passed to the symtab2gb binary, any arguments specified after an `_` +are passed to cbmc. diff --git a/regression/symtab2gb/chain.sh b/regression/symtab2gb/chain.sh index 8f6261e00b3..7ef64a5b8f6 100755 --- a/regression/symtab2gb/chain.sh +++ b/regression/symtab2gb/chain.sh @@ -4,6 +4,22 @@ set -e symtab2gb_exe=$1 cbmc_exe=$2 +source="${@: -1}" +goto_binary="$source.gb" -$symtab2gb_exe "${@:3}" -$cbmc_exe a.out +args=${*:3:$#-3} +if [[ "$args" == *" _ "* ]] +then + args_symtab="${args%%" _ "*}" + args_cbmc="${args#*" _ "}" +elif [[ "$args" == "_ "* ]] +then + args_symtab="" + args_cbmc="${args#"_ "}" +else + args_symtab=$args + args_cbmc="" +fi + +$symtab2gb_exe "$source" ${args_symtab} --out "$goto_binary" +$cbmc_exe ${args_cbmc} "$goto_binary" diff --git a/regression/symtab2gb-cbmc/show_foreign_symbol_table/json-ui.desc b/regression/symtab2gb/show_foreign_symbol_table/json-ui.desc similarity index 88% rename from regression/symtab2gb-cbmc/show_foreign_symbol_table/json-ui.desc rename to regression/symtab2gb/show_foreign_symbol_table/json-ui.desc index 6e6cde0b7a5..9a2f2394f37 100644 --- a/regression/symtab2gb-cbmc/show_foreign_symbol_table/json-ui.desc +++ b/regression/symtab2gb/show_foreign_symbol_table/json-ui.desc @@ -1,6 +1,6 @@ CORE rust.json ---json-ui --show-symbol-table + _ --json-ui --show-symbol-table "symbolTable": "mode": "rust", ^EXIT=0$ diff --git a/regression/symtab2gb-cbmc/show_foreign_symbol_table/plain_text.desc b/regression/symtab2gb/show_foreign_symbol_table/plain_text.desc similarity index 90% rename from regression/symtab2gb-cbmc/show_foreign_symbol_table/plain_text.desc rename to regression/symtab2gb/show_foreign_symbol_table/plain_text.desc index 9fdf6d48328..168e384c214 100644 --- a/regression/symtab2gb-cbmc/show_foreign_symbol_table/plain_text.desc +++ b/regression/symtab2gb/show_foreign_symbol_table/plain_text.desc @@ -1,6 +1,6 @@ CORE rust.json ---show-symbol-table + _ --show-symbol-table Symbols: Mode\.+: rust ^EXIT=0$ diff --git a/regression/symtab2gb-cbmc/show_foreign_symbol_table/rust.json b/regression/symtab2gb/show_foreign_symbol_table/rust.json similarity index 100% rename from regression/symtab2gb-cbmc/show_foreign_symbol_table/rust.json rename to regression/symtab2gb/show_foreign_symbol_table/rust.json diff --git a/regression/symtab2gb-cbmc/show_foreign_symbol_table/xml-ui.desc b/regression/symtab2gb/show_foreign_symbol_table/xml-ui.desc similarity index 91% rename from regression/symtab2gb-cbmc/show_foreign_symbol_table/xml-ui.desc rename to regression/symtab2gb/show_foreign_symbol_table/xml-ui.desc index fc807f3a61a..16bc0a07dcd 100644 --- a/regression/symtab2gb-cbmc/show_foreign_symbol_table/xml-ui.desc +++ b/regression/symtab2gb/show_foreign_symbol_table/xml-ui.desc @@ -1,6 +1,6 @@ CORE rust.json ---xml-ui --show-symbol-table + _ --xml-ui --show-symbol-table ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp index b60228bb68f..f12fe323452 100644 --- a/src/ansi-c/c_preprocess.cpp +++ b/src/ansi-c/c_preprocess.cpp @@ -127,7 +127,7 @@ static void error_parse_line( if(state==2) { saved_error_location.set_file(file); - saved_error_location.set_function(irep_idt()); + saved_error_location.clear_function(); saved_error_location.set_line(line_no); saved_error_location.set_column(irep_idt()); } diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index ac07f8cf029..941ab076caf 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -3026,7 +3026,7 @@ function_definition: PARSER.pop_scope(); // We are no longer in any function. - PARSER.set_function(irep_idt()); + PARSER.clear_function(); } ; @@ -3589,7 +3589,7 @@ parameter_postfixing_abstract_declarator: // Clear function name in source location after parsing if // at global scope. if (PARSER.current_scope().prefix.empty()) { - PARSER.set_function(irep_idt()); + PARSER.clear_function(); } $$ = merge($4, $1); @@ -3621,7 +3621,7 @@ parameter_postfixing_abstract_declarator: // Clear function name in source location after parsing if // at global scope. if (PARSER.current_scope().prefix.empty()) { - PARSER.set_function(irep_idt()); + PARSER.clear_function(); } if(parser_stack($5).is_not_nil()) diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index 850424001e0..2d0e26d5eda 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -48,6 +48,14 @@ json_objectt show_goto_functions_jsont::convert( function_name.starts_with("java::org.cprover") || function_name.starts_with("java::java"); json_function["isInternal"]=jsont::json_boolean(is_internal); + json_function["isHidden"] = jsont::json_boolean(function.is_hidden()); + auto json_parameter_id_range = + make_range( + function.parameter_identifiers.begin(), + function.parameter_identifiers.end()) + .map([](const irep_idt &id) { return json_stringt{id}; }); + json_function["parameterIdentifiers"] = json_arrayt{ + json_parameter_id_range.begin(), json_parameter_id_range.end()}; if(list_only) continue; @@ -60,12 +68,14 @@ json_objectt show_goto_functions_jsont::convert( function.body.instructions) { json_objectt instruction_entry{ - {"instructionId", json_stringt(instruction.to_string())}}; + {"instructionId", json_stringt(instruction.to_string())}, + {"locationNumber", + json_numbert{std::to_string(instruction.location_number)}}}; - if(instruction.code().source_location().is_not_nil()) + if(instruction.source_location().is_not_nil()) { instruction_entry["sourceLocation"] = - json(instruction.code().source_location()); + json(instruction.source_location()); } std::ostringstream instruction_builder; @@ -74,17 +84,12 @@ json_objectt show_goto_functions_jsont::convert( instruction_entry["instruction"]= json_stringt(instruction_builder.str()); - if(!instruction.code().operands().empty()) + if(instruction.code().is_not_nil()) { - json_arrayt operand_array; - for(const exprt &operand : instruction.code().operands()) - { - json_objectt operand_object= - no_comments_irep_converter.convert_from_irep( - operand); - operand_array.push_back(operand_object); - } - instruction_entry["operands"] = std::move(operand_array); + json_objectt code_object = + no_comments_irep_converter.convert_from_irep(instruction.code()); + + instruction_entry["code"] = std::move(code_object); } if(instruction.has_condition()) @@ -96,6 +101,27 @@ json_objectt show_goto_functions_jsont::convert( instruction_entry["guard"] = std::move(guard_object); } + if(!instruction.targets.empty()) + { + auto json_target_range = + make_range(instruction.targets.begin(), instruction.targets.end()) + .map( + [](const goto_programt::targett &target) { + return json_numbert{std::to_string(target->location_number)}; + }); + instruction_entry["targets"] = + json_arrayt{json_target_range.begin(), json_target_range.end()}; + } + + if(!instruction.labels.empty()) + { + auto json_label_range = + make_range(instruction.labels.begin(), instruction.labels.end()) + .map([](const irep_idt &id) { return json_stringt{id}; }); + instruction_entry["labels"] = + json_arrayt{json_label_range.begin(), json_label_range.end()}; + } + json_instruction_array.push_back(std::move(instruction_entry)); } diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index 4a5b870ab60..08d5a7f1e36 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -177,7 +177,7 @@ static void show_symbol_table_json_ui( {"type", irep_converter.convert_from_irep(symbol.type)}, {"value", irep_converter.convert_from_irep(symbol.value)}, - {"location", irep_converter.convert_from_irep(symbol.location)}, + {"location", json(symbol.location)}, {"isType", jsont::json_boolean(symbol.is_type)}, {"isMacro", jsont::json_boolean(symbol.is_macro)}, diff --git a/src/json-symtab-language/Makefile b/src/json-symtab-language/Makefile index 3fb674732cf..adc312b6d9b 100644 --- a/src/json-symtab-language/Makefile +++ b/src/json-symtab-language/Makefile @@ -1,6 +1,9 @@ -SRC = json_symtab_language.cpp \ - json_symbol_table.cpp \ - json_symbol.cpp +SRC = json_goto_function.cpp \ + json_goto_functions.cpp \ + json_symtab_language.cpp \ + json_symbol_table.cpp \ + json_symbol.cpp \ + # Empty last line INCLUDES= -I .. diff --git a/src/json-symtab-language/json_goto_function.cpp b/src/json-symtab-language/json_goto_function.cpp new file mode 100644 index 00000000000..b8545e95e46 --- /dev/null +++ b/src/json-symtab-language/json_goto_function.cpp @@ -0,0 +1,350 @@ +/*******************************************************************\ + +Module: JSON goto_function deserialization + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// JSON goto_function deserialization + +#include "json_goto_function.h" + +#include +#include +#include +#include + +#include "json_symbol.h" + +/// Return code at "code" key in a JSON object, if any. +/// \param json: The json object to pick the value from. +/// \return An expression, unless an exception was thrown before. +static goto_instruction_codet try_get_code(const json_objectt &json) +{ + auto code_it = json.find("code"); + if(code_it == json.end()) + throw deserialization_exceptiont{ + "instruction_from_json: key 'code' not found"}; + + json_irept json2irep{true}; + irept code_irep = json2irep.convert_from_json(code_it->second); + return static_cast(code_irep); +} + +/// Return code at "code" key in a JSON object, if any. +/// \param json: The json object to pick the value from. +/// \param code_id: The expected code type +/// \return An expression, unless an exception was thrown before. +static goto_instruction_codet +try_get_code(const json_objectt &json, const irep_idt &code_id) +{ + goto_instruction_codet code = try_get_code(json); + if(code.get_statement() != code_id) + { + throw deserialization_exceptiont{ + "instruction_from_json: expected '" + id2string(code_id) + "', got '" + + id2string(code.get_statement()) + "'"}; + } + return code; +} + +/// Return expression at "guard" key in a JSON object, if any. +/// \param json: The json object to pick the value from. +/// \return An expression, unless an exception was thrown before. +static exprt try_get_guard(const json_objectt &json) +{ + auto guard_it = json.find("guard"); + if(guard_it == json.end()) + throw deserialization_exceptiont{ + "instruction_from_json: key 'guard' not found"}; + + json_irept json2irep{true}; + irept guard_irep = json2irep.convert_from_json(guard_it->second); + return static_cast(guard_irep); +} + +/// Deserialize a goto_programt::instructiont from JSON +/// \param json: The JSON object representing an instruction +/// \return A goto_programt::instructiont +static goto_programt::instructiont +instruction_from_json(const json_objectt &json) +{ + auto id_it = json.find("instructionId"); + if(id_it == json.end()) + { + throw deserialization_exceptiont{ + "instruction_from_json: key 'instructionId' not found"}; + } + auto instruction_type = try_get_string(id_it->second, "instructionId"); + + source_locationt source_location = source_locationt::nil(); + auto location_it = json.find("sourceLocation"); + if(location_it != json.end()) + source_location = try_get_source_location(location_it->second); + + if(instruction_type == "GOTO") + { + return goto_programt::make_incomplete_goto( + try_get_guard(json), source_location); + } + else if(instruction_type == "ASSUME") + { + return goto_programt::make_assumption(try_get_guard(json), source_location); + } + else if(instruction_type == "ASSERT") + { + return goto_programt::make_assertion(try_get_guard(json), source_location); + } + else if(instruction_type == "OTHER") + { + return goto_programt::make_other(try_get_code(json), source_location); + } + else if(instruction_type == "SKIP") + { + return goto_programt::make_skip(source_location); + } + else if(instruction_type == "START_THREAD") + { + return goto_programt::instructiont{ + static_cast(get_nil_irep()), + source_location, + START_THREAD, + nil_exprt{}, + {}}; + } + else if(instruction_type == "END_THREAD") + { + return goto_programt::instructiont{ + static_cast(get_nil_irep()), + source_location, + END_THREAD, + nil_exprt{}, + {}}; + } + else if(instruction_type == "LOCATION") + { + return goto_programt::make_location(source_location); + } + else if(instruction_type == "END_FUNCTION") + { + return goto_programt::make_end_function(source_location); + } + else if(instruction_type == "ATOMIC_BEGIN") + { + return goto_programt::make_atomic_begin(source_location); + } + else if(instruction_type == "ATOMIC_END") + { + return goto_programt::make_atomic_end(source_location); + } + else if(instruction_type == "SET_RETURN_VALUE") + { + return goto_programt::make_set_return_value( + to_code_return(try_get_code(json, ID_return)).return_value(), + source_location); + } + else if(instruction_type == "ASSIGN") + { + return goto_programt::make_assignment( + to_code_assign(try_get_code(json, ID_assign)), source_location); + } + else if(instruction_type == "DECL") + { + return goto_programt::make_decl( + to_code_decl(try_get_code(json, ID_decl)), source_location); + } + else if(instruction_type == "DEAD") + { + return goto_programt::instructiont{ + to_code_dead(try_get_code(json, ID_dead)), + source_location, + DEAD, + nil_exprt{}, + {}}; + } + else if(instruction_type == "FUNCTION_CALL") + { + return goto_programt::make_function_call( + to_code_function_call(try_get_code(json, ID_function_call)), + source_location); + } + else if(instruction_type == "THROW") + { + return goto_programt::make_throw(source_location); + } + else if(instruction_type == "CATCH") + { + return goto_programt::make_catch(source_location); + } + else + { + throw deserialization_exceptiont{ + "instruction_from_json: got unexpected instructionId '" + + instruction_type + "'"}; + } +} + +/// Deserialize a goto_programt from JSON +/// \param json: The JSON object representing a goto_program +/// \return A goto_programt +static goto_programt goto_program_from_json(const jsont &json) +{ + if(!json.is_array()) + throw deserialization_exceptiont{"goto_program_from_json takes an array"}; + + goto_programt program; + + // First pass: create all instructions + std::map target_map; + for(const auto &instruction_json : to_json_array(json)) + { + if(!instruction_json.is_object()) + throw deserialization_exceptiont{"instruction_from_json takes an object"}; + + const json_objectt &json_object = to_json_object(instruction_json); + auto location_number_it = json_object.find("locationNumber"); + std::optional loc_unsigned; + if( + location_number_it != json_object.end() && + location_number_it->second.is_number()) + { + loc_unsigned = string2optional_unsigned(location_number_it->second.value); + } + if(!loc_unsigned.has_value()) + { + throw deserialization_exceptiont{ + "goto_program_from_json: key 'locationNumber' not found or does not " + "map to an unsigned number"}; + } + + program.add(instruction_from_json(json_object)); + auto new_key = + target_map.insert({*loc_unsigned, std::prev(program.instructions.end())}) + .second; + if(!new_key) + { + throw deserialization_exceptiont{ + "goto_program_from_json: duplicate locationNumber " + + location_number_it->second.value}; + } + } + + // Second pass: resolve targets + goto_programt::targett instruction_it = program.instructions.begin(); + for(const auto &instruction_json : to_json_array(json)) + { + for(const auto &kv : to_json_object(instruction_json)) + { + if( + kv.first == "code" || kv.first == "guard" || + kv.first == "instruction" || kv.first == "instructionId" || + kv.first == "locationNumber" || kv.first == "sourceLocation") + { + continue; + } + else if(kv.first == "labels") + { + if(!kv.second.is_array()) + throw deserialization_exceptiont{"labels must be an array"}; + + for(const auto &label : to_json_array(kv.second)) + { + if(!label.is_string()) + throw deserialization_exceptiont{"label must be a string"}; + instruction_it->labels.push_back(label.value); + } + } + else if(kv.first == "targets") + { + if(!kv.second.is_array()) + throw deserialization_exceptiont{"targets must be an array"}; + + for(const auto &target : to_json_array(kv.second)) + { + std::optional target_unsigned = + string2optional_unsigned(target.value); + if(!target.is_number() || !target_unsigned.has_value()) + throw deserialization_exceptiont{ + "target must be an unsigned number"}; + auto target_it = target_map.find(*target_unsigned); + if(target_it == target_map.end()) + throw deserialization_exceptiont{"target not in function"}; + instruction_it->targets.push_back(target_it->second); + } + + if( + !instruction_it->is_incomplete_goto() || + instruction_it->targets.empty()) + { + throw deserialization_exceptiont{ + "goto_program_from_json: invalid targets entry"}; + } + goto_programt::targett target = instruction_it->targets.back(); + instruction_it->targets.pop_back(); + instruction_it->complete_goto(target); + } + else + { + throw deserialization_exceptiont{ + "goto_program_from_json: unexpected key '" + kv.first + "'"}; + } + } + + ++instruction_it; + } + + return program; +} + +goto_functiont goto_function_from_json(const json_objectt &json) +{ + goto_functiont result; + + for(const auto &kv : json) + { + if(kv.first == "instructions") + { + result.body = goto_program_from_json(kv.second); + } + else if(kv.first == "parameterIdentifiers") + { + if(!kv.second.is_array()) + { + throw deserialization_exceptiont{ + "parameterIdentifiers must be an array"}; + } + + for(const auto ¶m : to_json_array(kv.second)) + { + if(!param.is_string()) + { + throw deserialization_exceptiont{ + "parameter identifier must be a string"}; + } + result.parameter_identifiers.push_back(param.value); + } + } + else if(kv.first == "isHidden") + { + if(try_get_bool(kv.second, "isHidden")) + result.make_hidden(); + } + else if(kv.first == "name") + { + // ignored, already processed by goto_functions_from_json + } + else if(kv.first == "isBodyAvailable" || kv.first == "isInternal") + { + // ignored, computed at runtime + } + else + { + throw deserialization_exceptiont{ + "goto_function_from_json: unexpected key '" + kv.first + "'"}; + } + } + + return result; +} diff --git a/src/json-symtab-language/json_goto_function.h b/src/json-symtab-language/json_goto_function.h new file mode 100644 index 00000000000..b2ad1bc3d11 --- /dev/null +++ b/src/json-symtab-language/json_goto_function.h @@ -0,0 +1,24 @@ +/*******************************************************************\ + +Module: JSON goto_function deserialization + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// JSON goto_function deserialization + +#ifndef CPROVER_JSON_SYMTAB_LANGUAGE_JSON_GOTO_FUNCTION_H +#define CPROVER_JSON_SYMTAB_LANGUAGE_JSON_GOTO_FUNCTION_H + +#include + +class json_objectt; + +/// Deserialize a goto_functiont from JSON +/// \param json: The JSON object representing a goto_function +/// \return A goto_functiont +goto_functiont goto_function_from_json(const json_objectt &json); + +#endif // CPROVER_JSON_SYMTAB_LANGUAGE_JSON_GOTO_FUNCTION_H diff --git a/src/json-symtab-language/json_goto_functions.cpp b/src/json-symtab-language/json_goto_functions.cpp new file mode 100644 index 00000000000..8869655cd44 --- /dev/null +++ b/src/json-symtab-language/json_goto_functions.cpp @@ -0,0 +1,72 @@ +/*******************************************************************\ + +Module: JSON goto_functions deserialization + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// JSON goto_functions deserialization + +#include "json_goto_functions.h" + +#include +#include + +#include + +#include "json_goto_function.h" + +void goto_functions_from_json( + const jsont &json, + goto_functionst &goto_functions) +{ + if(!json.is_object()) + { + throw deserialization_exceptiont{ + "goto_functions_from_json: JSON input must be an object"}; + } + + const json_objectt &json_object = to_json_object(json); + const auto it = json_object.find("functions"); + + if(it == json_object.end()) + { + throw deserialization_exceptiont{ + "goto_functions_from_json: JSON object must have key 'functions'"}; + } + + if(!it->second.is_array()) + { + throw deserialization_exceptiont{ + "goto_functions_from_json: JSON functions must be an array"}; + } + + const json_arrayt &json_functions = to_json_array(it->second); + + for(const auto &function : json_functions) + { + if(!function.is_object()) + { + throw deserialization_exceptiont{ + "goto_functions_from_json: JSON function must be an object"}; + } + + const json_objectt &json_function = to_json_object(function); + auto name_it = json_function.find("name"); + + if(name_it == json_function.end() || !name_it->second.is_string()) + { + throw deserialization_exceptiont{ + "goto_functions_from_json: JSON function object must have key 'name' " + "mapping to a string"}; + } + const auto function_name = name_it->second.value; + + goto_functiont goto_function = goto_function_from_json(json_function); + goto_functions.function_map[function_name] = std::move(goto_function); + } + + goto_functions.update(); +} diff --git a/src/json-symtab-language/json_goto_functions.h b/src/json-symtab-language/json_goto_functions.h new file mode 100644 index 00000000000..11155779bc7 --- /dev/null +++ b/src/json-symtab-language/json_goto_functions.h @@ -0,0 +1,25 @@ +/*******************************************************************\ + +Module: JSON goto_functions deserialization + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// JSON goto_functions deserialization + +#ifndef CPROVER_JSON_SYMTAB_LANGUAGE_JSON_GOTO_FUNCTIONS_H +#define CPROVER_JSON_SYMTAB_LANGUAGE_JSON_GOTO_FUNCTIONS_H + +class goto_functionst; +class jsont; + +/// Deserialize goto_functionst from JSON +/// \param json: The JSON object representing goto_functions +/// \param goto_functions: The goto_functionst object to populate +void goto_functions_from_json( + const jsont &json, + goto_functionst &goto_functions); + +#endif // CPROVER_JSON_SYMTAB_LANGUAGE_JSON_GOTO_FUNCTIONS_H diff --git a/src/json-symtab-language/json_symbol.cpp b/src/json-symtab-language/json_symbol.cpp index cd6b0d79bee..e11e8dd9c71 100644 --- a/src/json-symtab-language/json_symbol.cpp +++ b/src/json-symtab-language/json_symbol.cpp @@ -11,34 +11,129 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include #include -#include #include -/// Return string value for a given key if present in the json object. -/// \param in: The json object that is getting fetched as a string. -/// \param key: The key for the json value to be fetched. -/// \return A string value for the corresponding key. -static const std::string & -try_get_string(const jsont &in, const std::string &key) +const std::string &try_get_string(const jsont &in, const std::string &key) { if(!in.is_string()) - throw deserialization_exceptiont( - "symbol_from_json: expected string for key '" + key + "'"); + { + throw deserialization_exceptiont{"expected string for key '" + key + "'"}; + } return in.value; } -/// Return boolean value for a given key if present in the json object. -/// \param in: The json object that is getting fetched as a boolean. -/// \param key: The key for the json value to be fetched. -/// \return A boolean value for the corresponding key. -static bool try_get_bool(const jsont &in, const std::string &key) +bool try_get_bool(const jsont &in, const std::string &key) { if(!(in.is_true() || in.is_false())) - throw deserialization_exceptiont( - "symbol_from_json: expected bool for key '" + key + "'"); + { + throw deserialization_exceptiont{"expected bool for key '" + key + "'"}; + } return in.is_true(); } +source_locationt try_get_source_location(const jsont &json) +{ + if(!json.is_object()) + { + throw deserialization_exceptiont{ + "source location should be encoded as an object"}; + } + + const json_objectt &json_object = to_json_object(json); + + if(json_object.size() == 0) + { + return source_locationt::nil(); + } + else if(json_object.find("id") != json_object.end()) + { + json_irept json2irep{true}; + irept irep = json2irep.convert_from_json(json_object); + return static_cast(irep); + } + + source_locationt result; + for(const auto &kv : json_object) + { + if(kv.first == "workingDirectory") + { + result.set_working_directory( + try_get_string(kv.second, "workingDirectory")); + } + else if(kv.first == "file") + { + result.set_file(try_get_string(kv.second, "file")); + } + else if(kv.first == "line") + { + result.set_line(try_get_string(kv.second, "line")); + } + else if(kv.first == "column") + { + result.set_column(try_get_string(kv.second, "column")); + } + else if(kv.first == "function") + { + result.set_function(try_get_string(kv.second, "function")); + } + else if(kv.first == "bytecodeIndex") + { + result.set_java_bytecode_index( + try_get_string(kv.second, "bytecodeIndex")); + } + else if(kv.first == "propertyId") + { + result.set_property_id(try_get_string(kv.second, "propertyId")); + } + else if(kv.first == "propertyClass") + { + result.set_property_class(try_get_string(kv.second, "propertyClass")); + } + else if(kv.first == "comment") + { + result.set_comment(try_get_string(kv.second, "comment")); + } + else if(kv.first == "caseNumber") + { + result.set_case_number(try_get_string(kv.second, "caseNumber")); + } + else if(kv.first == "basicBlockSourceLines") + { + json_irept json2irep{true}; + irept irep = json2irep.convert_from_json(kv.second); + result.set_basic_block_source_lines(irep); + } + else if(kv.first == "propertyFatal") + { + result.property_fatal(try_get_bool(kv.second, "propertyFatal")); + } + else if(kv.first == "hide") + { + if(try_get_bool(kv.second, "hide")) + result.set_hide(); + } + else if(kv.first == "pragma") + { + if(!kv.second.is_array()) + throw deserialization_exceptiont{"pragmas must be an array"}; + + for(const auto &pragma : to_json_array(kv.second)) + { + if(!pragma.is_string()) + throw deserialization_exceptiont{"pragma must be a string"}; + result.add_pragma(pragma.value); + } + } + else + { + throw deserialization_exceptiont{ + "try_get_source_location: unexpected key '" + kv.first + "'"}; + } + } + + return result; +} + /// Deserialise a json object to a symbolt. /// \param in: The json object that is getting fetched as an object. /// \return A symbolt representing the json object. @@ -61,10 +156,7 @@ symbolt symbol_from_json(const jsont &in) result.value = static_cast(irep); } else if(kv.first == "location") - { - irept irep = json2irep.convert_from_json(kv.second); - result.location = static_cast(irep); - } + result.location = try_get_source_location(kv.second); else if(kv.first == "name") result.name = try_get_string(kv.second, "name"); else if(kv.first == "module") diff --git a/src/json-symtab-language/json_symbol.h b/src/json-symtab-language/json_symbol.h index 356e9575df3..b68177d5460 100644 --- a/src/json-symtab-language/json_symbol.h +++ b/src/json-symtab-language/json_symbol.h @@ -15,4 +15,21 @@ class jsont; symbolt symbol_from_json(const jsont &); +/// Return string value for a given key if present in the json object. +/// \param in: The json object that is getting fetched as a string. +/// \param key: The key for the json value to be fetched. +/// \return A string value for the corresponding key. +const std::string &try_get_string(const jsont &in, const std::string &key); + +/// Return boolean value for a given key if present in the json object. +/// \param in: The json object that is getting fetched as a boolean. +/// \param key: The key for the json value to be fetched. +/// \return A boolean value for the corresponding key. +bool try_get_bool(const jsont &in, const std::string &key); + +/// Return a `source_locationt` from the given JSON object. +/// \param json: The json object that represents a source location. +/// \return A source location, unless an exception was thrown before. +source_locationt try_get_source_location(const jsont &json); + #endif diff --git a/src/symtab2gb/module_dependencies.txt b/src/symtab2gb/module_dependencies.txt index 0b0b11dd35c..955fdd316d0 100644 --- a/src/symtab2gb/module_dependencies.txt +++ b/src/symtab2gb/module_dependencies.txt @@ -1,4 +1,5 @@ util +json json-symtab-language langapi goto-programs diff --git a/src/symtab2gb/symtab2gb_parse_options.cpp b/src/symtab2gb/symtab2gb_parse_options.cpp index 58f87fa9dda..b6a61f5b1bb 100644 --- a/src/symtab2gb/symtab2gb_parse_options.cpp +++ b/src/symtab2gb/symtab2gb_parse_options.cpp @@ -12,6 +12,7 @@ Author: Diffblue Ltd. #include #include #include +#include #include #include @@ -19,7 +20,9 @@ Author: Diffblue Ltd. #include #include +#include #include +#include #include #include @@ -43,6 +46,7 @@ static inline bool failed(bool error_indicator) static void run_symtab2gb( const std::vector &symtab_filenames, const std::string &gb_filename, + const std::string &goto_functions_filename_or_empty, const std::string &cmdline_verbosity) { // try opening all the files first to make sure we can @@ -64,6 +68,19 @@ static void run_symtab2gb( symtab_files.emplace_back(std::move(symtab_file)); } + // Open goto functions file if specified + std::optional goto_functions_file; + if(!goto_functions_filename_or_empty.empty()) + { + goto_functions_file = std::ifstream{goto_functions_filename_or_empty}; + if(!goto_functions_file->is_open()) + { + throw system_exceptiont{ + "couldn't open goto functions file '" + + goto_functions_filename_or_empty + "'"}; + } + } + stream_message_handlert message_handler{std::cerr}; messaget::eval_verbosity( cmdline_verbosity, messaget::M_STATUS, message_handler); @@ -103,6 +120,26 @@ static void run_symtab2gb( goto_modelt linked_goto_model; linked_goto_model.symbol_table.swap(linked_symbol_table); + + // If goto functions file is specified, parse it and use those functions + if(goto_functions_file.has_value()) + { + jsont json; + if(failed(parse_json( + *goto_functions_file, + goto_functions_filename_or_empty, + message_handler, + json))) + { + source_locationt source_location; + source_location.set_file(goto_functions_filename_or_empty); + throw invalid_source_file_exceptiont{ + "failed to parse JSON", source_location}; + } + goto_functions_from_json(json, linked_goto_model.goto_functions); + } + + // Convert symbols to goto functions goto_convert(linked_goto_model, message_handler); if(failed(write_goto_binary(out_file, linked_goto_model))) @@ -138,9 +175,17 @@ int symtab2gb_parse_optionst::doit() { gb_filename = cmdline.get_value(SYMTAB2GB_OUT_FILE_OPT); } + + std::string goto_functions_filename_or_empty = + cmdline.get_value(SYMTAB2GB_GOTO_FUNCTIONS_OPT); + register_languages(); config.set(cmdline); - run_symtab2gb(symtab_filenames, gb_filename, cmdline.get_value("verbosity")); + run_symtab2gb( + symtab_filenames, + gb_filename, + goto_functions_filename_or_empty, + cmdline.get_value("verbosity")); return CPROVER_EXIT_SUCCESS; } @@ -163,6 +208,8 @@ void symtab2gb_parse_optionst::help() "Options:\n" " {y--out} {uoutfile} \t specify the filename of the resulting binary" " (default: a.out)\n" + " {y--goto-functions} {ufile} \t specify a file containing JSON-encoded" + " goto functions\n" " {y--verbosity} {u#} \t verbosity level\n"); log.status() << messaget::eom; } diff --git a/src/symtab2gb/symtab2gb_parse_options.h b/src/symtab2gb/symtab2gb_parse_options.h index 61f482460c4..a97aa054c58 100644 --- a/src/symtab2gb/symtab2gb_parse_options.h +++ b/src/symtab2gb/symtab2gb_parse_options.h @@ -12,11 +12,13 @@ Author: Diffblue Ltd. #include #define SYMTAB2GB_OUT_FILE_OPT "out" +#define SYMTAB2GB_GOTO_FUNCTIONS_OPT "goto-functions" // clang-format off #define SYMTAB2GB_OPTIONS \ "(" SYMTAB2GB_OUT_FILE_OPT "):" \ + "(" SYMTAB2GB_GOTO_FUNCTIONS_OPT "):" \ "(verbosity):" \ // end options diff --git a/src/util/json_irep.cpp b/src/util/json_irep.cpp index 9bbef4200af..2fc56264a7b 100644 --- a/src/util/json_irep.cpp +++ b/src/util/json_irep.cpp @@ -158,5 +158,39 @@ json_objectt json(const source_locationt &location) if(!location.get_java_bytecode_index().empty()) result["bytecodeIndex"] = json_stringt(location.get_java_bytecode_index()); + if(!location.get_property_id().empty()) + result["propertyId"] = json_stringt{location.get_property_id()}; + + if(!location.get_property_class().empty()) + result["propertyClass"] = json_stringt{location.get_property_class()}; + + if(!location.get_comment().empty()) + result["comment"] = json_stringt{location.get_comment()}; + + if(!location.get_case_number().empty()) + result["caseNumber"] = json_stringt{location.get_case_number()}; + + if(location.get_basic_block_source_lines().is_not_nil()) + { + result["basicBlockSourceLines"] = json_irept{true}.convert_from_irep( + location.get_basic_block_source_lines()); + } + + if(location.property_fatal()) + result["propertyFatal"] = jsont::json_boolean(true); + + if(location.get_hide()) + result["hide"] = jsont::json_boolean(true); + + const auto &pragmas = location.get_pragmas(); + if(!pragmas.empty()) + { + auto json_pragma_range = make_range(pragmas.begin(), pragmas.end()) + .map([](const std::pair &entry) + { return json_stringt{entry.first}; }); + result["pragma"] = + json_arrayt{json_pragma_range.begin(), json_pragma_range.end()}; + } + return result; } diff --git a/src/util/parser.h b/src/util/parser.h index 43d2c853d22..eeec3b469a0 100644 --- a/src/util/parser.h +++ b/src/util/parser.h @@ -135,6 +135,11 @@ class parsert _source_location.set_function(function); } + void clear_function() + { + _source_location.clear_function(); + } + void advance_column(unsigned token_width) { column+=token_width; diff --git a/src/util/source_location.h b/src/util/source_location.h index 1f4373f14f9..d2dc44f6d7b 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -134,9 +134,15 @@ class source_locationt:public irept DEPRECATED(SINCE(2022, 10, 13, "use identifier of containing function")) void set_function(const irep_idt &function) { + PRECONDITION(!function.empty()); set(ID_function, function); } + void clear_function() + { + remove(ID_function); + } + void set_property_id(const irep_idt &property_id) { set(ID_property_id, property_id); diff --git a/unit/Makefile b/unit/Makefile index bc93e74a34c..a708a86b214 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -90,6 +90,11 @@ SRC += analyses/ai/ai.cpp \ goto-symex/symex_level1.cpp \ goto-symex/try_evaluate_pointer_comparisons.cpp \ interpreter/interpreter.cpp \ + json-symtab-language/json_goto_function.cpp \ + json-symtab-language/json_goto_function_extended.cpp \ + json-symtab-language/json_goto_functions.cpp \ + json-symtab-language/json_goto_functions_extended.cpp \ + json-symtab-language/json_malformed_input.cpp \ json/json_parser.cpp \ json_symbol_table.cpp \ path_strategies.cpp \ diff --git a/unit/json-symtab-language/json_goto_function.cpp b/unit/json-symtab-language/json_goto_function.cpp new file mode 100644 index 00000000000..b4b8f1b2974 --- /dev/null +++ b/unit/json-symtab-language/json_goto_function.cpp @@ -0,0 +1,46 @@ +/*******************************************************************\ + +Module: Unit tests for json_goto_function + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Unit tests for json_goto_function + +#include + +#include +#include + +TEST_CASE( + "JSON goto function without body", + "[core][json-symtab-language][json_goto_function]") +{ + // Create a simple JSON representation of a goto_function + json_objectt json_function; + + // Add is_hidden field + json_function["isHidden"] = jsont::json_boolean(true); + + // Add parameter_identifiers field + json_arrayt param_ids; + param_ids.push_back(json_stringt{"param1"}); + param_ids.push_back(json_stringt{"param2"}); + json_function["parameterIdentifiers"] = param_ids; + + // Add body field with empty instructions + json_arrayt instructions; + json_function["instructions"] = instructions; + + // Convert JSON to goto_function + goto_functiont function = goto_function_from_json(json_function); + + // Check that the function was parsed correctly + REQUIRE(function.is_hidden()); + REQUIRE(function.parameter_identifiers.size() == 2); + REQUIRE(function.parameter_identifiers[0] == "param1"); + REQUIRE(function.parameter_identifiers[1] == "param2"); + REQUIRE(!function.body_available()); +} diff --git a/unit/json-symtab-language/json_goto_function_extended.cpp b/unit/json-symtab-language/json_goto_function_extended.cpp new file mode 100644 index 00000000000..ea248020326 --- /dev/null +++ b/unit/json-symtab-language/json_goto_function_extended.cpp @@ -0,0 +1,331 @@ +/*******************************************************************\ + +Module: Extended unit tests for json_goto_function + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Extended unit tests for json_goto_function including error handling + +#include +#include +#include + +#include +#include + +TEST_CASE( + "JSON goto function without body (extended)", + "[core][json-symtab-language][json_goto_function]") +{ + // Create a JSON representation of a goto_function with instructions + json_objectt json_function; + + // Add parameter_identifiers field + json_arrayt param_ids; + param_ids.push_back(json_stringt{"param1"}); + param_ids.push_back(json_stringt{"param2"}); + json_function["parameterIdentifiers"] = param_ids; + + // Add body field with instructions + json_arrayt instructions; + + // Add a SKIP instruction + json_objectt skip_instruction; + skip_instruction["instructionId"] = json_stringt{"SKIP"}; + skip_instruction["locationNumber"] = json_numbert{"1"}; + + // Add a source location + json_objectt location; + location["file"] = json_stringt{"test.c"}; + location["line"] = json_stringt{"10"}; + location["column"] = json_stringt{"5"}; + skip_instruction["sourceLocation"] = location; + + // Add labels + json_arrayt labels; + labels.push_back(json_stringt{"label1"}); + labels.push_back(json_stringt{"label2"}); + skip_instruction["labels"] = labels; + + instructions.push_back(skip_instruction); + + // Add an END_FUNCTION instruction + json_objectt end_function_instruction; + end_function_instruction["instructionId"] = json_stringt{"END_FUNCTION"}; + end_function_instruction["locationNumber"] = json_numbert{"2"}; + + instructions.push_back(end_function_instruction); + + json_function["instructions"] = instructions; + + // Convert JSON to goto_function + goto_functiont function = goto_function_from_json(json_function); + + // Check that the function was parsed correctly + REQUIRE(function.parameter_identifiers.size() == 2); + REQUIRE(function.parameter_identifiers[0] == "param1"); + REQUIRE(function.parameter_identifiers[1] == "param2"); + REQUIRE(function.body.instructions.size() == 2); + + // Check the first instruction + auto it = function.body.instructions.begin(); + REQUIRE(it->is_skip()); + REQUIRE(it->source_location().get_file() == "test.c"); + REQUIRE(it->source_location().get_line() == "10"); + REQUIRE(it->labels.size() == 2); + REQUIRE(it->labels.front() == "label1"); + REQUIRE(it->labels.back() == "label2"); + + // Check the second instruction + ++it; + REQUIRE(it->is_end_function()); +} + +TEST_CASE( + "JSON goto function (non-trivial)", + "[core][json-symtab-language][json_goto_function]") +{ + // Create a JSON representation of a goto_function with instructions and + // targets + json_objectt json_function; + + // Add body field with instructions + json_arrayt instructions; + + // Add a GOTO instruction with a target + json_objectt goto_instruction; + goto_instruction["instructionId"] = json_stringt{"GOTO"}; + goto_instruction["guard"] = json_irept{true}.convert_from_irep(true_exprt{}); + goto_instruction["locationNumber"] = json_numbert{"0"}; + + // Add targets array pointing to the second instruction + json_arrayt targets; + targets.push_back(json_numbert{"1"}); + goto_instruction["targets"] = targets; + + instructions.push_back(goto_instruction); + + // Add a SKIP instruction as the target + json_objectt skip_instruction; + skip_instruction["instructionId"] = json_stringt{"SKIP"}; + skip_instruction["locationNumber"] = json_numbert{"1"}; + instructions.push_back(skip_instruction); + + // Add an END_FUNCTION instruction + json_objectt end_function_instruction; + end_function_instruction["instructionId"] = json_stringt{"END_FUNCTION"}; + end_function_instruction["locationNumber"] = json_numbert{"2"}; + instructions.push_back(end_function_instruction); + + json_function["instructions"] = instructions; + + // Convert JSON to goto_function + goto_functiont function = goto_function_from_json(json_function); + + // Check that the function was parsed correctly + REQUIRE(function.body.instructions.size() == 3); + + // Check the first instruction and its target + auto it = function.body.instructions.begin(); + REQUIRE(it->is_goto()); + REQUIRE(it->targets.size() == 1); + + // The target should be the second instruction + auto target_it = it->targets.front(); + REQUIRE(target_it->is_skip()); +} + +TEST_CASE( + "JSON goto function (non-trivial 2)", + "[core][json-symtab-language][json_goto_function]") +{ + // Create a JSON representation of a goto_function with code and guard + json_objectt json_function; + + // Add body field with instructions + json_arrayt instructions; + + // Add an ASSIGN instruction with code + json_objectt assign_instruction; + assign_instruction["instructionId"] = json_stringt{"ASSIGN"}; + assign_instruction["locationNumber"] = json_numbert{"1"}; + + // Create a simple assignment code: x = 42 + json_objectt code; + code["id"] = json_stringt{"code"}; + code["namedSub"] = + json_objectt{{"statement", json_objectt{{"id", json_stringt{"assign"}}}}}; + + json_objectt lhs; + lhs["id"] = json_stringt{"symbol"}; + lhs["namedSub"] = + json_objectt{{"identifier", json_objectt{{"id", json_stringt{"x"}}}}}; + + json_objectt rhs; + rhs["id"] = json_stringt{"constant"}; + rhs["namedSub"] = + json_objectt{{"value", json_objectt{{"id", json_stringt{"42"}}}}}; + + code["sub"] = json_arrayt{{lhs, rhs}}; + + assign_instruction["code"] = code; + + // Add an ASSUME instruction with guard + json_objectt assume_instruction; + assume_instruction["instructionId"] = json_stringt{"ASSUME"}; + assume_instruction["locationNumber"] = json_numbert{"2"}; + + // Create a simple guard: x > 0 + json_objectt guard; + guard["id"] = json_stringt{">"}; + + json_objectt op0; + op0["id"] = json_stringt{"symbol"}; + op0["namedSub"] = + json_objectt{{"identifier", json_objectt{{"id", json_stringt{"x"}}}}}; + + json_objectt op1; + op1["id"] = json_stringt{"constant"}; + op1["namedSub"] = + json_objectt{{"value", json_objectt{{"id", json_stringt{"0"}}}}}; + + guard["sub"] = json_arrayt{{op0, op1}}; + + assume_instruction["guard"] = guard; + + instructions.push_back(assign_instruction); + instructions.push_back(assume_instruction); + + json_function["instructions"] = instructions; + + // Convert JSON to goto_function + goto_functiont function = goto_function_from_json(json_function); + + // Check that the function was parsed correctly + REQUIRE(function.body.instructions.size() == 2); + + // Check the first instruction (ASSIGN) + auto it = function.body.instructions.begin(); + REQUIRE(it->is_assign()); + REQUIRE(it->code().id() == ID_code); + + // Check the second instruction (ASSUME) + ++it; + REQUIRE(it->is_assume()); + REQUIRE(it->condition().id() == ID_gt); +} + +TEST_CASE( + "JSON goto function error handling", + "[core][json-symtab-language][json_goto_function]") +{ + SECTION("Invalid parameter_identifiers type") + { + json_objectt json_function; + json_function["parameter_identifiers"] = json_stringt{"not an array"}; + + REQUIRE_THROWS_AS( + goto_function_from_json(json_function), deserialization_exceptiont); + } + + SECTION("Invalid parameter identifier type") + { + json_objectt json_function; + json_arrayt param_ids; + param_ids.push_back(json_numbert{"123"}); // Should be a string + json_function["parameter_identifiers"] = param_ids; + + REQUIRE_THROWS_AS( + goto_function_from_json(json_function), deserialization_exceptiont); + } + + SECTION("Invalid is_hidden type") + { + json_objectt json_function; + json_function["isHidden"] = json_stringt{"not a boolean"}; + + REQUIRE_THROWS_AS( + goto_function_from_json(json_function), deserialization_exceptiont); + } + + SECTION("Invalid instruction type") + { + json_objectt json_function; + json_arrayt instructions; + + json_objectt instruction; + instruction["instructionId"] = json_numbert{"123"}; // Should be a string + + instructions.push_back(instruction); + json_function["instructions"] = instructions; + + REQUIRE_THROWS_AS( + goto_function_from_json(json_function), deserialization_exceptiont); + } + + SECTION("Invalid targets type") + { + json_objectt json_function; + json_arrayt instructions; + + json_objectt instruction; + instruction["instructionId"] = json_stringt{"GOTO"}; + instruction["targets"] = json_stringt{"not an array"}; + + instructions.push_back(instruction); + json_function["instructions"] = instructions; + + REQUIRE_THROWS_AS( + goto_function_from_json(json_function), deserialization_exceptiont); + } + + SECTION("Invalid target index type") + { + json_objectt json_function; + json_arrayt instructions; + + json_objectt instruction; + instruction["instructionId"] = json_stringt{"GOTO"}; + + json_arrayt targets; + targets.push_back(json_stringt{"not a number"}); + instruction["targets"] = targets; + + instructions.push_back(instruction); + json_function["instructions"] = instructions; + + REQUIRE_THROWS_AS( + goto_function_from_json(json_function), deserialization_exceptiont); + } + + SECTION("Target index out of bounds") + { + json_objectt json_function; + json_arrayt instructions; + + json_objectt instruction; + instruction["instructionId"] = json_stringt{"GOTO"}; + + json_arrayt targets; + targets.push_back(json_numbert{"999"}); // Out of bounds + instruction["targets"] = targets; + + instructions.push_back(instruction); + json_function["instructions"] = instructions; + + REQUIRE_THROWS_AS( + goto_function_from_json(json_function), deserialization_exceptiont); + } + + SECTION("Unexpected key") + { + json_objectt json_function; + json_function["unexpected_key"] = json_stringt{"value"}; + + REQUIRE_THROWS_AS( + goto_function_from_json(json_function), deserialization_exceptiont); + } +} diff --git a/unit/json-symtab-language/json_goto_functions.cpp b/unit/json-symtab-language/json_goto_functions.cpp new file mode 100644 index 00000000000..ade91bd33d1 --- /dev/null +++ b/unit/json-symtab-language/json_goto_functions.cpp @@ -0,0 +1,63 @@ +/*******************************************************************\ + +Module: Unit tests for json_goto_functions + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Unit tests for json_goto_functions + +#include + +#include +#include + +#include + +TEST_CASE( + "JSON goto functions without body", + "[core][json-symtab-language][json_goto_functions]") +{ + // Create a simple JSON representation of goto_functions + json_objectt json_goto_functions; + json_arrayt functions; + + // Create a simple function + json_objectt json_function; + json_function["isHidden"] = jsont::json_boolean(false); + + // Add parameter_identifiers field + json_arrayt param_ids; + param_ids.push_back(json_stringt{"param1"}); + json_function["parameterIdentifiers"] = param_ids; + + // Add body field with empty instructions + json_arrayt instructions; + json_function["instructions"] = instructions; + + // Add the function to the functions object + json_function["name"] = json_stringt{"test_function"}; + functions.push_back(json_function); + + // Add the functions object to the goto_functions object + json_goto_functions["functions"] = functions; + + // Convert JSON to goto_functions + goto_functionst goto_functions; + goto_functions_from_json(json_goto_functions, goto_functions); + + // Check that the functions were parsed correctly + REQUIRE(goto_functions.function_map.size() == 1); + REQUIRE( + goto_functions.function_map.find("test_function") != + goto_functions.function_map.end()); + + const goto_functiont &function = + goto_functions.function_map.at("test_function"); + REQUIRE(!function.is_hidden()); + REQUIRE(function.parameter_identifiers.size() == 1); + REQUIRE(function.parameter_identifiers[0] == "param1"); + REQUIRE(function.body.instructions.empty()); +} diff --git a/unit/json-symtab-language/json_goto_functions_extended.cpp b/unit/json-symtab-language/json_goto_functions_extended.cpp new file mode 100644 index 00000000000..a0ff936b998 --- /dev/null +++ b/unit/json-symtab-language/json_goto_functions_extended.cpp @@ -0,0 +1,264 @@ +/*******************************************************************\ + +Module: Extended unit tests for json_goto_functions + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Extended unit tests for json_goto_functions including error handling + +#include +#include +#include + +#include +#include + +#include + +TEST_CASE( + "JSON goto functions without body (extended)", + "[core][json-symtab-language][json_goto_functions]") +{ + // Create a JSON representation of goto_functions with multiple functions + json_objectt json_goto_functions; + json_arrayt functions; + + // Create first function + json_objectt json_function1; + json_function1["isHidden"] = jsont::json_boolean(false); + + // Add parameter_identifiers field + json_arrayt param_ids1; + param_ids1.push_back(json_stringt{"param1"}); + json_function1["parameterIdentifiers"] = param_ids1; + + // Add body field with empty instructions + json_arrayt instructions1; + json_function1["instructions"] = instructions1; + + // Create second function + json_objectt json_function2; + json_function2["isHidden"] = jsont::json_boolean(true); + + // Add parameter_identifiers field + json_arrayt param_ids2; + param_ids2.push_back(json_stringt{"param1"}); + param_ids2.push_back(json_stringt{"param2"}); + json_function2["parameterIdentifiers"] = param_ids2; + + // Add body field with instructions + json_arrayt instructions2; + + // Add a SKIP instruction + json_objectt skip_instruction; + skip_instruction["instructionId"] = json_stringt{"SKIP"}; + skip_instruction["locationNumber"] = json_numbert{"1"}; + instructions2.push_back(skip_instruction); + + json_function2["instructions"] = instructions2; + + // Add the functions to the functions object + json_function1["name"] = json_stringt{"function1"}; + functions.push_back(json_function1); + json_function2["name"] = json_stringt{"function2"}; + functions.push_back(json_function2); + + // Add the functions object to the goto_functions object + json_goto_functions["functions"] = functions; + + // Convert JSON to goto_functions + goto_functionst goto_functions; + goto_functions_from_json(json_goto_functions, goto_functions); + + // Check that the functions were parsed correctly + REQUIRE(goto_functions.function_map.size() == 2); + REQUIRE( + goto_functions.function_map.find("function1") != + goto_functions.function_map.end()); + REQUIRE( + goto_functions.function_map.find("function2") != + goto_functions.function_map.end()); + + // Check function1 + const goto_functiont &function1 = goto_functions.function_map.at("function1"); + REQUIRE(!function1.is_hidden()); + REQUIRE(function1.parameter_identifiers.size() == 1); + REQUIRE(function1.parameter_identifiers[0] == "param1"); + REQUIRE(function1.body.instructions.empty()); + + // Check function2 + const goto_functiont &function2 = goto_functions.function_map.at("function2"); + REQUIRE(function2.is_hidden()); + REQUIRE(function2.parameter_identifiers.size() == 2); + REQUIRE(function2.parameter_identifiers[0] == "param1"); + REQUIRE(function2.parameter_identifiers[1] == "param2"); + REQUIRE(function2.body.instructions.size() == 1); + REQUIRE(function2.body.instructions.front().is_skip()); +} + +TEST_CASE( + "JSON goto functions error handling", + "[core][json-symtab-language][json_goto_functions]") +{ + SECTION("Non-object input") + { + jsont json_string = json_stringt{"not an object"}; + goto_functionst goto_functions; + + REQUIRE_THROWS_AS( + goto_functions_from_json(json_string, goto_functions), + deserialization_exceptiont); + } + + SECTION("Missing functions key") + { + json_objectt json_goto_functions; + // No "functions" key + + goto_functionst goto_functions; + REQUIRE_THROWS_AS( + goto_functions_from_json(json_goto_functions, goto_functions), + deserialization_exceptiont); + } + + SECTION("Invalid functions type") + { + json_objectt json_goto_functions; + json_goto_functions["functions"] = json_stringt{"not an object"}; + + goto_functionst goto_functions; + REQUIRE_THROWS_AS( + goto_functions_from_json(json_goto_functions, goto_functions), + deserialization_exceptiont); + } + + SECTION("Invalid function object") + { + json_objectt json_goto_functions; + json_arrayt functions; + + // Add an invalid function (string instead of object) + functions.push_back(json_stringt{"not an object"}); + + json_goto_functions["functions"] = functions; + + goto_functionst goto_functions; + REQUIRE_THROWS_AS( + goto_functions_from_json(json_goto_functions, goto_functions), + deserialization_exceptiont); + } + + SECTION("Function with invalid parameter_identifiers") + { + json_objectt json_goto_functions; + json_arrayt functions; + + json_objectt json_function; + json_function["parameterIdentifiers"] = json_stringt{"not an array"}; + + json_function["name"] = json_stringt{"invalid_function"}; + functions.push_back(json_function); + json_goto_functions["functions"] = functions; + + goto_functionst goto_functions; + REQUIRE_THROWS_AS( + goto_functions_from_json(json_goto_functions, goto_functions), + deserialization_exceptiont); + } +} + +TEST_CASE( + "JSON goto functions with non-trivial structure", + "[core][json-symtab-language][json_goto_functions]") +{ + // Create a JSON representation of goto_functions with a complex function + json_objectt json_goto_functions; + json_arrayt functions; + + // Create a function with a more complex structure + json_objectt json_function; + + // Add body field with instructions + json_arrayt instructions; + + // Add a GOTO instruction with a target + json_objectt goto_instruction; + goto_instruction["instructionId"] = json_stringt{"GOTO"}; + goto_instruction["guard"] = json_irept{true}.convert_from_irep(true_exprt{}); + goto_instruction["locationNumber"] = json_numbert{"1"}; + + // Add targets array pointing to the second instruction + json_arrayt targets; + targets.push_back(json_numbert{"2"}); + goto_instruction["targets"] = targets; + + // Add a source location + json_objectt goto_location; + goto_location["file"] = json_stringt{"test.c"}; + goto_location["line"] = json_stringt{"10"}; + goto_instruction["sourceLocation"] = goto_location; + + instructions.push_back(goto_instruction); + + // Add a SKIP instruction as the target + json_objectt skip_instruction; + skip_instruction["instructionId"] = json_stringt{"SKIP"}; + skip_instruction["locationNumber"] = json_numbert{"2"}; + + // Add a source location + json_objectt skip_location; + skip_location["file"] = json_stringt{"test.c"}; + skip_location["line"] = json_stringt{"11"}; + skip_instruction["sourceLocation"] = skip_location; + + instructions.push_back(skip_instruction); + + // Add an END_FUNCTION instruction + json_objectt end_function_instruction; + end_function_instruction["instructionId"] = json_stringt{"END_FUNCTION"}; + end_function_instruction["locationNumber"] = json_numbert{"3"}; + instructions.push_back(end_function_instruction); + + json_function["instructions"] = instructions; + + // Add the function to the functions object + json_function["name"] = json_stringt{"complex_function"}; + functions.push_back(json_function); + + // Add the functions object to the goto_functions object + json_goto_functions["functions"] = functions; + + // Convert JSON to goto_functions + goto_functionst goto_functions; + goto_functions_from_json(json_goto_functions, goto_functions); + + // Check that the function was parsed correctly + REQUIRE(goto_functions.function_map.size() == 1); + REQUIRE( + goto_functions.function_map.find("complex_function") != + goto_functions.function_map.end()); + + const goto_functiont &function = + goto_functions.function_map.at("complex_function"); + REQUIRE(function.body.instructions.size() == 3); + + // Check the first instruction and its target + auto it = function.body.instructions.begin(); + REQUIRE(it->is_goto()); + REQUIRE(it->source_location().get_file() == "test.c"); + REQUIRE(it->source_location().get_line() == "10"); + REQUIRE(it->targets.size() == 1); + + // The target should be the second instruction + auto target_it = it->targets.front(); + REQUIRE(target_it->is_skip()); + REQUIRE(target_it->source_location().get_file() == "test.c"); + REQUIRE(target_it->source_location().get_line() == "11"); + + // Check that the location numbers, target numbers, etc. were computed + REQUIRE(!function.body.instructions.begin()->is_target()); + REQUIRE(std::next(function.body.instructions.begin())->is_target()); +} diff --git a/unit/json-symtab-language/json_malformed_input.cpp b/unit/json-symtab-language/json_malformed_input.cpp new file mode 100644 index 00000000000..9a0fcc1d366 --- /dev/null +++ b/unit/json-symtab-language/json_malformed_input.cpp @@ -0,0 +1,279 @@ +/*******************************************************************\ + +Module: Unit tests for handling malformed JSON input + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Unit tests for handling malformed JSON input + +#include +#include + +#include +#include +#include +#include +#include +#include +#include + +#include + +TEST_CASE( + "Malformed JSON input for goto_function", + "[core][json-symtab-language][json_goto_function]") +{ + SECTION("Malformed JSON - syntax error") + { + // This is not valid JSON (missing closing brace) + std::string malformed_json = R"({ + "body": { + "instructions": [ + { + "instructionId": "SKIP" + } + ] + } + )"; + + // Try to parse the malformed JSON + jsont json; + std::istringstream stream(malformed_json); + // This should fail, i.e., return true + REQUIRE(parse_json(stream, "", null_message_handler, json) == true); + } + + SECTION("Malformed JSON - semantic errors") + { + // Test 1: Missing required field 'type' in instruction + json_objectt json_function; + json_arrayt instructions; + + // Create an instruction without a type field + json_objectt instruction_without_type; + // No "instructionId" field + + instructions.push_back(instruction_without_type); + json_function["instructions"] = instructions; + + REQUIRE_THROWS_AS( + goto_function_from_json(json_function), deserialization_exceptiont); + + // Test 2: Invalid instruction type value + json_objectt json_function2; + json_arrayt instructions2; + + json_objectt instruction_invalid_type; + instruction_invalid_type["instructionId"] = json_stringt{"INVALID_TYPE"}; + instruction_invalid_type["locationNumber"] = json_numbert{"1"}; + + instructions2.push_back(instruction_invalid_type); + json_function2["instructions"] = instructions2; + + // This should throw as unknown instruction types are not valid + REQUIRE_THROWS_AS( + goto_function_from_json(json_function2), deserialization_exceptiont); + + // Test 3: Invalid target index (negative) + json_objectt json_function3; + json_arrayt instructions3; + + json_objectt instruction_negative_target; + instruction_negative_target["instructionId"] = json_stringt{"GOTO"}; + instruction_negative_target["locationNumber"] = json_numbert{"1"}; + + json_arrayt targets; + targets.push_back(json_numbert{"-1"}); // Negative index + instruction_negative_target["targets"] = targets; + + instructions3.push_back(instruction_negative_target); + json_function3["instructions"] = instructions3; + + // This should throw as negative indices are not valid + REQUIRE_THROWS_AS( + goto_function_from_json(json_function3), deserialization_exceptiont); + + // Test 4: Target index out of bounds + json_objectt json_function4; + json_arrayt instructions4; + + json_objectt instruction_oob_target; + instruction_oob_target["instructionId"] = json_stringt{"GOTO"}; + instruction_oob_target["locationNumber"] = json_numbert{"1"}; + + json_arrayt targets4; + targets4.push_back(json_numbert{"999"}); // Out of bounds + instruction_oob_target["targets"] = targets4; + + instructions4.push_back(instruction_oob_target); + json_function4["instructions"] = instructions4; + + // This should throw as the target index is out of bounds + REQUIRE_THROWS_AS( + goto_function_from_json(json_function4), deserialization_exceptiont); + } +} + +TEST_CASE( + "Malformed JSON input for goto_functions", + "[core][json-symtab-language][json_goto_functions]") +{ + SECTION("Missing required fields") + { + // Test 1: Missing 'functions' field + json_objectt json_goto_functions; + // No "functions" field + + goto_functionst goto_functions; + REQUIRE_THROWS_AS( + goto_functions_from_json(json_goto_functions, goto_functions), + deserialization_exceptiont); + + // Test 2: 'functions' field is not an object + json_objectt json_goto_functions2; + json_goto_functions2["functions"] = json_stringt{"not an object"}; + + goto_functionst goto_functions2; + REQUIRE_THROWS_AS( + goto_functions_from_json(json_goto_functions2, goto_functions2), + deserialization_exceptiont); + } + + SECTION("Invalid function objects") + { + // Test 1: Function is not an object + json_objectt json_goto_functions; + json_objectt functions; + + functions["invalid_function"] = json_stringt{"not an object"}; + json_goto_functions["functions"] = functions; + + goto_functionst goto_functions; + REQUIRE_THROWS_AS( + goto_functions_from_json(json_goto_functions, goto_functions), + deserialization_exceptiont); + + // Test 2: Function with invalid body + json_objectt json_goto_functions2; + json_objectt functions2; + + json_objectt invalid_function; + invalid_function["instructions"] = json_stringt{"not an object"}; + + functions2["invalid_function"] = invalid_function; + json_goto_functions2["functions"] = functions2; + + goto_functionst goto_functions2; + REQUIRE_THROWS_AS( + goto_functions_from_json(json_goto_functions2, goto_functions2), + deserialization_exceptiont); + } + + SECTION("Deeply nested errors") + { + // Create a JSON structure with an error deep in the hierarchy + json_objectt json_goto_functions; + json_arrayt functions; + + json_objectt function; + json_arrayt instructions; + + // First instruction is valid + json_objectt valid_instruction; + valid_instruction["instructionId"] = json_stringt{"SKIP"}; + valid_instruction["locationNumber"] = json_numbert{"1"}; + instructions.push_back(valid_instruction); + + // Second instruction has an invalid guard + json_objectt invalid_instruction; + invalid_instruction["instructionId"] = json_stringt{"ASSUME"}; + invalid_instruction["locationNumber"] = json_numbert{"2"}; + invalid_instruction["guard"] = json_numbert{"123"}; // Should be an object + instructions.push_back(invalid_instruction); + + function["instructions"] = instructions; + function["name"] = json_stringt{"test_function"}; + functions.push_back(function); + json_goto_functions["functions"] = functions; + + goto_functionst goto_functions; + REQUIRE_THROWS_AS( + goto_functions_from_json(json_goto_functions, goto_functions), + deserialization_exceptiont); + } +} + +TEST_CASE( + "Edge cases for JSON parsing", + "[core][json-symtab-language][json_goto_function]") +{ + SECTION("Empty objects and arrays") + { + // Test 1: Empty function object + json_objectt empty_function; + + // This should not throw, but create an empty function + goto_functiont function = goto_function_from_json(empty_function); + REQUIRE(function.body.instructions.empty()); + REQUIRE(function.parameter_identifiers.empty()); + REQUIRE(!function.is_hidden()); + + // Test 2: Empty body + json_objectt json_function; + json_function["instructions"] = json_arrayt{}; + + // This should not throw + goto_functiont function2 = goto_function_from_json(json_function); + REQUIRE(function2.body.instructions.empty()); + + // Test 3: Empty instructions array + json_objectt json_function3; + json_arrayt empty_instructions; + json_function3["instructions"] = empty_instructions; + + // This should not throw + goto_functiont function3 = goto_function_from_json(json_function3); + REQUIRE(function3.body.instructions.empty()); + } + + SECTION("Unusual but valid JSON") + { + // Test 1: Very large instruction array + json_objectt json_function; + json_arrayt instructions; + + // Add 1000 SKIP instructions + for(int i = 0; i < 1000; i++) + { + json_objectt skip_instruction; + skip_instruction["instructionId"] = json_stringt{"SKIP"}; + skip_instruction["locationNumber"] = json_numbert{std::to_string(i)}; + instructions.push_back(skip_instruction); + } + + json_function["instructions"] = instructions; + + // This should not throw + goto_functiont function = goto_function_from_json(json_function); + REQUIRE(function.body.instructions.size() == 1000); + + // Test 2: Very long parameter identifiers array + json_objectt json_function2; + json_arrayt param_ids; + + // Add 1000 parameter identifiers + for(int i = 0; i < 1000; i++) + { + param_ids.push_back(json_stringt{"param" + std::to_string(i)}); + } + + json_function2["parameterIdentifiers"] = param_ids; + + // This should not throw + goto_functiont function2 = goto_function_from_json(json_function2); + REQUIRE(function2.parameter_identifiers.size() == 1000); + } +} diff --git a/unit/json-symtab-language/module_dependencies.txt b/unit/json-symtab-language/module_dependencies.txt new file mode 100644 index 00000000000..d554d7c3542 --- /dev/null +++ b/unit/json-symtab-language/module_dependencies.txt @@ -0,0 +1,5 @@ +goto-programs +json +json-symtab-language +testing-utils +util