41 if(expr.
id()==ID_symbol)
47 error() <<
"unexpected symbol: " <<
id <<
eom;
67 error() <<
"make_type_compatible got empty type: " << expr.
pretty() <<
eom;
83 error() <<
"failed to typecheck expr " 84 << expr.
pretty() <<
" with type " 86 <<
"; required type " << type.
pretty() <<
eom;
100 if(type.
id()==ID_code)
111 p.set_identifier(
add_prefix(p.get_identifier()));
112 new_symbol.
name=p.get_identifier();
121 new_symbol.
mode=
"jsil";
128 error() <<
"failed to add parameter symbol `" 129 << new_symbol.
name <<
"' in the symbol table" <<
eom;
153 if(expr.
id()==ID_code)
156 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
159 else if(expr.
id()==ID_symbol)
161 else if(expr.
id()==ID_constant)
169 if(expr.
id()==ID_null ||
170 expr.
id()==
"undefined" ||
173 else if(expr.
id()==
"null_type" ||
174 expr.
id()==
"undefined_type" ||
175 expr.
id()==ID_boolean ||
176 expr.
id()==ID_string ||
177 expr.
id()==
"number" ||
178 expr.
id()==
"builtin_object" ||
179 expr.
id()==
"user_object" ||
180 expr.
id()==
"object" ||
181 expr.
id()==ID_reference ||
182 expr.
id()==ID_member ||
183 expr.
id()==
"variable")
185 else if(expr.
id()==
"proto" ||
187 expr.
id()==
"scope" ||
188 expr.
id()==
"constructid" ||
189 expr.
id()==
"primvalue" ||
190 expr.
id()==
"targetfunction" ||
196 else if(expr.
id()==ID_not)
198 else if(expr.
id()==
"string_to_num")
200 else if(expr.
id()==ID_unary_minus ||
201 expr.
id()==
"num_to_int32" ||
202 expr.
id()==
"num_to_uint32" ||
203 expr.
id()==ID_bitnot)
208 else if(expr.
id()==
"num_to_string")
213 else if(expr.
id()==ID_equal)
215 else if(expr.
id()==ID_lt ||
218 else if(expr.
id()==ID_plus ||
219 expr.
id()==ID_minus ||
220 expr.
id()==ID_mult ||
223 expr.
id()==ID_bitand ||
224 expr.
id()==ID_bitor ||
225 expr.
id()==ID_bitxor ||
230 else if(expr.
id()==ID_and ||
233 else if(expr.
id()==
"subtype_of")
235 else if(expr.
id()==ID_concatenation)
237 else if(expr.
id()==
"ref")
239 else if(expr.
id()==
"field")
241 else if(expr.
id()==ID_base)
243 else if(expr.
id()==ID_typeof)
245 else if(expr.
id()==
"new")
247 else if(expr.
id()==
"hasField")
249 else if(expr.
id()==ID_index)
251 else if(expr.
id()==
"delete")
253 else if(expr.
id()==
"protoField")
255 else if(expr.
id()==
"protoObj")
257 else if(expr.
id()==ID_side_effect)
271 irept &excep_list=expr.
add(ID_exception_list);
272 assert(excep_list.
id()==ID_symbol);
279 if(expr.
id()==ID_null)
281 else if(expr.
id()==
"undefined")
283 else if(expr.
id()==ID_empty)
292 error() <<
"operator `" << expr.
id()
293 <<
"' expects two operands" <<
eom;
308 error() <<
"operator `" << expr.
id()
309 <<
"' expects two operands";
324 error() <<
"operator `" << expr.
id()
325 <<
"' expects two operands" <<
eom;
340 error() <<
"operator `" << expr.
id()
341 <<
"' expects two operands" <<
eom;
349 if(expr.
op1().
id()==
"fid" || expr.
op1().
id()==
"constructid")
360 error() <<
"operator `" << expr.
id()
361 <<
"' expects two operands" <<
eom;
376 error() <<
"operator `" << expr.
id()
377 <<
"' expects single operand" <<
eom;
391 error() <<
"operator `" << expr.
id()
392 <<
"' expects single operand" <<
eom;
406 error() <<
"operator `" << expr.
id()
407 <<
"' expects three operands" <<
eom;
417 if(operand3.id()==ID_member)
419 else if(operand3.id()==
"variable")
424 error() <<
"operator `" << expr.
id()
425 <<
"' expects reference type in the third parameter. Got:" 426 << operand3.pretty() <<
eom;
436 error() <<
"operator `" << expr.
id()
437 <<
"' expects two operands" <<
eom;
452 error() <<
"operator `" << expr.
id()
453 <<
"' expects two operands" <<
eom;
468 error() <<
"operator `" << expr.
id()
469 <<
"' expects two operands" <<
eom;
484 error() <<
"operator `" << expr.
id()
485 <<
"' expects two operands" <<
eom;
501 error() <<
"operator `" << expr.
id()
502 <<
"' expects two operands" <<
eom;
516 error() <<
"operator `" << expr.
id()
517 <<
"' expects two operands" <<
eom;
532 error() <<
"operator `" << expr.
id()
533 <<
"' expects one operand" <<
eom;
547 error() <<
"operator `" << expr.
id()
548 <<
"' expects one operand" <<
eom;
562 error() <<
"operator `" << expr.
id()
563 <<
"' expects one operand" <<
eom;
579 identifier==
"eval" ||
582 symbol_tablet::symbolst::const_iterator s_it=
587 error() <<
"unexpected internal symbol: " << identifier <<
eom;
593 const symbolt &symbol=s_it->second;
603 irep_idt identifier_base = identifier;
610 symbol_tablet::symbolst::const_iterator s_it=
617 new_symbol.
name=identifier;
620 new_symbol.
mode=
"jsil";
629 error() <<
"failed to add symbol `" 630 << new_symbol.
name <<
"' in the symbol table" 638 assert(!s_it->second.is_type);
640 const symbolt &symbol=s_it->second;
652 if(statement==ID_function_call)
654 else if(statement==ID_return)
656 else if(statement==ID_expression)
661 error() <<
"expression statement expected to have one operand" 668 else if(statement==ID_label)
673 else if(statement==ID_block)
675 else if(statement==ID_ifthenelse)
677 else if(statement==ID_goto)
681 else if(statement==ID_assign)
683 else if(statement==ID_try_catch)
685 else if(statement==ID_skip)
691 error() <<
"unexpected statement: " << statement <<
eom;
714 error() <<
"try_catch expected to have three operands" <<
eom;
732 error() <<
"function call expected to have three operands" <<
eom;
746 if(f.
id()==ID_symbol)
758 for(std::size_t i=0; i<codet.
parameters().size(); i++)
775 for(std::size_t i=call.
arguments().size();
805 new_symbol.
mode=
"jsil";
814 error() <<
"failed to add expression symbol to symbol table" 858 if(symbol.
value.
id()!=
"no-body-just-yet")
866 else if(symbol.
name==
"eval")
870 else if(symbol.
value.
id()==
"no-body-just-yet")
877 error() <<
"non-type symbol value expected code, but got " 888 std::vector<irep_idt> identifiers;
891 identifiers.push_back(s_it->first);
895 for(
const irep_idt &
id : identifiers)
904 for(
const irep_idt &
id : identifiers)
926 const unsigned errors_before=
942 jsil_typecheck.
error();
950 catch(
const std::string &e)
const irep_idt & get_statement() const
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_constant(exprt &expr)
The type of an expression.
irep_idt name
The unique identifier.
const codet & then_case() const
const exprt & return_value() const
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
const std::string & id2string(const irep_idt &d)
void typecheck_expr_proto_obj(exprt &expr)
#define forall_symbols(it, expr)
std::string expr2jsil(const exprt &expr, const namespacet &ns)
Symbol table entry of function parameterThis is a symbol generated as part of type checking...
void typecheck_expr_unary_num(exprt &expr)
codet & get_catch_code(unsigned i)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void typecheck_expr_base(exprt &expr)
Fixed-width bit-vector with IEEE floating-point interpretation.
irep_idt mode
Language mode.
const exprt & cond() const
void typecheck_expr_ref(exprt &expr)
void typecheck_expr_binary_arith(exprt &expr)
const irep_idt & get_identifier() const
void typecheck_assign(code_assignt &code)
exprt value
Initial value of symbol.
void typecheck_expr_main(exprt &expr)
void typecheck_function_call(code_function_callt &function_call)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr)
static mstreamt & eom(mstreamt &m)
A side effect that throws an exception.
void typecheck_symbol_expr(symbol_exprt &symbol_expr)
void typecheck_exp_binary_equal(exprt &expr)
typet jsil_value_or_reference_type()
virtual std::string to_string(const exprt &expr)
bool is_jsil_spec_code_type(const typet &type)
irep_idt add_prefix(const irep_idt &ds)
Prefix parameters and variables with a procedure name.
void typecheck_expr_concatenation(exprt &expr)
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
void typecheck_code(codet &code)
bool jsil_incompatible_types(const typet &type1, const typet &type2)
void typecheck_non_type_symbol(symbolt &symbol)
typechecking procedure declaration; any other symbols should have been typechecked during typecheckin...
void typecheck_expr_unary_boolean(exprt &expr)
typet jsil_union(const typet &type1, const typet &type2)
void typecheck_return(code_returnt &code)
source_locationt source_location
typet jsil_reference_type()
API to expression classes.
typet jsil_undefined_type()
const code_returnt & to_code_return(const codet &code)
void typecheck_type_symbol(symbolt &symbol)
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
Base class for tree-like data structures with sharing.
void err_location(const source_locationt &loc)
void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_expr_subtype(exprt &expr)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
typet jsil_variable_reference_type()
void typecheck_expr_proto_field(exprt &expr)
bool has_return_value() const
bool has_prefix(const std::string &s, const std::string &prefix)
void typecheck_type(typet &type)
bool is_jsil_builtin_code_type(const typet &type)
void make_type_compatible(exprt &expr, const typet &type, bool must)
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
void typecheck_expr_unary_string(exprt &expr)
void typecheck_block(codet &code)
bool jsil_is_subtype(const typet &type1, const typet &type2)
std::string type2jsil(const typet &type, const namespacet &ns)
Base class for all expressions.
typet jsil_member_reference_type()
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void typecheck_expr_operands(exprt &expr)
typet jsil_value_or_empty_type()
irept & add(const irep_namet &name)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void set_identifier(const irep_idt &identifier)
#define Forall_operands(it, expr)
bool has_symbol(const irep_idt &name) const
const codet & to_code(const exprt &expr)
symbol_tablet & symbol_table
Expression to hold a symbol (variable)
typet jsil_user_object_type()
void typecheck_expr_delete(exprt &expr)
A statement in a programming language.
const code_labelt & to_code_label(const codet &code)
const code_try_catcht & to_code_try_catch(const codet &code)
const codet & else_case() const
message_handlert * message_handler
void typecheck_expr_binary_compare(exprt &expr)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
void typecheck_ifthenelse(code_ifthenelset &code)
virtual bool typecheck_main()
void typecheck_expr_field(exprt &expr)
const typet & return_type() const
void typecheck_expr_has_field(exprt &expr)
void typecheck_try_catch(code_try_catcht &code)
const code_function_callt & to_code_function_call(const codet &code)
bool jsil_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)
void update_expr_type(exprt &expr, const typet &type)
void typecheck_expr_index(exprt &expr)
unsigned get_message_count(unsigned level) const