cprover
Loading...
Searching...
No Matches
jsil_language.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Jsil Language
4
5Author: Michael Tautschnig, tautschn@amazon.com
6
7\*******************************************************************/
8
11
12#include "jsil_language.h"
13
14#include <util/get_base_name.h>
15#include <util/symbol_table.h>
16
17#include "expr2jsil.h"
18#include "jsil_convert.h"
19#include "jsil_entry_point.h"
21#include "jsil_parser.h"
22#include "jsil_typecheck.h"
23
24std::set<std::string> jsil_languaget::extensions() const
25{
26 return { "jsil" };
27}
28
29void jsil_languaget::modules_provided(std::set<std::string> &modules)
30{
31 modules.insert(get_base_name(parse_path, true));
32}
33
36{
37 if(jsil_convert(parse_tree, symbol_table, get_message_handler()))
38 return true;
39
40 jsil_internal_additions(symbol_table);
41 return false;
42}
43
45 std::istream &,
46 const std::string &,
47 std::ostream &)
48{
49 // there is no preprocessing!
50 return true;
51}
52
54 std::istream &instream,
55 const std::string &path)
56{
57 // store the path
58 parse_path=path;
59
60 // parsing
65
68
69 // save result
71
72 // save some memory
74
75 return result;
76}
77
80 symbol_table_baset &symbol_table,
81 const std::string &)
82{
83 if(jsil_typecheck(symbol_table, get_message_handler()))
84 return true;
85
86 return false;
87}
88
90 symbol_table_baset &symbol_table)
91{
92 return jsil_entry_point(
93 symbol_table,
95}
96
97void jsil_languaget::show_parse(std::ostream &out)
98{
99 parse_tree.output(out);
100}
101
102std::unique_ptr<languaget> new_jsil_language()
103{
105}
106
108 const exprt &expr,
109 std::string &code,
110 const namespacet &ns)
111{
112 code=expr2jsil(expr, ns);
113 return false;
114}
115
117 const typet &type,
118 std::string &code,
119 const namespacet &ns)
120{
121 code=type2jsil(type, ns);
122 return false;
123}
124
126 const std::string &code,
127 const std::string &,
128 exprt &expr,
129 const namespacet &ns)
130{
131 expr.make_nil();
132 std::istringstream instream(code);
133
134 // parsing
135
141
142 bool result=jsil_parser.parse();
143
144 if(jsil_parser.parse_tree.items.size()!=1)
145 result=true;
146 else
147 {
148 symbol_tablet symbol_table;
149 result=
151
152 if(symbol_table.symbols.size()!=1)
153 result=true;
154
155 if(!result)
156 expr=symbol_table.symbols.begin()->second.value;
157
158 // typecheck it
159 if(!result)
161 }
162
163 // save some memory
165
166 return result;
167}
168
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Base class for all expressions.
Definition expr.h:56
void make_nil()
Definition irep.h:454
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
jsil_parse_treet parse_tree
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
std::string parse_path
bool parse(std::istream &instream, const std::string &path) override
virtual ~jsil_languaget()
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
std::set< std::string > extensions() const override
bool typecheck(symbol_table_baset &context, const std::string &module) override
Converting from parse tree and type checking.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
bool generate_support_functions(symbol_table_baset &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
bool interfaces(symbol_table_baset &symbol_table) override
Adding symbols for all procedure declarations.
void show_parse(std::ostream &out) override
void modules_provided(std::set< std::string > &modules) override
void output(std::ostream &out) const
void swap(jsil_parse_treet &other)
jsil_parse_treet parse_tree
Definition jsil_parser.h:24
virtual bool parse() override
Definition jsil_parser.h:26
virtual void clear() override
Definition jsil_parser.h:31
message_handlert & get_message_handler()
Definition message.h:184
virtual void set_message_handler(message_handlert &_message_handler)
Definition message.h:179
mstreamt & result() const
Definition message.h:409
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
std::istream * in
Definition parser.h:26
void set_file(const irep_idt &file)
Definition parser.h:85
messaget log
Definition parser.h:136
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
The type of an expression, extends irept.
Definition type.h:29
std::string type2jsil(const typet &type, const namespacet &ns)
Definition expr2jsil.cpp:31
std::string expr2jsil(const exprt &expr, const namespacet &ns)
Definition expr2jsil.cpp:24
Jsil Language.
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
bool jsil_convert(const jsil_parse_treet &parse_tree, symbol_table_baset &symbol_table, message_handlert &message_handler)
Jsil Language Conversion.
bool jsil_entry_point(symbol_table_baset &symbol_table, message_handlert &message_handler)
Jsil Language.
void jsil_internal_additions(symbol_table_baset &dest)
std::unique_ptr< languaget > new_jsil_language()
Jsil Language.
jsil_parsert jsil_parser
Jsil Language.
void jsil_scanner_init()
bool jsil_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler)
Jsil Language.
Author: Diffblue Ltd.
dstringt irep_idt