diff --git a/src/json-symtab-language/json_symtab_language.cpp b/src/json-symtab-language/json_symtab_language.cpp index f176a727b10..8910d668911 100644 --- a/src/json-symtab-language/json_symtab_language.cpp +++ b/src/json-symtab-language/json_symtab_language.cpp @@ -11,6 +11,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "json_symtab_language.h" #include #include +#include bool json_symtab_languaget::parse( std::istream &instream, @@ -30,6 +31,7 @@ bool json_symtab_languaget::typecheck( try { symbol_table_from_json(parsed_json_file, symbol_table); + follow_type_symbols(symbol_table); return false; } catch(const std::string &str) @@ -39,6 +41,51 @@ bool json_symtab_languaget::typecheck( } } +void json_symtab_languaget::follow_type_symbols( + irept &irep, + const namespacet &ns) +{ + ns.follow_type_symbol(irep); + + for(irept &sub : irep.get_sub()) + { + follow_type_symbols(sub, ns); + } + + for(auto &entry : irep.get_named_sub()) + { + irept &sub = entry.second; + + follow_type_symbols(sub, ns); + } +} + +void json_symtab_languaget::follow_type_symbols(symbol_tablet &symbol_table) +{ + const namespacet ns(symbol_table); + + std::vector type_symbol_names; + + for(auto &entry : symbol_table) + { + symbolt &symbol = symbol_table.get_writeable_ref(entry.first); + + if(symbol.is_type) + { + type_symbol_names.push_back(symbol.name); + } + + // Modify entries in place + follow_type_symbols(symbol.type, ns); + follow_type_symbols(symbol.value, ns); + } + + for(const irep_idt &id : type_symbol_names) + { + symbol_table.remove(id); + } +} + void json_symtab_languaget::show_parse(std::ostream &out) { parsed_json_file.output(out); diff --git a/src/json-symtab-language/json_symtab_language.h b/src/json-symtab-language/json_symtab_language.h index b5561a13442..1606d72de3a 100644 --- a/src/json-symtab-language/json_symtab_language.h +++ b/src/json-symtab-language/json_symtab_language.h @@ -60,6 +60,9 @@ class json_symtab_languaget:public languaget } protected: + void follow_type_symbols(symbol_tablet &symbol_table); + void follow_type_symbols(irept &irep, const namespacet &ns); + jsont parsed_json_file; }; diff --git a/src/util/Makefile b/src/util/Makefile index e28551fa668..20afbef0df3 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -38,6 +38,7 @@ SRC = arith_tools.cpp \ json_expr.cpp \ json_irep.cpp \ json_stream.cpp \ + json_symbol.cpp \ json_symbol_table.cpp \ lispexpr.cpp \ lispirep.cpp \ diff --git a/src/util/namespace.cpp b/src/util/namespace.cpp index 5329755d0cc..dd21672e3d1 100644 --- a/src/util/namespace.cpp +++ b/src/util/namespace.cpp @@ -67,6 +67,23 @@ void namespace_baset::follow_symbol(irept &irep) const } } +void namespace_baset::follow_type_symbol(irept &irep) const +{ + while(irep.id() == ID_symbol) + { + const symbolt &symbol = lookup(irep); + + if(symbol.is_type && !symbol.type.is_nil()) + { + irep = symbol.type; + } + else + { + break; + } + } +} + const typet &namespace_baset::follow(const typet &src) const { if(src.id()!=ID_symbol) diff --git a/src/util/namespace.h b/src/util/namespace.h index a72a3ba8a19..d84e42026e8 100644 --- a/src/util/namespace.h +++ b/src/util/namespace.h @@ -43,6 +43,7 @@ class namespace_baset virtual ~namespace_baset(); void follow_symbol(irept &irep) const; + void follow_type_symbol(irept &irep) const; void follow_macros(exprt &expr) const; const typet &follow(const typet &src) const; diff --git a/src/util/symbol_table_base.h b/src/util/symbol_table_base.h index 6a51a34a863..4057c685d11 100644 --- a/src/util/symbol_table_base.h +++ b/src/util/symbol_table_base.h @@ -179,7 +179,7 @@ class symbol_table_baset return &**this; } - symbolt &get_writeable_symbol(const irep_idt &identifier) + symbolt &get_writeable_symbol() { if(on_get_writeable) on_get_writeable((*this)->first);