44 if(expr.
id()==ID_symbol)
51 error() <<
"unexpected symbol: " <<
id <<
eom;
71 error() <<
"make_type_compatible got empty type: " << expr.
pretty() <<
eom;
87 error() <<
"failed to typecheck expr "
88 << expr.
pretty() <<
" with type "
90 <<
"; required type " << type.
pretty() <<
eom;
104 if(type.
id()==ID_code)
115 p.set_identifier(
add_prefix(p.get_identifier()));
116 new_symbol.
name=p.get_identifier();
125 new_symbol.
mode=
"jsil";
132 error() <<
"failed to add parameter symbol '" << new_symbol.
name
133 <<
"' in the symbol table" <<
eom;
157 if(expr.
id()==ID_code)
160 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
163 else if(expr.
id()==ID_symbol)
172 "expressions are expected not to have type set just yet");
174 if(expr.
id()==ID_null ||
175 expr.
id()==
"undefined" ||
178 else if(expr.
id()==
"null_type" ||
179 expr.
id()==
"undefined_type" ||
180 expr.
id()==ID_boolean ||
181 expr.
id()==ID_string ||
182 expr.
id()==
"number" ||
183 expr.
id()==
"builtin_object" ||
184 expr.
id()==
"user_object" ||
185 expr.
id()==
"object" ||
186 expr.
id()==ID_pointer ||
187 expr.
id()==ID_member ||
188 expr.
id()==
"variable")
190 else if(expr.
id()==
"proto" ||
192 expr.
id()==
"scope" ||
193 expr.
id()==
"constructid" ||
194 expr.
id()==
"primvalue" ||
195 expr.
id()==
"targetfunction" ||
201 else if(expr.
id()==ID_not)
203 else if(expr.
id()==
"string_to_num")
205 else if(expr.
id()==ID_unary_minus ||
206 expr.
id()==
"num_to_int32" ||
207 expr.
id()==
"num_to_uint32" ||
208 expr.
id()==ID_bitnot)
213 else if(expr.
id()==
"num_to_string")
218 else if(expr.
id()==ID_equal)
220 else if(expr.
id()==ID_lt ||
223 else if(expr.
id()==ID_plus ||
224 expr.
id()==ID_minus ||
225 expr.
id()==ID_mult ||
228 expr.
id()==ID_bitand ||
229 expr.
id()==ID_bitor ||
230 expr.
id()==ID_bitxor ||
235 else if(expr.
id()==ID_and ||
238 else if(expr.
id()==
"subtype_of")
240 else if(expr.
id()==ID_concatenation)
242 else if(expr.
id()==
"ref")
244 else if(expr.
id()==
"field")
246 else if(expr.
id()==ID_base)
248 else if(expr.
id()==ID_typeof)
250 else if(expr.
id()==
"new")
252 else if(expr.
id()==
"hasField")
254 else if(expr.
id()==ID_index)
256 else if(expr.
id()==
"delete")
258 else if(expr.
id()==
"protoField")
260 else if(expr.
id()==
"protoObj")
262 else if(expr.
id()==ID_side_effect)
276 irept &excep_list=expr.
add(ID_exception_list);
284 if(expr.
id()==ID_null)
286 else if(expr.
id()==
"undefined")
288 else if(expr.
id()==ID_empty)
297 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
312 error() <<
"operator '" << expr.
id() <<
"' expects two operands";
327 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
342 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
363 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
378 error() <<
"operator '" << expr.
id() <<
"' expects single operand" <<
eom;
392 error() <<
"operator '" << expr.
id() <<
"' expects single operand" <<
eom;
406 error() <<
"operator '" << expr.
id() <<
"' expects three operands" <<
eom;
416 if(operand3.
id()==ID_member)
418 else if(operand3.
id()==
"variable")
423 error() <<
"operator '" << expr.
id()
424 <<
"' expects reference type in the third parameter. Got:"
435 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
450 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
465 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
480 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
495 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
509 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
524 error() <<
"operator '" << expr.
id() <<
"' expects one operand" <<
eom;
538 error() <<
"operator '" << expr.
id() <<
"' expects one operand" <<
eom;
552 error() <<
"operator '" << expr.
id() <<
"' expects one operand" <<
eom;
568 identifier==
"eval" ||
571 symbol_table_baset::symbolst::const_iterator s_it =
576 error() <<
"unexpected internal symbol: " << identifier <<
eom;
582 const symbolt &symbol=s_it->second;
592 irep_idt identifier_base = identifier;
599 symbol_table_baset::symbolst::const_iterator s_it =
605 symbolt new_symbol{identifier, symbol_expr.
type(),
"jsil"};
606 new_symbol.base_name=identifier_base;
607 new_symbol.is_lvalue=new_symbol.type.id()!=ID_code;
610 new_symbol.is_extern=
true;
614 error() <<
"failed to add symbol '" << new_symbol.name
615 <<
"' in the symbol table" <<
eom;
622 DATA_INVARIANT(!s_it->second.is_type,
"non-type symbol expected");
624 const symbolt &symbol=s_it->second;
636 if(statement==ID_function_call)
638 else if(statement==ID_return)
640 else if(statement==ID_expression)
645 error() <<
"expression statement expected to have one operand"
652 else if(statement==ID_label)
657 else if(statement==ID_block)
659 else if(statement==ID_ifthenelse)
661 else if(statement==ID_goto)
665 else if(statement==ID_assign)
667 else if(statement==ID_try_catch)
669 else if(statement==ID_skip)
675 error() <<
"unexpected statement: " << statement <<
eom;
698 error() <<
"try_catch expected to have three operands" <<
eom;
716 error() <<
"function call expected to have three operands" <<
eom;
730 if(f.
id()==ID_symbol)
736 const symbolt &s=*maybe_symbol;
742 for(std::size_t i=0; i<
codet.parameters().size(); i++)
759 for(std::size_t i=call.
arguments().size();
760 i<
codet.parameters().size();
787 new_symbol.value=
exprt(
"no-body-just-yet");
794 error() <<
"failed to add expression symbol to symbol table"
838 if(symbol.
value.
id()!=
"no-body-just-yet")
846 else if(symbol.
name==
"eval")
850 else if(symbol.
value.
id()==
"no-body-just-yet")
857 error() <<
"non-type symbol value expected code, but got "
868 std::vector<irep_idt> identifiers;
872 identifiers.push_back(symbol_pair.first);
877 for(
const irep_idt &
id : identifiers)
885 for(
const irep_idt &
id : identifiers)
906 const unsigned errors_before=
930 catch(
const std::string &e)
Pre-defined bitvector types.
A goto_instruction_codet representing an assignment in the program.
codet representation of a "return from a function" statement.
const exprt & return_value() const
bool has_return_value() const
goto_instruction_codet representation of a function call statement.
codet representation of an if-then-else statement.
const exprt & cond() const
const codet & else_case() const
const codet & then_case() const
codet representation of a try/catch block.
codet & get_catch_code(unsigned i)
const parameterst & parameters() const
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
Fixed-width bit-vector with IEEE floating-point interpretation.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & id() const
irept & add(const irep_idt &name)
void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr)
void typecheck_expr_binary_arith(exprt &expr)
void typecheck_expr_constant(exprt &expr)
void typecheck_expr_has_field(exprt &expr)
void typecheck_expr_main(exprt &expr)
void typecheck_type_symbol(symbolt &)
void typecheck_function_call(code_function_callt &function_call)
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_unary_boolean(exprt &expr)
void typecheck_try_catch(code_try_catcht &code)
void typecheck_assign(code_assignt &code)
symbol_table_baset & symbol_table
void typecheck_expr_index(exprt &expr)
void typecheck_expr_proto_field(exprt &expr)
void typecheck_ifthenelse(code_ifthenelset &code)
void typecheck_expr_subtype(exprt &expr)
void typecheck_expr_ref(exprt &expr)
irep_idt add_prefix(const irep_idt &ds)
Prefix parameters and variables with a procedure name.
void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_expr_concatenation(exprt &expr)
void typecheck_expr_field(exprt &expr)
void typecheck_expr_unary_string(exprt &expr)
void typecheck_code(codet &code)
virtual std::string to_string(const exprt &expr)
void make_type_compatible(exprt &expr, const typet &type, bool must)
void typecheck_exp_binary_equal(exprt &expr)
void typecheck_expr_operands(exprt &expr)
void typecheck_expr_base(exprt &expr)
void typecheck_expr_delete(exprt &expr)
void typecheck_expr_proto_obj(exprt &expr)
void typecheck_block(codet &code)
void typecheck_expr_unary_num(exprt &expr)
void typecheck_symbol_expr(symbol_exprt &symbol_expr)
void typecheck_type(typet &type)
void typecheck_non_type_symbol(symbolt &symbol)
typechecking procedure declaration; any other symbols should have been typechecked during typecheckin...
void update_expr_type(exprt &expr, const typet &type)
void typecheck_return(code_frontend_returnt &)
void typecheck_expr_binary_compare(exprt &expr)
std::size_t get_message_count(unsigned level) const
source_locationt source_location
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
A side_effect_exprt representation of a side effect that throws an exception.
Expression to hold a symbol (variable)
void set_identifier(const irep_idt &identifier)
const irep_idt & get_identifier() const
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
The type of an expression, extends irept.
bool has_prefix(const std::string &s, const std::string &prefix)
std::string type2jsil(const typet &type, const namespacet &ns)
std::string expr2jsil(const exprt &expr, const namespacet &ns)
#define Forall_operands(it, expr)
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
const code_assignt & to_code_assign(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
bool jsil_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler)
typet jsil_value_or_empty_type()
typet jsil_undefined_type()
typet jsil_variable_reference_type()
bool jsil_is_subtype(const typet &type1, const typet &type2)
typet jsil_user_object_type()
typet jsil_union(const typet &type1, const typet &type2)
bool jsil_incompatible_types(const typet &type1, const typet &type2)
typet jsil_reference_type()
typet jsil_member_reference_type()
typet jsil_value_or_reference_type()
bool is_jsil_spec_code_type(const typet &type)
bool is_jsil_builtin_code_type(const typet &type)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
const code_frontend_returnt & to_code_frontend_return(const codet &code)
const code_labelt & to_code_label(const codet &code)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
const code_try_catcht & to_code_try_catch(const codet &code)
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
const codet & to_code(const exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.