Go to the documentation of this file.
41 if(expr.
id()==ID_symbol)
48 error() <<
"unexpected symbol: " <<
id <<
eom;
68 error() <<
"make_type_compatible got empty type: " << expr.
pretty() <<
eom;
84 error() <<
"failed to typecheck expr "
85 << expr.
pretty() <<
" with type "
87 <<
"; required type " << type.
pretty() <<
eom;
101 if(type.
id()==ID_code)
112 p.set_identifier(
add_prefix(p.get_identifier()));
113 new_symbol.
name=p.get_identifier();
122 new_symbol.
mode=
"jsil";
129 error() <<
"failed to add parameter symbol `"
130 << new_symbol.
name <<
"' in the symbol table" <<
eom;
154 if(expr.
id()==ID_code)
157 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
160 else if(expr.
id()==ID_symbol)
162 else if(expr.
id()==ID_constant)
170 if(expr.
id()==ID_null ||
171 expr.
id()==
"undefined" ||
174 else if(expr.
id()==
"null_type" ||
175 expr.
id()==
"undefined_type" ||
176 expr.
id()==ID_boolean ||
177 expr.
id()==ID_string ||
178 expr.
id()==
"number" ||
179 expr.
id()==
"builtin_object" ||
180 expr.
id()==
"user_object" ||
181 expr.
id()==
"object" ||
182 expr.
id()==ID_pointer ||
183 expr.
id()==ID_member ||
184 expr.
id()==
"variable")
186 else if(expr.
id()==
"proto" ||
188 expr.
id()==
"scope" ||
189 expr.
id()==
"constructid" ||
190 expr.
id()==
"primvalue" ||
191 expr.
id()==
"targetfunction" ||
197 else if(expr.
id()==ID_not)
199 else if(expr.
id()==
"string_to_num")
201 else if(expr.
id()==ID_unary_minus ||
202 expr.
id()==
"num_to_int32" ||
203 expr.
id()==
"num_to_uint32" ||
204 expr.
id()==ID_bitnot)
209 else if(expr.
id()==
"num_to_string")
214 else if(expr.
id()==ID_equal)
216 else if(expr.
id()==ID_lt ||
219 else if(expr.
id()==ID_plus ||
220 expr.
id()==ID_minus ||
221 expr.
id()==ID_mult ||
224 expr.
id()==ID_bitand ||
225 expr.
id()==ID_bitor ||
226 expr.
id()==ID_bitxor ||
231 else if(expr.
id()==ID_and ||
234 else if(expr.
id()==
"subtype_of")
236 else if(expr.
id()==ID_concatenation)
238 else if(expr.
id()==
"ref")
240 else if(expr.
id()==
"field")
242 else if(expr.
id()==ID_base)
244 else if(expr.
id()==ID_typeof)
246 else if(expr.
id()==
"new")
248 else if(expr.
id()==
"hasField")
250 else if(expr.
id()==ID_index)
252 else if(expr.
id()==
"delete")
254 else if(expr.
id()==
"protoField")
256 else if(expr.
id()==
"protoObj")
258 else if(expr.
id()==ID_side_effect)
272 irept &excep_list=expr.
add(ID_exception_list);
273 assert(excep_list.
id()==ID_symbol);
274 symbol_exprt &s=static_cast<symbol_exprt &>(excep_list);
280 if(expr.
id()==ID_null)
282 else if(expr.
id()==
"undefined")
284 else if(expr.
id()==ID_empty)
293 error() <<
"operator `" << expr.
id()
294 <<
"' expects two operands" <<
eom;
309 error() <<
"operator `" << expr.
id()
310 <<
"' expects two operands";
325 error() <<
"operator `" << expr.
id()
326 <<
"' expects two operands" <<
eom;
341 error() <<
"operator `" << expr.
id()
342 <<
"' expects two operands" <<
eom;
350 if(expr.
op1().
id()==
"fid" || expr.
op1().
id()==
"constructid")
361 error() <<
"operator `" << expr.
id()
362 <<
"' expects two operands" <<
eom;
377 error() <<
"operator `" << expr.
id()
378 <<
"' expects single operand" <<
eom;
392 error() <<
"operator `" << expr.
id()
393 <<
"' expects single operand" <<
eom;
407 error() <<
"operator `" << expr.
id()
408 <<
"' expects three operands" <<
eom;
418 if(operand3.id()==ID_member)
420 else if(operand3.id()==
"variable")
425 error() <<
"operator `" << expr.
id()
426 <<
"' expects reference type in the third parameter. Got:"
427 << operand3.pretty() <<
eom;
437 error() <<
"operator `" << expr.
id()
438 <<
"' expects two operands" <<
eom;
453 error() <<
"operator `" << expr.
id()
454 <<
"' expects two operands" <<
eom;
469 error() <<
"operator `" << expr.
id()
470 <<
"' expects two operands" <<
eom;
485 error() <<
"operator `" << expr.
id()
486 <<
"' expects two operands" <<
eom;
502 error() <<
"operator `" << expr.
id()
503 <<
"' expects two operands" <<
eom;
517 error() <<
"operator `" << expr.
id()
518 <<
"' expects two operands" <<
eom;
533 error() <<
"operator `" << expr.
id()
534 <<
"' expects one operand" <<
eom;
548 error() <<
"operator `" << expr.
id()
549 <<
"' expects one operand" <<
eom;
563 error() <<
"operator `" << expr.
id()
564 <<
"' expects one operand" <<
eom;
580 identifier==
"eval" ||
583 symbol_tablet::symbolst::const_iterator s_it=
588 error() <<
"unexpected internal symbol: " << identifier <<
eom;
594 const symbolt &symbol=s_it->second;
604 irep_idt identifier_base = identifier;
611 symbol_tablet::symbolst::const_iterator s_it=
618 new_symbol.
name=identifier;
621 new_symbol.
mode=
"jsil";
630 error() <<
"failed to add symbol `"
631 << new_symbol.
name <<
"' in the symbol table"
639 assert(!s_it->second.is_type);
641 const symbolt &symbol=s_it->second;
653 if(statement==ID_function_call)
655 else if(statement==ID_return)
657 else if(statement==ID_expression)
662 error() <<
"expression statement expected to have one operand"
669 else if(statement==ID_label)
674 else if(statement==ID_block)
676 else if(statement==ID_ifthenelse)
678 else if(statement==ID_goto)
682 else if(statement==ID_assign)
684 else if(statement==ID_try_catch)
686 else if(statement==ID_skip)
692 error() <<
"unexpected statement: " << statement <<
eom;
715 error() <<
"try_catch expected to have three operands" <<
eom;
733 error() <<
"function call expected to have three operands" <<
eom;
747 if(f.
id()==ID_symbol)
753 const symbolt &s=*maybe_symbol;
759 for(std::size_t i=0; i<
codet.parameters().size(); i++)
776 for(std::size_t i=call.
arguments().size();
777 i<
codet.parameters().size();
806 new_symbol.
mode=
"jsil";
815 error() <<
"failed to add expression symbol to symbol table"
859 if(symbol.
value.
id()!=
"no-body-just-yet")
867 else if(symbol.
name==
"eval")
871 else if(symbol.
value.
id()==
"no-body-just-yet")
878 error() <<
"non-type symbol value expected code, but got "
889 std::vector<irep_idt> identifiers;
893 identifiers.push_back(symbol_pair.first);
898 for(
const irep_idt &
id : identifiers)
906 for(
const irep_idt &
id : identifiers)
927 const unsigned errors_before=
951 catch(
const std::string &e)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void typecheck_expr_operands(exprt &expr)
void update_expr_type(exprt &expr, const typet &type)
void typecheck_expr_has_field(exprt &expr)
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
void typecheck_expr_binary_compare(exprt &expr)
#define Forall_operands(it, expr)
void typecheck_expr_unary_string(exprt &expr)
void typecheck_expr_ref(exprt &expr)
void typecheck_function_call(code_function_callt &function_call)
virtual std::string to_string(const exprt &expr)
The type of an expression, extends irept.
const codet & then_case() const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void typecheck_assign(code_assignt &code)
void typecheck_expr_base(exprt &expr)
codet representation of a try/catch block.
typet type
Type of symbol.
bool jsil_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)
codet & get_catch_code(unsigned i)
void typecheck_try_catch(code_try_catcht &code)
irept & add(const irep_namet &name)
Fixed-width bit-vector with IEEE floating-point interpretation.
void typecheck_type(typet &type)
void typecheck_expr_index(exprt &expr)
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
void typecheck_code(codet &code)
const exprt & cond() const
Expression to hold a symbol (variable)
void typecheck_return(code_returnt &code)
codet representation of an if-then-else statement.
bool jsil_incompatible_types(const typet &type1, const typet &type2)
void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr)
void typecheck_expr_unary_num(exprt &expr)
typet jsil_value_or_reference_type()
const codet & to_code(const exprt &expr)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
codet representation of a function call statement.
typet jsil_reference_type()
void typecheck_non_type_symbol(symbolt &symbol)
typechecking procedure declaration; any other symbols should have been typechecked during typecheckin...
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
irep_idt mode
Language mode.
void typecheck_expr_main(exprt &expr)
const std::string & id2string(const irep_idt &d)
std::string type2jsil(const typet &type, const namespacet &ns)
source_locationt source_location
typet jsil_union(const typet &type1, const typet &type2)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
const irep_idt & get_identifier() const
const code_labelt & to_code_label(const codet &code)
typet jsil_variable_reference_type()
void typecheck_expr_unary_boolean(exprt &expr)
void typecheck_expr_proto_field(exprt &expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
typet jsil_undefined_type()
void typecheck_ifthenelse(code_ifthenelset &code)
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
const code_returnt & to_code_return(const codet &code)
const parameterst & parameters() const
void typecheck_expr_proto_obj(exprt &expr)
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_binary_boolean(exprt &expr)
const code_try_catcht & to_code_try_catch(const codet &code)
void typecheck_symbol_expr(symbol_exprt &symbol_expr)
symbol_table_baset & symbol_table
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void typecheck_expr_constant(exprt &expr)
bool has_return_value() const
exprt value
Initial value of symbol.
typet jsil_member_reference_type()
codet representation of a "return from a function" statement.
const code_assignt & to_code_assign(const codet &code)
source_locationt location
Source code location of definition of symbol.
bool is_jsil_builtin_code_type(const typet &type)
void typecheck_type_symbol(symbolt &)
void typecheck_expr_concatenation(exprt &expr)
std::string expr2jsil(const exprt &expr, const namespacet &ns)
void typecheck_block(codet &code)
const codet & else_case() const
bool jsil_is_subtype(const typet &type1, const typet &type2)
bool is_jsil_spec_code_type(const typet &type)
void typecheck_expr_binary_arith(exprt &expr)
typet jsil_user_object_type()
typet jsil_value_or_empty_type()
A side_effect_exprt representation of a side effect that throws an exception.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_prefix(const std::string &s, const std::string &prefix)
Base class for tree-like data structures with sharing.
void typecheck_expr_subtype(exprt &expr)
Symbol table entry of function parameter.
void typecheck_expr_field(exprt &expr)
const exprt & return_value() const
A codet representing an assignment in the program.
const irep_idt & get_statement() const
irep_idt add_prefix(const irep_idt &ds)
Prefix parameters and variables with a procedure name.
const source_locationt & source_location() const
void set_identifier(const irep_idt &identifier)
irep_idt name
The unique identifier.
void typecheck_exp_binary_equal(exprt &expr)
void make_type_compatible(exprt &expr, const typet &type, bool must)
std::size_t get_message_count(unsigned level) const
void typecheck_expr_delete(exprt &expr)
Data structure for representing an arbitrary statement in a program.