Skip to content

Commit 86e8356

Browse files
smowtonNlightNFotis
authored andcommitted
Implement JSON symtab language frontend.
Implement JSON symtab language, a new, more generic language frontend, able to read GOTO programs in JSON form, from any frontend that generates them. Currently this stands as the support frontend for our ADA conversion tool, GNAT2GOTO.
1 parent 5862b59 commit 86e8356

20 files changed

+346
-3
lines changed

CMakeLists.txt

+1
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,7 @@ set_target_properties(
6666
goto-symex
6767
jsil
6868
json
69+
json-symtab-language
6970
langapi
7071
linking
7172
pointer-analysis

jbmc/unit/CMakeLists.txt

+1
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ target_link_libraries(java-unit
2626
goto-programs
2727
goto-instrument-lib
2828
cbmc-lib
29+
json-symtab-language
2930
)
3031

3132
add_test(

jbmc/unit/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
108108
$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
109109
$(CPROVER_DIR)/src/cpp/cpp$(LIBEXT) \
110110
$(CPROVER_DIR)/src/json/json$(LIBEXT) \
111+
$(CPROVER_DIR)/src/json-symtab-language/json-symtab-language$(LIBEXT) \
111112
$(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
112113
$(CPROVER_DIR)/src/util/util$(LIBEXT) \
113114
$(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \

src/CMakeLists.txt

+1
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,7 @@ add_subdirectory(goto-programs)
8989
add_subdirectory(goto-symex)
9090
add_subdirectory(jsil)
9191
add_subdirectory(json)
92+
add_subdirectory(json-symtab-language)
9293
add_subdirectory(langapi)
9394
add_subdirectory(linking)
9495
add_subdirectory(pointer-analysis)

src/Makefile

+2-1
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ DIRS = analyses \
1212
goto-symex \
1313
jsil \
1414
json \
15+
json-symtab-language \
1516
langapi \
1617
linking \
1718
pointer-analysis \
@@ -41,7 +42,7 @@ cpp.dir: ansi-c.dir linking.dir
4142

4243
languages: util.dir langapi.dir \
4344
cpp.dir ansi-c.dir xmllang.dir assembler.dir \
44-
jsil.dir
45+
jsil.dir json-symtab-language.dir
4546

4647
solvers.dir: util.dir langapi.dir
4748

src/cbmc/CMakeLists.txt

+1
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ target_link_libraries(cbmc-lib
1717
goto-programs
1818
goto-symex
1919
json
20+
json-symtab-language
2021
langapi
2122
linking
2223
pointer-analysis

src/cbmc/Makefile

+2
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ SRC = all_properties.cpp \
1414

1515
OBJ += ../ansi-c/ansi-c$(LIBEXT) \
1616
../cpp/cpp$(LIBEXT) \
17+
../json/json$(LIBEXT) \
18+
../json-symtab-language/json-symtab-language$(LIBEXT) \
1719
../linking/linking$(LIBEXT) \
1820
../big-int/big-int$(LIBEXT) \
1921
../goto-programs/goto-programs$(LIBEXT) \

src/cbmc/cbmc_languages.cpp

+4-2
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
1515

1616
#include <ansi-c/ansi_c_language.h>
1717
#include <cpp/cpp_language.h>
18+
#include <json-symtab-language/json_symtab_language.h>
1819

1920
#ifdef HAVE_JSIL
2021
#include <jsil/jsil_language.h>
@@ -24,8 +25,9 @@ void cbmc_parse_optionst::register_languages()
2425
{
2526
register_language(new_ansi_c_language);
2627
register_language(new_cpp_language);
28+
register_language(new_json_symtab_language);
2729

28-
#ifdef HAVE_JSIL
30+
#ifdef HAVE_JSIL
2931
register_language(new_jsil_language);
30-
#endif
32+
#endif
3133
}

src/cbmc/module_dependencies.txt

+1
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ goto-instrument
55
goto-programs
66
goto-symex
77
jsil
8+
json-symtab-language
89
langapi # should go away
910
linking
1011
pointer-analysis
+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
file(GLOB_RECURSE sources "*.cpp" "*.h")
2+
add_library(json-symtab-language ${sources})
3+
4+
generic_includes(json-symtab-language)
5+
6+
target_link_libraries(json-symtab-language json util)

src/json-symtab-language/Makefile

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
SRC = json_symtab_language.cpp \
2+
json_symbol_table.cpp \
3+
json_symbol.cpp
4+
5+
INCLUDES= -I ..
6+
7+
include ../config.inc
8+
include ../common
9+
10+
CLEANFILES = json-symtab-language$(LIBEXT)
11+
12+
all: json-symtab-language$(LIBEXT)
13+
14+
###############################################################################
15+
16+
json-symtab-language$(LIBEXT): $(OBJ)
17+
$(LINKLIB)
+116
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
/*******************************************************************\
2+
3+
Module: JSON symbol deserialization
4+
5+
Author: Chris Smowton, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "json_symbol.h"
10+
11+
#include <util/exception_utils.h>
12+
#include <util/expr.h>
13+
#include <util/json_irep.h>
14+
#include <util/source_location.h>
15+
#include <util/type.h>
16+
17+
/// Return string value for a given key if present in the json object.
18+
/// \param in: The json object that is getting fetched as a string.
19+
/// \param key: The key for the json value to be fetched.
20+
/// \return: A string value for the corresponding key.
21+
static const std::string &
22+
try_get_string(const jsont &in, const std::string &key)
23+
{
24+
if(!in.is_string())
25+
throw deserialization_exceptiont(
26+
"symbol_from_json: expected string for key '" + key + "'");
27+
return in.value;
28+
}
29+
30+
/// Return boolean value for a given key if present in the json object.
31+
/// \param in: The json object that is getting fetched as a boolean.
32+
/// \param key: The key for the json value to be fetched.
33+
/// \return: A boolean value for the corresponding key.
34+
static bool try_get_bool(const jsont &in, const std::string &key)
35+
{
36+
if(!(in.is_true() || in.is_false()))
37+
throw deserialization_exceptiont(
38+
"symbol_from_json: expected bool for key '" + key + "'");
39+
return in.is_true();
40+
}
41+
42+
/// Deserialise a json object to a symbolt.
43+
/// \param in: The json object that is getting fetched as an object.
44+
/// \return: A symbolt representing the json object.
45+
symbolt symbol_from_json(const jsont &in)
46+
{
47+
if(!in.is_object())
48+
throw deserialization_exceptiont("symbol_from_json takes an object");
49+
symbolt result;
50+
json_irept json2irep(true);
51+
for(const auto &kv : in.object)
52+
{
53+
if(kv.first == "type")
54+
{
55+
irept irep = json2irep.convert_from_json(kv.second);
56+
result.type = static_cast<typet &>(irep);
57+
}
58+
else if(kv.first == "value")
59+
{
60+
irept irep = json2irep.convert_from_json(kv.second);
61+
result.value = static_cast<exprt &>(irep);
62+
}
63+
else if(kv.first == "location")
64+
{
65+
irept irep = json2irep.convert_from_json(kv.second);
66+
result.location = static_cast<source_locationt &>(irep);
67+
}
68+
else if(kv.first == "name")
69+
result.name = try_get_string(kv.second, "name");
70+
else if(kv.first == "module")
71+
result.module = try_get_string(kv.second, "module");
72+
else if(kv.first == "base_name")
73+
result.base_name = try_get_string(kv.second, "base_name");
74+
else if(kv.first == "mode")
75+
result.mode = try_get_string(kv.second, "mode");
76+
else if(kv.first == "pretty_name")
77+
result.pretty_name = try_get_string(kv.second, "pretty_name");
78+
else if(kv.first == "is_type")
79+
result.is_type = try_get_bool(kv.second, "is_type");
80+
else if(kv.first == "is_macro")
81+
result.is_macro = try_get_bool(kv.second, "is_macro");
82+
else if(kv.first == "is_exported")
83+
result.is_exported = try_get_bool(kv.second, "is_exported");
84+
else if(kv.first == "is_input")
85+
result.is_input = try_get_bool(kv.second, "is_input");
86+
else if(kv.first == "is_output")
87+
result.is_output = try_get_bool(kv.second, "is_output");
88+
else if(kv.first == "is_state_var")
89+
result.is_state_var = try_get_bool(kv.second, "is_state_var");
90+
else if(kv.first == "is_property")
91+
result.is_property = try_get_bool(kv.second, "is_property");
92+
else if(kv.first == "is_static_lifetime")
93+
result.is_static_lifetime = try_get_bool(kv.second, "is_static_lifetime");
94+
else if(kv.first == "is_thread_local")
95+
result.is_thread_local = try_get_bool(kv.second, "is_thread_local");
96+
else if(kv.first == "is_lvalue")
97+
result.is_lvalue = try_get_bool(kv.second, "is_lvalue");
98+
else if(kv.first == "is_file_local")
99+
result.is_file_local = try_get_bool(kv.second, "is_file_local");
100+
else if(kv.first == "is_extern")
101+
result.is_extern = try_get_bool(kv.second, "is_extern");
102+
else if(kv.first == "is_volatile")
103+
result.is_volatile = try_get_bool(kv.second, "is_volatile");
104+
else if(kv.first == "is_parameter")
105+
result.is_parameter = try_get_bool(kv.second, "is_parameter");
106+
else if(kv.first == "is_auxiliary")
107+
result.is_auxiliary = try_get_bool(kv.second, "is_auxiliary");
108+
else if(kv.first == "is_weak")
109+
result.is_weak = try_get_bool(kv.second, "is_weak");
110+
else
111+
throw deserialization_exceptiont(
112+
"symbol_from_json: unexpected key '" + kv.first + "'");
113+
}
114+
115+
return result;
116+
}
+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
/*******************************************************************\
2+
3+
Module: JSON symbol deserialization
4+
5+
Author: Chris Smowton, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMBOL_H
10+
#define CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMBOL_H
11+
12+
#include <util/json.h>
13+
#include <util/symbol.h>
14+
15+
symbolt symbol_from_json(const jsont &);
16+
17+
#endif
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
/*******************************************************************\
2+
3+
Module: JSON symbol table deserialization
4+
5+
Author: Chris Smowton, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "json_symbol_table.h"
10+
#include "json_symbol.h"
11+
12+
#include <util/exception_utils.h>
13+
#include <util/json.h>
14+
#include <util/symbol_table.h>
15+
16+
void symbol_table_from_json(const jsont &in, symbol_tablet &symbol_table)
17+
{
18+
if(!in.is_array())
19+
throw deserialization_exceptiont(
20+
"symbol_table_from_json: JSON input must be an array");
21+
for(const auto &js_symbol : in.array)
22+
{
23+
symbolt deserialized = symbol_from_json(js_symbol);
24+
if(symbol_table.add(deserialized))
25+
throw deserialization_exceptiont(
26+
"symbol_table_from_json: duplicate symbol name '" +
27+
id2string(deserialized.name) + "'");
28+
}
29+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
/*******************************************************************\
2+
3+
Module: JSON symbol table deserialization
4+
5+
Author: Chris Smowton, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMBOL_TABLE_H
10+
#define CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMBOL_TABLE_H
11+
12+
class jsont;
13+
class symbol_tablet;
14+
15+
void symbol_table_from_json(const jsont &, symbol_tablet &);
16+
17+
#endif
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
/*******************************************************************\
2+
3+
Module: JSON symbol table language. Accepts a JSON format symbol
4+
table that has been produced out-of-process, e.g. by using
5+
a compiler's front-end.
6+
7+
Author: Chris Smowton, [email protected]
8+
9+
\*******************************************************************/
10+
11+
#include "json_symtab_language.h"
12+
#include "json_symbol_table.h"
13+
#include <json/json_parser.h>
14+
#include <util/namespace.h>
15+
16+
/// Parse a goto program in json form.
17+
/// \param instream: The input stream
18+
/// \param path: A file path
19+
/// \return: boolean signifying success or failure of the parsing
20+
bool json_symtab_languaget::parse(
21+
std::istream &instream,
22+
const std::string &path)
23+
{
24+
return parse_json(instream, path, get_message_handler(), parsed_json_file);
25+
}
26+
27+
/// Typecheck a goto program in json form.
28+
/// \param symbol_table: The symbol table containing symbols read from file.
29+
/// \param module: A useless parameter, there for interface consistency.
30+
/// \return: boolean signifying success or failure of the typechecking.
31+
bool json_symtab_languaget::typecheck(
32+
symbol_tablet &symbol_table,
33+
const std::string &module)
34+
{
35+
try
36+
{
37+
symbol_table_from_json(parsed_json_file, symbol_table);
38+
return false;
39+
}
40+
catch(const std::string &str)
41+
{
42+
error() << "typecheck: " << str << eom;
43+
return true;
44+
}
45+
}
46+
47+
/// Output the result of the parsed json file to the output stream
48+
/// passed as a parameter to this function.
49+
/// \param out: The stream to use to output the parsed_json_file.
50+
void json_symtab_languaget::show_parse(std::ostream &out)
51+
{
52+
parsed_json_file.output(out);
53+
}

0 commit comments

Comments
 (0)