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/typecheck.h>
19 
20 class code_assignt;
22 class code_ifthenelset;
23 class code_returnt;
24 class code_try_catcht;
25 class codet;
26 class message_handlert;
28 class symbol_exprt;
29 class symbol_tablet;
30 
31 bool jsil_typecheck(
32  symbol_tablet &symbol_table,
33  message_handlert &message_handler);
34 
35 bool jsil_typecheck(
36  exprt &expr,
37  message_handlert &message_handler,
38  const namespacet &ns);
39 
41 {
42 public:
44  symbol_table_baset &_symbol_table,
45  message_handlert &_message_handler)
46  : typecheckt(_message_handler),
47  symbol_table(_symbol_table),
49  proc_name()
50  {
51  }
52 
53  virtual ~jsil_typecheckt() { }
54 
55  virtual void typecheck();
56  virtual void typecheck_expr(exprt &expr);
57 
58 protected:
60  const namespacet ns;
61  // prefix to variables which is set in typecheck_declaration
63 
64  void update_expr_type(exprt &expr, const typet &type);
65  void make_type_compatible(exprt &expr, const typet &type, bool must);
67  void typecheck_non_type_symbol(symbolt &symbol);
68  void typecheck_symbol_expr(symbol_exprt &symbol_expr);
70  void typecheck_expr_delete(exprt &expr);
71  void typecheck_expr_index(exprt &expr);
73  void typecheck_expr_proto_obj(exprt &expr);
74  void typecheck_expr_has_field(exprt &expr);
75  void typecheck_expr_ref(exprt &expr);
76  void typecheck_expr_field(exprt &expr);
77  void typecheck_expr_base(exprt &expr);
78  void typecheck_expr_constant(exprt &expr);
80  void typecheck_expr_subtype(exprt &expr);
87  void typecheck_expr_unary_num(exprt &expr);
88  void typecheck_expr_operands(exprt &expr);
89  void typecheck_expr_main(exprt &expr);
90  void typecheck_code(codet &code);
91  void typecheck_function_call(code_function_callt &function_call);
92  void typecheck_return(code_returnt &code);
93  void typecheck_block(codet &code);
95  void typecheck_assign(code_assignt &code);
97  void typecheck_type(typet &type);
98  irep_idt add_prefix(const irep_idt &ds);
99 
100  // overload to use language-specific syntax
101  virtual std::string to_string(const exprt &expr);
102  virtual std::string to_string(const typet &type);
103 
104  std::unordered_set<irep_idt> already_typechecked;
105 };
106 
107 #endif // CPROVER_JSIL_JSIL_TYPECHECK_H
A codet representing an assignment in the program.
Definition: std_code.h:293
codet representation of a function call statement.
Definition: std_code.h:1213
codet representation of an if-then-else statement.
Definition: std_code.h:776
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
codet representation of a try/catch block.
Definition: std_code.h:2432
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
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_return(code_returnt &code)
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)
const namespacet ns
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)
jsil_typecheckt(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
virtual void typecheck()
irep_idt proc_name
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)
std::unordered_set< irep_idt > already_typechecked
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)
virtual ~jsil_typecheckt()
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_expr_binary_compare(exprt &expr)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:2203
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:28
bool jsil_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)