cprover
java_bytecode_typecheck_expr.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/arith_tools.h>
15 #include <util/expr_initializer.h>
16 #include <util/unicode.h>
17 
18 #include "java_pointer_casts.h"
19 #include "java_types.h"
20 #include "java_utils.h"
21 #include "java_root_class.h"
23 
25 {
26  if(expr.id()==ID_code)
27  return typecheck_code(to_code(expr));
28 
29  if(expr.id()==ID_typecast &&
30  expr.type().id()==ID_pointer)
32  expr,
33  to_pointer_type(expr.type()),
34  ns);
35 
36  // do operands recursively
37  Forall_operands(it, expr)
38  typecheck_expr(*it);
39 
40  INVARIANT(
41  expr.id() != ID_java_string_literal,
42  "String literals should have been converted to constant globals "
43  "before typecheck_expr");
44 
45  if(expr.id()==ID_symbol)
47  else if(expr.id()==ID_side_effect)
48  {
49  const irep_idt &statement=to_side_effect_expr(expr).get_statement();
50  if(statement==ID_java_new)
52  else if(statement==ID_java_new_array)
54  }
55  else if(expr.id()==ID_member)
57 }
58 
60 {
61  PRECONDITION(expr.operands().empty());
62  typet &type=expr.type();
63  typecheck_type(type);
64 }
65 
67  side_effect_exprt &expr)
68 {
69  PRECONDITION(expr.operands().size()>=1); // one per dimension
70  typet &type=expr.type();
71  typecheck_type(type);
72 }
73 
75 {
76  irep_idt identifier=expr.get_identifier();
77 
78  // does it exist already in the destination symbol table?
79  symbol_tablet::symbolst::const_iterator s_it=
80  symbol_table.symbols.find(identifier);
81 
82  if(s_it==symbol_table.symbols.end())
83  {
85  has_prefix(id2string(identifier), "java::") ||
86  has_prefix(id2string(identifier), CPROVER_PREFIX));
87 
88  // no, create the symbol
89  symbolt new_symbol;
90  new_symbol.name=identifier;
91  new_symbol.type=expr.type();
92  new_symbol.base_name=expr.get(ID_C_base_name);
93  new_symbol.pretty_name=id2string(identifier).substr(6, std::string::npos);
94  new_symbol.mode=ID_java;
95  new_symbol.is_type=false;
96 
97  if(new_symbol.type.id()==ID_code)
98  {
99  new_symbol.is_lvalue=false;
100  }
101  else
102  {
103  new_symbol.is_lvalue=true;
104  }
105 
106  if(symbol_table.add(new_symbol))
107  {
108  error() << "failed to add expression symbol to symbol table" << eom;
109  throw 0;
110  }
111  }
112  else
113  {
114  // yes!
115  INVARIANT(!s_it->second.is_type, "symbol identifier should not be a type");
116 
117  const symbolt &symbol=s_it->second;
118 
119  // type the expression
120  expr.type()=symbol.type;
121  }
122 }
123 
125 {
126  // The member might be in a parent class or an opaque class, which we resolve
127  // here.
128  const irep_idt component_name=expr.get_component_name();
129 
130  while(1)
131  {
132  typet base_type(ns.follow(expr.struct_op().type()));
133 
134  if(base_type.id()!=ID_struct)
135  break; // give up
136 
137  struct_typet &struct_type=
139 
140  if(struct_type.has_component(component_name))
141  return; // done
142 
143  // look at parent
144  struct_typet::componentst &components=
145  struct_type.components();
146 
147  if(components.empty())
148  break;
149 
150  const struct_typet::componentt &c=components.front();
151 
152  member_exprt m(expr.struct_op(), c.get_name(), c.type());
154 
155  expr.struct_op()=m;
156  }
157 
159  warning() << "failed to find field `"
160  << component_name << "` in class hierarchy" << eom;
161 
162  // We replace by a non-det of same type
163  side_effect_expr_nondett nondet(expr.type(), expr.source_location());
164  expr.swap(nondet);
165 }
const irep_idt & get_name() const
Definition: std_types.h:132
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define CPROVER_PREFIX
irep_idt mode
Language mode.
Definition: symbol.h:49
const irep_idt & get_identifier() const
Definition: std_expr.h:176
std::vector< componentt > componentst
Definition: std_types.h:203
const componentst & components() const
Definition: std_types.h:205
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
typet & type()
Return the type of the expression.
Definition: expr.h:68
Symbol table entry.
Definition: symbol.h:27
Structure type, corresponds to C style structs.
Definition: std_types.h:276
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1620
Extract member of struct or union.
Definition: std_expr.h:3890
mstreamt & warning() const
Definition: message.h:391
JAVA Bytecode Language Type Checking.
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:259
symbol_table_baset & symbol_table
source_locationt source_location
Definition: message.h:236
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
mstreamt & error() const
Definition: message.h:386
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
void typecheck_expr_java_new_array(side_effect_exprt &)
virtual void typecheck_expr(exprt &expr)
const symbolst & symbols
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:215
static eomt eom
Definition: message.h:284
typet type
Type of symbol.
Definition: symbol.h:31
Base class for all expressions.
Definition: expr.h:54
const exprt & struct_op() const
Definition: std_expr.h:3931
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
JAVA Pointer Casts.
const source_locationt & source_location() const
Definition: expr.h:228
irep_idt get_component_name() const
Definition: std_expr.h:3915
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:135
void swap(irept &irep)
Definition: irep.h:303
#define Forall_operands(it, expr)
Definition: expr.h:26
source_locationt & add_source_location()
Definition: expr.h:233
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
bool is_type
Definition: symbol.h:61
An expression containing a side effect.
Definition: std_code.h:1560
void typecheck_expr_java_new(side_effect_exprt &)
operandst & operands()
Definition: expr.h:78
exprt make_clean_pointer_cast(const exprt &rawptr, const pointer_typet &target_type, const namespacet &ns)
const irep_idt & get_statement() const
Definition: std_code.h:1586
Produce code for simple implementation of String Java libraries.
bool is_lvalue
Definition: symbol.h:66