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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
jsil_typecheckt::typecheck_expr_operands
void typecheck_expr_operands(exprt &expr)
Definition: jsil_typecheck.cpp:146
jsil_typecheckt::update_expr_type
void update_expr_type(exprt &expr, const typet &type)
Definition: jsil_typecheck.cpp:37
jsil_typecheckt::typecheck_expr_has_field
void typecheck_expr_has_field(exprt &expr)
Definition: jsil_typecheck.cpp:354
jsil_typecheckt::typecheck_expr_binary_compare
void typecheck_expr_binary_compare(exprt &expr)
Definition: jsil_typecheck.cpp:500
jsil_typecheckt::typecheck_expr_unary_string
void typecheck_expr_unary_string(exprt &expr)
Definition: jsil_typecheck.cpp:529
jsil_typecheckt::typecheck_expr_ref
void typecheck_expr_ref(exprt &expr)
Definition: jsil_typecheck.cpp:397
jsil_typecheckt::typecheck_function_call
void typecheck_function_call(code_function_callt &function_call)
Definition: jsil_typecheck.cpp:710
jsil_typecheckt::to_string
virtual std::string to_string(const exprt &expr)
Definition: jsil_typecheck.cpp:21
typet
The type of an expression, extends irept.
Definition: type.h:29
jsil_typecheckt::typecheck_assign
void typecheck_assign(code_assignt &code)
Definition: jsil_typecheck.cpp:824
jsil_typecheckt::typecheck_expr_base
void typecheck_expr_base(exprt &expr)
Definition: jsil_typecheck.cpp:383
code_try_catcht
codet representation of a try/catch block.
Definition: std_code.h:2429
jsil_typecheckt::typecheck_try_catch
void typecheck_try_catch(code_try_catcht &code)
Definition: jsil_typecheck.cpp:692
jsil_typecheckt
Definition: jsil_typecheck.h:35
jsil_typecheckt::typecheck_type
void typecheck_type(typet &type)
Definition: jsil_typecheck.cpp:99
jsil_typecheckt::~jsil_typecheckt
virtual ~jsil_typecheckt()
Definition: jsil_typecheck.h:47
jsil_typecheckt::typecheck_expr_index
void typecheck_expr_index(exprt &expr)
Definition: jsil_typecheck.cpp:333
exprt
Base class for all expressions.
Definition: expr.h:53
jsil_typecheckt::typecheck_code
void typecheck_code(codet &code)
Definition: jsil_typecheck.cpp:632
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
jsil_typecheckt::already_typechecked
std::unordered_set< irep_idt > already_typechecked
Definition: jsil_typecheck.h:98
jsil_typecheckt::typecheck_return
void typecheck_return(code_returnt &code)
Definition: jsil_typecheck.cpp:680
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
jsil_typecheckt::typecheck_expr_side_effect_throw
void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr)
Definition: jsil_typecheck.cpp:269
jsil_typecheckt::typecheck_expr_unary_num
void typecheck_expr_unary_num(exprt &expr)
Definition: jsil_typecheck.cpp:543
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
jsil_typecheckt::typecheck_non_type_symbol
void typecheck_non_type_symbol(symbolt &symbol)
typechecking procedure declaration; any other symbols should have been typechecked during typecheckin...
Definition: jsil_typecheck.cpp:835
jsil_typecheckt::typecheck_expr_main
void typecheck_expr_main(exprt &expr)
Definition: jsil_typecheck.cpp:152
typecheck.h
jsil_typecheckt::jsil_typecheckt
jsil_typecheckt(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
Definition: jsil_typecheck.h:37
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
jsil_typecheckt::typecheck_expr_unary_boolean
void typecheck_expr_unary_boolean(exprt &expr)
Definition: jsil_typecheck.cpp:515
jsil_typecheckt::typecheck_expr_proto_field
void typecheck_expr_proto_field(exprt &expr)
Definition: jsil_typecheck.cpp:288
jsil_typecheckt::typecheck_ifthenelse
void typecheck_ifthenelse(code_ifthenelset &code)
Definition: jsil_typecheck.cpp:812
message_handlert
Definition: message.h:28
jsil_typecheckt::typecheck_expr_proto_obj
void typecheck_expr_proto_obj(exprt &expr)
Definition: jsil_typecheck.cpp:303
jsil_typecheckt::typecheck_expr
virtual void typecheck_expr(exprt &expr)
Definition: jsil_typecheck.cpp:137
std_code.h
jsil_typecheckt::typecheck_expr_binary_boolean
void typecheck_expr_binary_boolean(exprt &expr)
Definition: jsil_typecheck.cpp:456
jsil_typecheckt::typecheck_symbol_expr
void typecheck_symbol_expr(symbol_exprt &symbol_expr)
Definition: jsil_typecheck.cpp:555
jsil_typecheckt::symbol_table
symbol_table_baset & symbol_table
Definition: jsil_typecheck.h:53
jsil_typecheckt::typecheck_expr_constant
void typecheck_expr_constant(exprt &expr)
Definition: jsil_typecheck.cpp:278
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
jsil_typecheckt::ns
const namespacet ns
Definition: jsil_typecheck.h:54
jsil_typecheckt::typecheck_type_symbol
void typecheck_type_symbol(symbolt &)
Definition: jsil_typecheck.h:60
jsil_typecheckt::typecheck_expr_concatenation
void typecheck_expr_concatenation(exprt &expr)
Definition: jsil_typecheck.cpp:426
symbolt
Symbol table entry.
Definition: symbol.h:28
jsil_typecheckt::typecheck_block
void typecheck_block(codet &code)
Definition: jsil_typecheck.cpp:686
jsil_typecheckt::proc_name
irep_idt proc_name
Definition: jsil_typecheck.h:56
jsil_typecheckt::typecheck_expr_binary_arith
void typecheck_expr_binary_arith(exprt &expr)
Definition: jsil_typecheck.cpp:471
side_effect_expr_throwt
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:2200
jsil_typecheck
bool jsil_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: jsil_typecheck.cpp:897
jsil_typecheckt::typecheck_expr_subtype
void typecheck_expr_subtype(exprt &expr)
Definition: jsil_typecheck.cpp:441
typecheckt
Definition: typecheck.h:17
jsil_typecheckt::typecheck
virtual void typecheck()
Definition: jsil_typecheck.cpp:867
jsil_typecheckt::typecheck_expr_field
void typecheck_expr_field(exprt &expr)
Definition: jsil_typecheck.cpp:369
symbol_table_base.h
Author: Diffblue Ltd.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
jsil_typecheckt::add_prefix
irep_idt add_prefix(const irep_idt &ds)
Prefix parameters and variables with a procedure name.
Definition: jsil_typecheck.cpp:32
jsil_typecheckt::typecheck_exp_binary_equal
void typecheck_exp_binary_equal(exprt &expr)
Definition: jsil_typecheck.cpp:486
jsil_typecheckt::make_type_compatible
void make_type_compatible(exprt &expr, const typet &type, bool must)
Definition: jsil_typecheck.cpp:60
jsil_typecheckt::typecheck_expr_delete
void typecheck_expr_delete(exprt &expr)
Definition: jsil_typecheck.cpp:318
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35