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 
17 #include "expr2java.h"
18 
20 {
21  return expr2java(expr, ns);
22 }
23 
25 {
26  return type2java(type, ns);
27 }
28 
30 {
31  assert(!symbol.is_type);
32  typecheck_type(symbol.type);
33  typecheck_expr(symbol.value);
34 }
35 
37 {
38  // The hash table iterators are not stable,
39  // and we might add new symbols.
41  identifiers.reserve(symbol_table.symbols.size());
42  for(const auto &symbol_pair : symbol_table.symbols)
43  identifiers.insert(symbol_pair.first);
44  typecheck(identifiers);
45 }
46 
48  const journalling_symbol_tablet::changesett &identifiers)
49 {
50  // We first check all type symbols,
51  // recursively doing base classes first.
52  for(const irep_idt &id : identifiers)
53  {
55  if(symbol.is_type)
56  typecheck_type_symbol(symbol);
57  }
58  // We now check all non-type symbols
59  for(const irep_idt &id : identifiers)
60  {
62  if(!symbol.is_type)
64  }
65 }
66 
68  symbol_table_baset &symbol_table,
69  message_handlert &message_handler,
70  bool string_refinement_enabled)
71 {
73  symbol_table, message_handler, string_refinement_enabled);
74  return java_bytecode_typecheck.typecheck_main();
75 }
76 
78  journalling_symbol_tablet &symbol_table,
79  message_handlert &message_handler,
80  bool string_refinement_enabled)
81 {
83  symbol_table, message_handler, string_refinement_enabled);
84  return java_bytecode_typecheck.typecheck(symbol_table.get_updated());
85 }
86 
88  exprt &expr,
89  message_handlert &message_handler,
90  const namespacet &ns)
91 {
92 #if 0
93  symbol_tablet symbol_table;
94  java_bytecode_parse_treet java_bytecode_parse_tree;
95 
97  java_bytecode_parse_tree, symbol_table,
98  "", message_handler);
99 
100  try
101  {
102  java_bytecode_typecheck.typecheck_expr(expr);
103  }
104 
105  catch(int e)
106  {
107  java_bytecode_typecheck.error();
108  }
109 
110  catch(const char *e)
111  {
112  java_bytecode_typecheck.error(e);
113  }
114 
115  catch(const std::string &e)
116  {
117  java_bytecode_typecheck.error(e);
118  }
119 
120  return java_bytecode_typecheck.get_error_found();
121 #else
122  // unused parameters
123  (void)expr;
124  (void)message_handler;
125  (void)ns;
126 #endif
127 
128  // fail for now
129  return true;
130 }
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
java_bytecode_parse_treet
Definition: java_bytecode_parse_tree.h:24
java_bytecode_typecheckt::to_string
virtual std::string to_string(const exprt &expr)
Definition: java_bytecode_typecheck.cpp:19
typet
The type of an expression, extends irept.
Definition: type.h:28
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
prefix.h
journalling_symbol_tablet::get_updated
const changesett & get_updated() const
Definition: journalling_symbol_table.h:150
exprt
Base class for all expressions.
Definition: expr.h:54
java_bytecode_typecheckt::typecheck_type
void typecheck_type(typet &)
Definition: java_bytecode_typecheck_type.cpp:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
java_bytecode_typecheckt::typecheck_type_symbol
void typecheck_type_symbol(symbolt &)
Definition: java_bytecode_typecheck_type.cpp:53
java_bytecode_typecheckt::ns
const namespacet ns
Definition: java_bytecode_typecheck.h:64
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
std_types.h
Pre-defined types.
journalling_symbol_tablet::changesett
std::unordered_set< irep_idt > changesett
Definition: journalling_symbol_table.h:38
java_bytecode_typecheck_updated_symbols
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
Definition: java_bytecode_typecheck.cpp:77
java_bytecode_typecheckt::symbol_table
symbol_table_baset & symbol_table
Definition: java_bytecode_typecheck.h:63
message_handlert
Definition: message.h:28
java_bytecode_typecheckt::typecheck_non_type_symbol
void typecheck_non_type_symbol(symbolt &)
Definition: java_bytecode_typecheck.cpp:29
java_bytecode_typecheckt::typecheck
virtual void typecheck()
Definition: java_bytecode_typecheck.cpp:36
java_bytecode_typecheckt
Definition: java_bytecode_typecheck.h:43
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbolt::is_type
bool is_type
Definition: symbol.h:61
type2java
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:461
expr2java
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:454
java_bytecode_typecheck
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
Definition: java_bytecode_typecheck.cpp:67
expr2java.h
journalling_symbol_tablet
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
Definition: journalling_symbol_table.h:36
java_bytecode_typecheck.h
JAVA Bytecode Language Type Checking.
java_bytecode_typecheckt::typecheck_expr
virtual void typecheck_expr(exprt &expr)
Definition: java_bytecode_typecheck_expr.cpp:26