cprover
jsil_typecheck.h
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 #ifndef CPROVER_JSIL_JSIL_TYPECHECK_H
13 #define CPROVER_JSIL_JSIL_TYPECHECK_H
14 
15 #include <unordered_set>
16 
17 #include <util/namespace.h>
18 #include <util/std_code.h>
19 #include <util/symbol_table_base.h>
20 #include <util/typecheck.h>
21 
22 class symbol_exprt;
23 class codet;
24 
25 bool jsil_typecheck(
26  symbol_tablet &symbol_table,
27  message_handlert &message_handler);
28 
29 bool jsil_typecheck(
30  exprt &expr,
31  message_handlert &message_handler,
32  const namespacet &ns);
33 
35 {
36 public:
38  symbol_table_baset &_symbol_table,
39  message_handlert &_message_handler)
40  : typecheckt(_message_handler),
41  symbol_table(_symbol_table),
43  proc_name()
44  {
45  }
46 
47  virtual ~jsil_typecheckt() { }
48 
49  virtual void typecheck();
50  virtual void typecheck_expr(exprt &expr);
51 
52 protected:
54  const namespacet ns;
55  // prefix to variables which is set in typecheck_declaration
57 
58  void update_expr_type(exprt &expr, const typet &type);
59  void make_type_compatible(exprt &expr, const typet &type, bool must);
61  void typecheck_non_type_symbol(symbolt &symbol);
62  void typecheck_symbol_expr(symbol_exprt &symbol_expr);
64  void typecheck_expr_delete(exprt &expr);
65  void typecheck_expr_index(exprt &expr);
67  void typecheck_expr_proto_obj(exprt &expr);
68  void typecheck_expr_has_field(exprt &expr);
69  void typecheck_expr_ref(exprt &expr);
70  void typecheck_expr_field(exprt &expr);
71  void typecheck_expr_base(exprt &expr);
72  void typecheck_expr_constant(exprt &expr);
74  void typecheck_expr_subtype(exprt &expr);
81  void typecheck_expr_unary_num(exprt &expr);
82  void typecheck_expr_operands(exprt &expr);
83  void typecheck_expr_main(exprt &expr);
84  void typecheck_code(codet &code);
85  void typecheck_function_call(code_function_callt &function_call);
86  void typecheck_return(code_returnt &code);
87  void typecheck_block(codet &code);
89  void typecheck_assign(code_assignt &code);
91  void typecheck_type(typet &type);
92  irep_idt add_prefix(const irep_idt &ds);
93 
94  // overload to use language-specific syntax
95  virtual std::string to_string(const exprt &expr);
96  virtual std::string to_string(const typet &type);
97 
98  std::unordered_set<irep_idt> already_typechecked;
99 };
100 
101 #endif // CPROVER_JSIL_JSIL_TYPECHECK_H
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_constant(exprt &expr)
The type of an expression, extends irept.
Definition: type.h:27
void typecheck_expr_proto_obj(exprt &expr)
codet representation of a try/catch block.
Definition: std_code.h:2007
void typecheck_expr_unary_num(exprt &expr)
void typecheck_expr_base(exprt &expr)
void typecheck_expr_ref(exprt &expr)
void typecheck_expr_binary_arith(exprt &expr)
void typecheck_assign(code_assignt &code)
const namespacet ns
void typecheck_expr_main(exprt &expr)
void typecheck_function_call(code_function_callt &function_call)
Symbol table entry.
Definition: symbol.h:27
void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr)
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:1792
void typecheck_symbol_expr(symbol_exprt &symbol_expr)
irep_idt proc_name
void typecheck_exp_binary_equal(exprt &expr)
virtual std::string to_string(const exprt &expr)
irep_idt add_prefix(const irep_idt &ds)
Prefix parameters and variables with a procedure name.
void typecheck_expr_concatenation(exprt &expr)
void typecheck_code(codet &code)
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)
void typecheck_return(code_returnt &code)
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
codet representation of a function call statement.
Definition: std_code.h:1036
void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_expr_subtype(exprt &expr)
void typecheck_type_symbol(symbolt &)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
jsil_typecheckt(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
void typecheck_expr_proto_field(exprt &expr)
virtual ~jsil_typecheckt()
void typecheck_type(typet &type)
void make_type_compatible(exprt &expr, const typet &type, bool must)
void typecheck_expr_unary_string(exprt &expr)
void typecheck_block(codet &code)
symbol_table_baset & symbol_table
Base class for all expressions.
Definition: expr.h:54
Author: Diffblue Ltd.
void typecheck_expr_operands(exprt &expr)
The symbol table base class interface.
bool jsil_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)
codet representation of an if-then-else statement.
Definition: std_code.h:614
Expression to hold a symbol (variable)
Definition: std_expr.h:143
void typecheck_expr_delete(exprt &expr)
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
codet representation of a "return from a function" statement.
Definition: std_code.h:1191
void typecheck_expr_binary_compare(exprt &expr)
void typecheck_ifthenelse(code_ifthenelset &code)
void typecheck_expr_field(exprt &expr)
A codet representing an assignment in the program.
Definition: std_code.h:256
void typecheck_expr_has_field(exprt &expr)
std::unordered_set< irep_idt > already_typechecked
void typecheck_try_catch(code_try_catcht &code)
virtual void typecheck()
void update_expr_type(exprt &expr, const typet &type)
void typecheck_expr_index(exprt &expr)