From 455e8afa5a784b8b3819c024d89844a2cdca0e4e Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 17 Aug 2021 10:45:45 +0100 Subject: [PATCH 1/5] Deduplicate code for getting language for showing symbol table So that the reader can more easily see that each of the functions in this file get the language in the same way and so that any future changes to this functionality only need to be made in one place. --- src/goto-programs/show_symbol_table.cpp | 75 +++++++++---------------- 1 file changed, 26 insertions(+), 49 deletions(-) diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index b91cb973e29..01e49e23f63 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -24,6 +24,28 @@ 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. +static std::unique_ptr +get_show_symbol_language(const symbolt &symbol) +{ + 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"; + + return ptr; +} + void show_symbol_table_xml_ui() { } @@ -39,16 +61,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 +85,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 +161,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 +223,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; From d0c9659e4c135ffd7a80d78c7b5b8a028ec7ef4d Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 17 Aug 2021 10:45:46 +0100 Subject: [PATCH 2/5] Use default language for showing symbols of unrecognised language --- src/goto-programs/show_symbol_table.cpp | 19 ++++--------------- 1 file changed, 4 insertions(+), 15 deletions(-) diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index 01e49e23f63..20f4d5b09b1 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -29,21 +29,10 @@ Author: Daniel Kroening, kroening@kroening.com static std::unique_ptr get_show_symbol_language(const symbolt &symbol) { - 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"; - - return ptr; + 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() From 13e88180d34aa7a4f507a3b1bdc3381c713be229 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 17 Aug 2021 10:45:47 +0100 Subject: [PATCH 3/5] Document how tests in `symtab2gb` directory work --- regression/symtab2gb/readme.md | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 regression/symtab2gb/readme.md 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. From 2b474815d2d31a7bf1b075038f35a30ff2cccee9 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 17 Aug 2021 10:45:48 +0100 Subject: [PATCH 4/5] Add tests of --show-symbol-table with unsupported language To confirm that the fix from the previous "use default language" commit is worked as expected. --- regression/CMakeLists.txt | 1 + regression/Makefile | 1 + regression/symtab2gb-cbmc/CMakeLists.txt | 3 + regression/symtab2gb-cbmc/Makefile | 20 + regression/symtab2gb-cbmc/chain.sh | 12 + regression/symtab2gb-cbmc/readme.md | 4 + .../show_foreign_symbol_table/json-ui.desc | 12 + .../show_foreign_symbol_table/plain_text.desc | 12 + .../show_foreign_symbol_table/rust.json | 591 ++++++++++++++++++ .../show_foreign_symbol_table/xml-ui.desc | 12 + 10 files changed, 668 insertions(+) create mode 100644 regression/symtab2gb-cbmc/CMakeLists.txt create mode 100644 regression/symtab2gb-cbmc/Makefile create mode 100755 regression/symtab2gb-cbmc/chain.sh create mode 100644 regression/symtab2gb-cbmc/readme.md create mode 100644 regression/symtab2gb-cbmc/show_foreign_symbol_table/json-ui.desc create mode 100644 regression/symtab2gb-cbmc/show_foreign_symbol_table/plain_text.desc create mode 100644 regression/symtab2gb-cbmc/show_foreign_symbol_table/rust.json create mode 100644 regression/symtab2gb-cbmc/show_foreign_symbol_table/xml-ui.desc 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. From 21ac5506cc9483c88792abb31164a80a66fd291d Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 18 Aug 2021 11:19:42 +0100 Subject: [PATCH 5/5] Document return value of `get_show_symbol_language` function Because the behaviour could be surprising if the reader is not familiar with the intended behaviour. --- src/goto-programs/show_symbol_table.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index 20f4d5b09b1..85e7049f4cb 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -26,6 +26,12 @@ Author: Daniel Kroening, kroening@kroening.com /// \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) {