cprover
Loading...
Searching...
No Matches
java_bytecode_typecheck_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JAVA Bytecode Conversion / Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#include <util/cprover_prefix.h>
15#include <util/pointer_expr.h>
16#include <util/prefix.h>
17#include <util/std_code.h>
18
19#include "java_pointer_casts.h"
21
23{
24 if(expr.id()==ID_code)
25 return typecheck_code(to_code(expr));
26
27 if(expr.id()==ID_typecast &&
28 expr.type().id()==ID_pointer)
30 expr,
31 to_pointer_type(expr.type()),
32 ns);
33
34 // do operands recursively
35 Forall_operands(it, expr)
36 typecheck_expr(*it);
37
40 "String literals should have been converted to constant globals "
41 "before typecheck_expr");
42
43 if(expr.id()==ID_symbol)
45 else if(expr.id()==ID_side_effect)
46 {
47 const irep_idt &statement=to_side_effect_expr(expr).get_statement();
48 if(statement==ID_java_new)
50 else if(statement==ID_java_new_array)
52 }
53}
54
56{
57 PRECONDITION(expr.operands().empty());
58 typet &type=expr.type();
59 typecheck_type(type);
60}
61
64{
65 PRECONDITION(expr.operands().size()>=1); // one per dimension
66 typet &type=expr.type();
67 typecheck_type(type);
68}
69
71{
72 irep_idt identifier=expr.get_identifier();
73
74 // does it exist already in the destination symbol table?
75 symbol_tablet::symbolst::const_iterator s_it=
76 symbol_table.symbols.find(identifier);
77
78 if(s_it==symbol_table.symbols.end())
79 {
81 has_prefix(id2string(identifier), "java::") ||
82 has_prefix(id2string(identifier), CPROVER_PREFIX));
83
84 // no, create the symbol
85 symbolt new_symbol;
86 new_symbol.name=identifier;
87 new_symbol.type=expr.type();
88 new_symbol.base_name=expr.get(ID_C_base_name);
89 new_symbol.pretty_name=id2string(identifier).substr(6, std::string::npos);
90 new_symbol.mode=ID_java;
91 new_symbol.is_type=false;
92
93 if(new_symbol.type.id()==ID_code)
94 {
95 new_symbol.is_lvalue=false;
96 }
97 else
98 {
99 new_symbol.is_lvalue=true;
100 }
101
102 if(symbol_table.add(new_symbol))
103 {
104 error() << "failed to add expression symbol to symbol table" << eom;
105 throw 0;
106 }
107 }
108 else
109 {
110 // yes!
111 INVARIANT(!s_it->second.is_type, "symbol identifier should not be a type");
112
113 const symbolt &symbol=s_it->second;
114
115 // type the expression
116 expr.type()=symbol.type;
117 }
118}
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
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
const irep_idt & id() const
Definition: irep.h:396
void typecheck_expr_java_new(side_effect_exprt &)
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_java_new_array(side_effect_exprt &)
symbol_table_baset & symbol_table
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
An expression containing a side effect.
Definition: std_code.h:1450
const irep_idt & get_statement() const
Definition: std_code.h:1472
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_type
Definition: symbol.h:61
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
bool is_lvalue
Definition: symbol.h:66
irep_idt mode
Language mode.
Definition: symbol.h:49
The type of an expression, extends irept.
Definition: type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
#define Forall_operands(it, expr)
Definition: expr.h:25
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
JAVA Bytecode Language Type Checking.
exprt make_clean_pointer_cast(const exprt &rawptr, const pointer_typet &target_type, const namespacet &ns)
JAVA Pointer Casts.
Representation of a constant Java string.
bool can_cast_expr< java_string_literal_exprt >(const exprt &base)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1506
const codet & to_code(const exprt &expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189