cprover
jsil_language.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Jsil Language
4 
5 Author: Michael Tautschnig, tautschn@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #include "jsil_language.h"
13 
14 #include <util/symbol_table.h>
15 #include <util/get_base_name.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 
24 std::set<std::string> jsil_languaget::extensions() const
25 {
26  return { "jsil" };
27 }
28 
29 void 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 &instream,
46  const std::string &path,
47  std::ostream &outstream)
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
62  jsil_parser.set_file(path);
63  jsil_parser.in=&instream;
65 
67  bool result=jsil_parser.parse();
68 
69  // save result
71 
72  // save some memory
74 
75  return result;
76 }
77 
80  symbol_tablet &symbol_table,
81  const std::string &module)
82 {
83  if(jsil_typecheck(symbol_table, get_message_handler()))
84  return true;
85 
86  return false;
87 }
88 
90 {
92  symbol_table,
94  return true;
95 
96  return false;
97 }
98 
99 void jsil_languaget::show_parse(std::ostream &out)
100 {
101  parse_tree.output(out);
102 }
103 
105 {
106  return new jsil_languaget;
107 }
108 
110  const exprt &expr,
111  std::string &code,
112  const namespacet &ns)
113 {
114  code=expr2jsil(expr, ns);
115  return false;
116 }
117 
119  const typet &type,
120  std::string &code,
121  const namespacet &ns)
122 {
123  code=type2jsil(type, ns);
124  return false;
125 }
126 
128  const std::string &code,
129  const std::string &module,
130  exprt &expr,
131  const namespacet &ns)
132 {
133  expr.make_nil();
134  std::istringstream instream(code);
135 
136  // parsing
137 
138  jsil_parser.clear();
139  jsil_parser.set_file("");
140  jsil_parser.in=&instream;
143 
144  bool result=jsil_parser.parse();
145 
146  if(jsil_parser.parse_tree.items.size()!=1)
147  result=true;
148  else
149  {
150  symbol_tablet symbol_table;
151  result=
152  jsil_convert(parse_tree, symbol_table, get_message_handler());
153 
154  if(symbol_table.symbols.size()!=1)
155  result=true;
156 
157  if(!result)
158  expr=symbol_table.symbols.begin()->second.value;
159 
160  // typecheck it
161  if(!result)
162  result=jsil_typecheck(expr, get_message_handler(), ns);
163  }
164 
165  // save some memory
166  jsil_parser.clear();
167 
168  return result;
169 }
170 
172 {
173 }
Jsil Language.
The type of an expression.
Definition: type.h:20
mstreamt & result()
Definition: message.h:233
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
virtual bool parse(std::istream &instream, const std::string &path)
Jsil Language.
std::string expr2jsil(const exprt &expr, const namespacet &ns)
Definition: expr2jsil.cpp:24
std::istream * in
Definition: parser.h:26
jsil_parse_treet parse_tree
Definition: jsil_language.h:71
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
jsil_parsert jsil_parser
Definition: jsil_parser.cpp:14
void jsil_internal_additions(symbol_tablet &dest)
virtual bool final(symbol_tablet &context)
void jsil_scanner_init()
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
virtual std::set< std::string > extensions() const
virtual void modules_provided(std::set< std::string > &modules)
languaget * new_jsil_language()
void swap(jsil_parse_treet &other)
symbolst symbols
Definition: symbol_table.h:57
void set_file(const irep_idt &file)
Definition: parser.h:85
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
Jsil Language.
Symbol table.
virtual bool interfaces(symbol_tablet &symbol_table)
Adding symbols for all procedure declarations.
Jsil Language.
void output(std::ostream &out) const
virtual void show_parse(std::ostream &out)
bool jsil_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler)
virtual ~jsil_languaget()
message_handlert & get_message_handler()
Definition: message.h:127
std::string type2jsil(const typet &type, const namespacet &ns)
Definition: expr2jsil.cpp:31
Base class for all expressions.
Definition: expr.h:46
std::string parse_path
Definition: jsil_language.h:72
Jsil Language Conversion.
bool jsil_convert(const jsil_parse_treet &parse_tree, symbol_tablet &symbol_table, message_handlert &message_handler)
void make_nil()
Definition: irep.h:243
jsil_parse_treet parse_tree
Definition: jsil_parser.h:24
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
virtual bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns)
virtual void clear() override
Definition: jsil_parser.h:31
virtual bool parse() override
Definition: jsil_parser.h:26
virtual bool typecheck(symbol_tablet &context, const std::string &module)
Converting from parse tree and type checking.
Jsil Language.
bool jsil_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)