Skip to content

Commit 58b9d93

Browse files
Merge pull request #3112 from NlightNFotis/external_parser_support_rebased
Merge in feature branch that adds gnat2goto compatibility
2 parents 154b7ba + 86e8356 commit 58b9d93

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)