diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index ed71ad439ef..48f02e64c03 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -67,6 +67,7 @@ add_subdirectory(goto-cc-file-local) 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 cac9d590b2f..4e6f9bf85ca 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -42,6 +42,7 @@ DIRS = cbmc \ 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 new file mode 100644 index 00000000000..a8c851843b8 --- /dev/null +++ b/regression/symtab2gb-cbmc/CMakeLists.txt @@ -0,0 +1,3 @@ +add_test_pl_tests( + "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $" +) diff --git a/regression/symtab2gb-cbmc/Makefile b/regression/symtab2gb-cbmc/Makefile new file mode 100644 index 00000000000..32a16d37382 --- /dev/null +++ b/regression/symtab2gb-cbmc/Makefile @@ -0,0 +1,20 @@ +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: + @for dir in *; do \ + $(RM) tests.log; \ + if [ -d "$$dir" ]; then \ + cd "$$dir"; \ + $(RM) *.out *.gb; \ + cd ..; \ + fi \ + done diff --git a/regression/symtab2gb-cbmc/chain.sh b/regression/symtab2gb-cbmc/chain.sh new file mode 100755 index 00000000000..b3017af4186 --- /dev/null +++ b/regression/symtab2gb-cbmc/chain.sh @@ -0,0 +1,12 @@ +#!/bin/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-cbmc/readme.md b/regression/symtab2gb-cbmc/readme.md new file mode 100644 index 00000000000..5b29572a245 --- /dev/null +++ b/regression/symtab2gb-cbmc/readme.md @@ -0,0 +1,4 @@ +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/show_foreign_symbol_table/json-ui.desc b/regression/symtab2gb-cbmc/show_foreign_symbol_table/json-ui.desc new file mode 100644 index 00000000000..6e6cde0b7a5 --- /dev/null +++ b/regression/symtab2gb-cbmc/show_foreign_symbol_table/json-ui.desc @@ -0,0 +1,12 @@ +CORE +rust.json +--json-ui --show-symbol-table +"symbolTable": +"mode": "rust", +^EXIT=0$ +^SIGNAL=0$ +-- +symbol \w+ has unknown mode +-- +Test that --show-symbol-table with --json-ui correctly shows the source language +mode of a symbol, even if that language mode is unsupported. diff --git a/regression/symtab2gb-cbmc/show_foreign_symbol_table/plain_text.desc b/regression/symtab2gb-cbmc/show_foreign_symbol_table/plain_text.desc new file mode 100644 index 00000000000..9fdf6d48328 --- /dev/null +++ b/regression/symtab2gb-cbmc/show_foreign_symbol_table/plain_text.desc @@ -0,0 +1,12 @@ +CORE +rust.json +--show-symbol-table +Symbols: +Mode\.+: rust +^EXIT=0$ +^SIGNAL=0$ +-- +symbol \w+ has unknown mode +-- +Test that --show-symbol-table correctly shows the source language mode of a +symbol, even if that language mode is unsupported. diff --git a/regression/symtab2gb-cbmc/show_foreign_symbol_table/rust.json b/regression/symtab2gb-cbmc/show_foreign_symbol_table/rust.json new file mode 100644 index 00000000000..b9dcc02d67a --- /dev/null +++ b/regression/symtab2gb-cbmc/show_foreign_symbol_table/rust.json @@ -0,0 +1,591 @@ +{ + "symbolTable": { + "VoidUnit": { + "baseName": "VoidUnit", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "rust", + "module": "", + "name": "VoidUnit", + "prettyName": "", + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + }, + "value": { + "id": "nil" + } + }, + "main": { + "baseName": "main", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "1" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "mode": "rust", + "module": "", + "name": "main", + "prettyName": "main", + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "" + }, + "return_type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + }, + "value": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "1" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "block" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "decl" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_0" + }, + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "9" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "statement": { + "id": "decl" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_1::rol8" + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "label": { + "id": "bb0" + }, + "statement": { + "id": "label" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "statement": { + "id": "block" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "statement": { + "id": "assign" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_1::rol8" + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + } + }, + { + "id": "rol", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "38" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "3" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "destination": { + "id": "bb1" + }, + "statement": { + "id": "goto" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "label": { + "id": "bb1" + }, + "statement": { + "id": "label" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "skip" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "statement": { + "id": "return" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "VoidUnit" + }, + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + } + ] + } + ] + } + }, + "main::1::var_0": { + "baseName": "var_0", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "mode": "rust", + "module": "", + "name": "main::1::var_0", + "prettyName": "", + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + }, + "value": { + "id": "nil" + } + }, + "main::1::var_1::rol8": { + "baseName": "rol8", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "9" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "mode": "rust", + "module": "", + "name": "main::1::var_1::rol8", + "prettyName": "", + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "nil" + } + }, + "tag-Unit": { + "baseName": "Unit", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": false, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": true, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "rust", + "module": "", + "name": "tag-Unit", + "prettyName": "", + "type": { + "id": "struct", + "namedSub": { + "components": { + "id": "" + }, + "tag": { + "id": "Unit" + } + } + }, + "value": { + "id": "nil" + } + } + } +} diff --git a/regression/symtab2gb-cbmc/show_foreign_symbol_table/xml-ui.desc b/regression/symtab2gb-cbmc/show_foreign_symbol_table/xml-ui.desc new file mode 100644 index 00000000000..fc807f3a61a --- /dev/null +++ b/regression/symtab2gb-cbmc/show_foreign_symbol_table/xml-ui.desc @@ -0,0 +1,12 @@ +CORE +rust.json +--xml-ui --show-symbol-table +^EXIT=0$ +^SIGNAL=0$ +-- +symbol \w+ has unknown mode +-- +Test that --show-symbol-table with --xml-ui does not crash when given an symbol +with an unsupported language mode. Note that no symbol table is shown at the +time of writing this test, because --show-symbol-table has not been implemented +for the xml user interface. diff --git a/regression/symtab2gb/readme.md b/regression/symtab2gb/readme.md new file mode 100644 index 00000000000..2cbc1d83ce8 --- /dev/null +++ b/regression/symtab2gb/readme.md @@ -0,0 +1,4 @@ +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. diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index b91cb973e29..85e7049f4cb 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -24,6 +24,23 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_model.h" +/// \brief Gets the language which should be used for showing the type and value +/// of the supplied \p symbol. +/// \return A unique pointer, pointing to the language corresponding to the mode +/// of the \p symbol in the case where the symbol specifies a known/registered +/// language mode. Returns the globally configured default language/first +/// language registered in the case where mode is empty or does not correspond +/// to a known registered language. The enables showing the symbol even if the +/// language is not recognised. +static std::unique_ptr +get_show_symbol_language(const symbolt &symbol) +{ + if(!symbol.mode.empty()) + if(auto language_from_mode = get_language_from_mode(symbol.mode)) + return language_from_mode; + return get_default_language(); +} + void show_symbol_table_xml_ui() { } @@ -39,16 +56,7 @@ void show_symbol_table_brief_plain( { const symbolt &symbol=ns.lookup(id); - std::unique_ptr ptr; - - if(symbol.mode.empty()) - ptr=get_default_language(); - else - { - ptr=get_language_from_mode(symbol.mode); - if(ptr==nullptr) - throw "symbol "+id2string(symbol.name)+" has unknown mode"; - } + const std::unique_ptr ptr = get_show_symbol_language(symbol); std::string type_str; @@ -72,19 +80,7 @@ void show_symbol_table_plain( { const symbolt &symbol=ns.lookup(id); - std::unique_ptr ptr; - - if(symbol.mode.empty()) - { - ptr=get_default_language(); - } - else - { - ptr=get_language_from_mode(symbol.mode); - } - - if(!ptr) - throw "symbol "+id2string(symbol.name)+" has unknown mode"; + const std::unique_ptr ptr = get_show_symbol_language(symbol); std::string type_str, value_str; @@ -160,19 +156,7 @@ static void show_symbol_table_json_ui( { const symbolt &symbol = id_and_symbol.second; - std::unique_ptr ptr; - - if(symbol.mode.empty()) - { - ptr=get_default_language(); - } - else - { - ptr=get_language_from_mode(symbol.mode); - } - - if(!ptr) - throw "symbol "+id2string(symbol.name)+" has unknown mode"; + const std::unique_ptr ptr = get_show_symbol_language(symbol); std::string type_str, value_str; @@ -234,19 +218,7 @@ static void show_symbol_table_brief_json_ui( { const symbolt &symbol = id_and_symbol.second; - std::unique_ptr ptr; - - if(symbol.mode.empty()) - { - ptr=get_default_language(); - } - else - { - ptr=get_language_from_mode(symbol.mode); - } - - if(!ptr) - throw "symbol "+id2string(symbol.name)+" has unknown mode"; + const std::unique_ptr ptr = get_show_symbol_language(symbol); std::string type_str, value_str;