cprover
java_bytecode_typecheck.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JAVA Bytecode Conversion / Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/std_types.h>
15 #include <util/prefix.h>
16 #include <util/config.h>
17 
18 #include "expr2java.h"
19 
21 {
22  return expr2java(expr, ns);
23 }
24 
26 {
27  return type2java(type, ns);
28 }
29 
31 {
32  assert(!symbol.is_type);
33  typecheck_type(symbol.type);
34  typecheck_expr(symbol.value);
35 }
36 
38 {
39  // The hash table iterators are not stable,
40  // and we might add new symbols.
42  identifiers.reserve(symbol_table.symbols.size());
43  for(const auto &symbol_pair : symbol_table.symbols)
44  identifiers.insert(symbol_pair.first);
45  typecheck(identifiers);
46 }
47 
49  const journalling_symbol_tablet::changesett &identifiers)
50 {
51  // We first check all type symbols,
52  // recursively doing base classes first.
53  for(const irep_idt &id : identifiers)
54  {
55  symbolt &symbol=*symbol_table.get_writeable(id);
56  if(symbol.is_type)
57  typecheck_type_symbol(symbol);
58  }
59  // We now check all non-type symbols
60  for(const irep_idt &id : identifiers)
61  {
62  symbolt &symbol=*symbol_table.get_writeable(id);
63  if(!symbol.is_type)
65  }
66 }
67 
69  symbol_table_baset &symbol_table,
70  message_handlert &message_handler,
71  bool string_refinement_enabled)
72 {
74  symbol_table, message_handler, string_refinement_enabled);
75  return java_bytecode_typecheck.typecheck_main();
76 }
77 
79  journalling_symbol_tablet &symbol_table,
80  message_handlert &message_handler,
81  bool string_refinement_enabled)
82 {
84  symbol_table, message_handler, string_refinement_enabled);
85  return java_bytecode_typecheck.typecheck(symbol_table.get_updated());
86 }
87 
89  exprt &expr,
90  message_handlert &message_handler,
91  const namespacet &ns)
92 {
93 #if 0
94  symbol_tablet symbol_table;
95  java_bytecode_parse_treet java_bytecode_parse_tree;
96 
98  java_bytecode_parse_tree, symbol_table,
99  "", message_handler);
100 
101  try
102  {
103  java_bytecode_typecheck.typecheck_expr(expr);
104  }
105 
106  catch(int e)
107  {
108  java_bytecode_typecheck.error();
109  }
110 
111  catch(const char *e)
112  {
113  java_bytecode_typecheck.error(e);
114  }
115 
116  catch(const std::string &e)
117  {
118  java_bytecode_typecheck.error(e);
119  }
120 
121  return java_bytecode_typecheck.get_error_found();
122 #else
123  // unused parameters
124  (void)expr;
125  (void)message_handler;
126  (void)ns;
127 #endif
128 
129  // fail for now
130  return true;
131 }
The type of an expression, extends irept.
Definition: type.h:27
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:448
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
exprt value
Initial value of symbol.
Definition: symbol.h:34
Symbol table entry.
Definition: symbol.h:27
virtual std::string to_string(const exprt &expr)
JAVA Bytecode Language Type Checking.
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
symbol_table_baset & symbol_table
const changesett & get_updated() const
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
virtual void typecheck_expr(exprt &expr)
const symbolst & symbols
typet type
Type of symbol.
Definition: symbol.h:31
Pre-defined types.
Base class for all expressions.
Definition: expr.h:54
The symbol table base class interface.
std::unordered_set< irep_idt > changesett
bool is_type
Definition: symbol.h:61
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:441