From 06a88d6fdd310aa5fa1c0c4382ebbcc252a96bb3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 17 Sep 2025 12:34:48 +0000 Subject: [PATCH 1/6] Consolidate symtab2gb regression tests Use an approach similar to contracts regression tests to extract parameters for multiple tools from a single line in the .desc file. This avoids overly fragmenting regression tests. --- regression/CMakeLists.txt | 1 - regression/Makefile | 1 - regression/symtab2gb-cbmc/CMakeLists.txt | 3 --- regression/symtab2gb-cbmc/Makefile | 20 ------------------- regression/symtab2gb-cbmc/README.md | 4 ---- regression/symtab2gb-cbmc/chain.sh | 12 ----------- regression/symtab2gb/README.md | 5 +++-- regression/symtab2gb/chain.sh | 20 +++++++++++++++++-- .../show_foreign_symbol_table/json-ui.desc | 2 +- .../show_foreign_symbol_table/plain_text.desc | 2 +- .../show_foreign_symbol_table/rust.json | 0 .../show_foreign_symbol_table/xml-ui.desc | 2 +- 12 files changed, 24 insertions(+), 48 deletions(-) delete mode 100644 regression/symtab2gb-cbmc/CMakeLists.txt delete mode 100644 regression/symtab2gb-cbmc/Makefile delete mode 100644 regression/symtab2gb-cbmc/README.md delete mode 100755 regression/symtab2gb-cbmc/chain.sh rename regression/{symtab2gb-cbmc => symtab2gb}/show_foreign_symbol_table/json-ui.desc (88%) rename regression/{symtab2gb-cbmc => symtab2gb}/show_foreign_symbol_table/plain_text.desc (90%) rename regression/{symtab2gb-cbmc => symtab2gb}/show_foreign_symbol_table/rust.json (100%) rename regression/{symtab2gb-cbmc => symtab2gb}/show_foreign_symbol_table/xml-ui.desc (91%) 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/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$ -- From 618af82a9f4e2340aee2f7723316e4f7bdab50bd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 16 Sep 2025 18:52:21 +0000 Subject: [PATCH 2/6] Do not create locations with a set-but-empty function The C front-end created symbols that had the function set to an empty string. This was not accurately represented in the JSON representation, but also shouldn't be used at all. Thus, changing the parser rather than the JSON serialisation. --- src/ansi-c/c_preprocess.cpp | 2 +- src/ansi-c/parser.y | 6 +++--- src/util/parser.h | 5 +++++ src/util/source_location.h | 6 ++++++ 4 files changed, 15 insertions(+), 4 deletions(-) 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/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); From 29051b46b2ee3b9de196695d44b48b28bbf076a6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 16 Sep 2025 16:23:27 +0000 Subject: [PATCH 3/6] Write all source_locationt members as JSON We were previously only printing a subset, making it impossible to restore a `source_locationt` from its JSON representation. --- .../jdiff/java-properties/test.desc | 2 +- regression/cbmc-cover/json-goals1/test.desc | 2 +- regression/cbmc/json-interface1/test.desc | 4 +-- regression/cbmc/loophead-trace/test-json.desc | 2 +- regression/solver-hardness/guards/test.desc | 4 +-- src/util/json_irep.cpp | 34 +++++++++++++++++++ 6 files changed, 41 insertions(+), 7 deletions(-) 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/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/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; } From a36793a5900630f0d71f323b60e1b2c1d0559500 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 16 Sep 2025 16:27:32 +0000 Subject: [PATCH 4/6] Fix JSON parsing of source_locationt The JSON output of a `source_locationt` is different from generic `irept`. Also, make `try_get_{bool,string}` publicly available for subsequent re-use. --- src/goto-programs/show_symbol_table.cpp | 2 +- src/json-symtab-language/json_symbol.cpp | 132 +++++++++++++++++++---- src/json-symtab-language/json_symbol.h | 17 +++ 3 files changed, 130 insertions(+), 21 deletions(-) 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/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 From 5777e16cdfdcfbe67613e548bd25578a16a20376 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 16 Sep 2025 16:29:14 +0000 Subject: [PATCH 5/6] Make JSON output of goto functions complete We must include all information required to re-produce a goto program from its JSON representation. --- .../show_goto_functions_json.cpp | 52 ++++++++++++++----- 1 file changed, 39 insertions(+), 13 deletions(-) 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)); } From 6d3ce5d9203a37568e58c197250473a64e4a8436 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 16 Sep 2025 16:30:52 +0000 Subject: [PATCH 6/6] Add support for reading GOTO functions from JSON Adds a parser for JSON-encoded `goto_functionst` and support to `symtab2gb` to optionally read such from a file and store them in `goto_functions` of a `goto_modelt`. --- doc/man/symtab2gb.1 | 3 + src/json-symtab-language/Makefile | 9 +- .../json_goto_function.cpp | 350 ++++++++++++++++++ src/json-symtab-language/json_goto_function.h | 24 ++ .../json_goto_functions.cpp | 72 ++++ .../json_goto_functions.h | 25 ++ src/symtab2gb/module_dependencies.txt | 1 + src/symtab2gb/symtab2gb_parse_options.cpp | 49 ++- src/symtab2gb/symtab2gb_parse_options.h | 2 + unit/Makefile | 5 + .../json_goto_function.cpp | 46 +++ .../json_goto_function_extended.cpp | 331 +++++++++++++++++ .../json_goto_functions.cpp | 63 ++++ .../json_goto_functions_extended.cpp | 264 +++++++++++++ .../json_malformed_input.cpp | 279 ++++++++++++++ .../module_dependencies.txt | 5 + 16 files changed, 1524 insertions(+), 4 deletions(-) create mode 100644 src/json-symtab-language/json_goto_function.cpp create mode 100644 src/json-symtab-language/json_goto_function.h create mode 100644 src/json-symtab-language/json_goto_functions.cpp create mode 100644 src/json-symtab-language/json_goto_functions.h create mode 100644 unit/json-symtab-language/json_goto_function.cpp create mode 100644 unit/json-symtab-language/json_goto_function_extended.cpp create mode 100644 unit/json-symtab-language/json_goto_functions.cpp create mode 100644 unit/json-symtab-language/json_goto_functions_extended.cpp create mode 100644 unit/json-symtab-language/json_malformed_input.cpp create mode 100644 unit/json-symtab-language/module_dependencies.txt 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/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/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/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