cprover
Loading...
Searching...
No Matches
java_entry_point.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "java_entry_point.h"
10
11#include <util/config.h>
14#include <util/suffix.h>
15
19
21
24#include "java_object_factory.h"
26#include "java_types.h"
27#include "java_utils.h"
28#include "nondet.h"
29
30#include <cstring>
31
32#define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V"
33
35 const symbolt &function,
36 const symbol_table_baset &symbol_table);
37
39 const symbolt &function,
40 const std::vector<exprt> &arguments,
41 const symbol_table_baset &symbol_table);
42
44 const symbolt &function,
45 const symbol_table_baset &symbol_table);
46
48{
49 // If __CPROVER_initialize already exists, replace it. It may already exist
50 // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend.
51 symbol_table.remove(INITIALIZE_FUNCTION);
52
53 symbolt initialize;
54 initialize.name=INITIALIZE_FUNCTION;
56 initialize.mode=ID_java;
57
58 initialize.type = java_method_typet({}, java_void_type());
59 symbol_table.add(initialize);
60}
61
62static bool should_init_symbol(const symbolt &sym)
63{
64 if(sym.type.id()!=ID_code &&
65 sym.is_lvalue &&
66 sym.is_state_var &&
67 sym.is_static_lifetime &&
68 sym.mode==ID_java)
69 {
70 // Consider some sort of annotation indicating a global variable that
71 // doesn't require initialisation?
72 return !sym.type.get_bool(ID_C_no_initialization_required);
73 }
74
75 return is_java_string_literal_id(sym.name);
76}
77
79{
80 static irep_idt signature =
81 "java::java.lang.Class.cproverInitializeClassLiteral:"
82 "(Ljava/lang/String;ZZZZZZZ)V";
83 return signature;
84}
85
92 const symbolt &symbol,
93 const symbol_table_baset &symbol_table)
94{
95 if(symbol.value.is_not_nil())
96 return nullptr;
97 if(symbol.type != struct_tag_typet("java::java.lang.Class"))
98 return nullptr;
100 return nullptr;
102}
103
105{
106 return from_integer(val ? 1 : 0, java_boolean_type());
107}
108
109static std::unordered_set<irep_idt> init_symbol(
110 const symbolt &sym,
112 symbol_table_baset &symbol_table,
113 const source_locationt &source_location,
115 const java_object_factory_parameterst &object_factory_parameters,
116 const select_pointer_typet &pointer_type_selector,
117 bool string_refinement_enabled,
118 message_handlert &message_handler)
119{
120 std::unordered_set<irep_idt> additional_symbols;
121
122 if(
124 get_class_literal_initializer(sym, symbol_table))
125 {
126 const std::string &name_str = id2string(sym.name);
127 irep_idt class_name =
128 name_str.substr(0, name_str.size() - strlen(JAVA_CLASS_MODEL_SUFFIX));
129 const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
130
132
135
139 string_refinement_enabled);
140
141 // If that created any new symbols make sure we initialise those too:
142 additional_symbols = journalling_table.get_inserted();
143
144 // Call the literal initializer method instead of a nondet initializer:
145
146 // For arguments we can't parse yet:
148
150
151 // Argument order is: name, isAnnotation, isArray, isInterface,
152 // isSynthetic, isLocalClass, isMemberClass, isEnum
153
155 class_literal_init_method->symbol_expr(),
156 {// this:
157 address_of_exprt(sym.symbol_expr()),
158 // name:
159 address_of_exprt(class_name_literal),
160 // isAnnotation:
161 constant_bool(java_class_type.get_is_annotation()),
162 // isArray:
163 constant_bool(class_is_array),
164 // isInterface:
165 constant_bool(java_class_type.get_interface()),
166 // isSynthetic:
167 constant_bool(java_class_type.get_synthetic()),
168 // isLocalClass:
169 nondet_bool,
170 // isMemberClass:
171 nondet_bool,
172 // isEnum:
173 constant_bool(java_class_type.get_is_enumeration())});
174
175 // First initialize the object as prior to a constructor:
176 namespacet ns(symbol_table);
177
179 if(!zero_object.has_value())
180 {
181 messaget message(message_handler);
182 message.error() << "failed to zero-initialize " << sym.name
183 << messaget::eom;
184 throw 0;
185 }
188
189 code_block.add(
190 std::move(code_frontend_assignt(sym.symbol_expr(), *zero_object)));
191
192 // Then call the init function:
193 code_block.add(std::move(initializer_call));
194 }
195 else if(sym.value.is_nil() && sym.type != java_void_type())
196 {
197 const bool is_class_model = has_suffix(id2string(sym.name), "@class_model");
198 const bool not_allow_null = is_java_string_literal_id(sym.name) ||
201
202 java_object_factory_parameterst parameters = object_factory_parameters;
204 parameters.min_null_tree_depth = 1;
205
207 sym.symbol_expr(),
209 symbol_table,
210 source_location,
211 false,
213 parameters,
214 pointer_type_selector,
216 message_handler);
217 }
218 else if(sym.value.is_not_nil())
219 {
220 code_frontend_assignt assignment(sym.symbol_expr(), sym.value);
221 assignment.add_source_location() = source_location;
222 code_block.add(assignment);
223 }
224
225 return additional_symbols;
226}
227
229 symbol_table_baset &symbol_table,
230 const source_locationt &source_location,
232 java_object_factory_parameterst object_factory_parameters,
233 const select_pointer_typet &pointer_type_selector,
234 bool string_refinement_enabled,
235 message_handlert &message_handler)
236{
239 PRECONDITION(initialize_symbol.value.is_nil());
241
242 const symbol_exprt rounding_mode =
244 code_block.add(code_frontend_assignt{rounding_mode,
245 from_integer(0, rounding_mode.type())});
246
247 object_factory_parameters.function_id = initialize_symbol.name;
248
249 // If there are strings given using --string-input-value, we need to add
250 // them to the symbol table now, so that they appear in __CPROVER_initialize
251 // and we can refer to them later when we initialize input values.
252 for(const auto &val : object_factory_parameters.string_input_values)
253 {
254 // We ignore the return value of the following call, we just need to
255 // make sure the string is in the symbol table.
257 val, symbol_table, string_refinement_enabled);
258 }
259
260 // We need to zero out all static variables, or nondet-initialize if they're
261 // external. Iterate over a copy of the symtab, as its iterators are
262 // invalidated by object_factory:
263
264 // sort alphabetically for reproducible results
265 std::set<std::string> symbol_names;
266 for(const auto &entry : symbol_table.symbols)
267 symbol_names.insert(id2string(entry.first));
268
269 std::set<std::string> additional_symbols;
270 while(!symbol_names.empty() || !additional_symbols.empty())
271 {
272 if(!additional_symbols.empty())
274
275 for(const auto &symbol_name : symbol_names)
276 {
277 const symbolt &sym = symbol_table.lookup_ref(symbol_name);
279 {
281 sym,
283 symbol_table,
284 source_location,
286 object_factory_parameters,
287 pointer_type_selector,
288 string_refinement_enabled,
289 message_handler);
290 for(const auto &new_symbol_name : new_symbols)
292 }
293 }
294
296 }
297
298 initialize_symbol.value = std::move(code_block);
299}
300
306bool is_java_main(const symbolt &function)
307{
309 const java_method_typet &function_type = to_java_method_type(function.type);
310 const auto string_array_type = java_type_from_string("[Ljava/lang/String;");
311 // checks whether the function is static and has a single String[] parameter
312 bool is_static = !function_type.has_this();
313 // this should be implied by the signature
314 const java_method_typet::parameterst &parameters = function_type.parameters();
315 bool has_correct_type = function_type.return_type().id() == ID_empty &&
316 parameters.size() == 1 &&
317 parameters[0].type().full_eq(*string_array_type);
318 bool public_access = function_type.get(ID_access) == ID_public;
319 return named_main && is_static && has_correct_type && public_access;
320}
321
322std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
323 const symbolt &function,
324 symbol_table_baset &symbol_table,
326 java_object_factory_parameterst object_factory_parameters,
327 const select_pointer_typet &pointer_type_selector,
328 message_handlert &message_handler)
329{
330 const java_method_typet &function_type = to_java_method_type(function.type);
331 const java_method_typet::parameterst &parameters = function_type.parameters();
332
335 main_arguments.resize(parameters.size());
336
337 // certain method arguments cannot be allowed to be null, we set the following
338 // variable to true iff the method under test is the "main" method, which will
339 // be called (by the jvm) with arguments that are never null
340 bool is_main = is_java_main(function);
341
342 // we iterate through all the parameters of the function under test, allocate
343 // an object for that parameter (recursively allocating other objects
344 // necessary to initialize it), and mark such object using `code_inputt`.
345 for(std::size_t param_number=0;
346 param_number<parameters.size();
347 param_number++)
348 {
349 const java_method_typet::parametert &p = parameters[param_number];
350 const irep_idt base_name=p.get_base_name().empty()?
351 ("argument#"+std::to_string(param_number)):p.get_base_name();
352
353 // true iff this parameter is the `this` pointer of the method, which cannot
354 // be null
355 bool is_this=(param_number==0) && parameters[param_number].get_this();
356
357 if(is_this && function_type.get_is_constructor())
358 {
359 const symbol_exprt result = fresh_java_symbol(
360 p.type(),
361 "this_parameter",
362 function.location,
363 function.name,
364 symbol_table)
365 .symbol_expr();
367 init_code.add(code_declt{result});
369 result,
370 side_effect_exprt{ID_java_new, {}, p.type(), function.location}});
371 continue;
372 }
373
375 object_factory_parameters;
376 // only pointer must be non-null
378 factory_parameters.min_null_tree_depth = 1;
379 // in main() also the array elements of the argument must be non-null
380 if(is_main)
381 factory_parameters.min_null_tree_depth = 2;
382
384
385 namespacet ns(symbol_table);
386
387 // Generate code to allocate and non-deterministicaly initialize the
388 // argument, if the argument has different possible object types (e.g., from
389 // casts in the function body), then choose one in a non-deterministic way.
390 const auto alternatives =
391 pointer_type_selector.get_parameter_alternative_types(
392 function.name, p.get_identifier(), ns);
393 if(alternatives.empty())
394 {
396 p.type(),
397 base_name,
398 init_code,
399 symbol_table,
402 function.location,
403 pointer_type_selector,
404 message_handler);
405 }
406 else
407 {
408 INVARIANT(!is_this, "We cannot have different types for `this` here");
409 // create a non-deterministic switch between all possible values for the
410 // type of the parameter.
411
412 // the idea is to get a new symbol for the parameter value `tmp`
413
414 // then add a non-deterministic switch over all possible input types,
415 // construct the object type at hand and assign to `tmp`
416
417 // switch(...)
418 // {
419 // case obj1:
420 // tmp_expr = object_factory(...)
421 // param = tmp_expr
422 // break
423 // ...
424 // }
425 // method(..., param, ...)
426 //
427
429 p.type(),
430 "nondet_parameter_" + std::to_string(param_number),
431 function.location,
432 function.name,
433 symbol_table);
435
436 std::vector<codet> cases;
437 cases.reserve(alternatives.size());
438 for(const auto &type : alternatives)
439 {
443 id2string(base_name) + "_alternative_" +
444 id2string(type.get_identifier()),
446 symbol_table,
449 function.location,
450 pointer_type_selector,
451 message_handler);
453 result_symbol.symbol_expr(),
455 cases.push_back(init_code_for_type);
456 }
457
458 init_code.add(
460 id2string(function.name) + "_" + std::to_string(param_number),
461 cases,
463 ID_java,
464 function.location,
465 symbol_table));
466 }
467
468 // record as an input
469 init_code.add(
470 code_inputt{base_name, main_arguments[param_number], function.location});
471 }
472
474}
475
478 const symbolt &function,
480 symbol_table_baset &symbol_table)
481{
483
484 if(auto return_value = record_return_value(function, symbol_table))
485 {
486 init_code.add(std::move(*return_value));
487 }
488
489 init_code.append(
490 record_pointer_parameters(function, main_arguments, symbol_table));
491
492 init_code.add(record_exception(function, symbol_table));
493
494 return init_code;
495}
496
498 const symbolt &function,
499 const symbol_table_baset &symbol_table)
500{
502 return {};
503
504 const symbolt &return_symbol =
506
507 return code_outputt{
508 return_symbol.base_name, return_symbol.symbol_expr(), function.location};
509}
510
512 const symbolt &function,
513 const std::vector<exprt> &arguments,
514 const symbol_table_baset &symbol_table)
515{
516 const java_method_typet::parameterst &parameters =
518
520
521 for(std::size_t param_number = 0; param_number < parameters.size();
522 param_number++)
523 {
524 const symbolt &p_symbol =
525 symbol_table.lookup_ref(parameters[param_number].get_identifier());
526
528 continue;
529
531 p_symbol.base_name, arguments[param_number], function.location});
532 }
533 return init_code;
534}
535
537 const symbolt &function,
538 const symbol_table_baset &symbol_table)
539{
540 // retrieve the exception variable
541 const symbolt &exc_symbol =
543
544 // record exceptional return variable as output
545 return code_outputt{
546 exc_symbol.base_name, exc_symbol.symbol_expr(), function.location};
547}
548
550 const symbol_table_baset &symbol_table,
551 const irep_idt &main_class,
552 message_handlert &message_handler)
553{
554 messaget message(message_handler);
555
556 // find main symbol
557 if(config.main.has_value())
558 {
559 std::string error_message;
561 config.main.value(), symbol_table, error_message);
562
563 if(main_symbol_id.empty())
564 {
565 message.error()
566 << "main symbol resolution failed: " << error_message << messaget::eom;
568 }
569
570 const symbolt *symbol = symbol_table.lookup(main_symbol_id);
571 INVARIANT(
572 symbol != nullptr,
573 "resolve_friendly_method_name should return a symbol-table identifier");
574
575 return *symbol; // Return found function
576 }
577 else
578 {
579 // are we given a main class?
580 if(main_class.empty())
581 {
582 // no, but we allow this situation to output symbol table,
583 // goto functions, etc
585 }
586
587 std::string entry_method =
588 "java::" + id2string(main_class) + "." + JAVA_MAIN_METHOD;
589 const symbolt *symbol = symbol_table.lookup(entry_method);
590
591 // has the class a correct main method?
592 if(!symbol || !is_java_main(*symbol))
593 {
594 // no, but we allow this situation to output symbol table,
595 // goto functions, etc
597 }
598
599 return *symbol;
600 }
601}
602
604 symbol_table_baset &symbol_table,
605 const irep_idt &main_class,
606 message_handlert &message_handler,
608 bool assert_uncaught_exceptions,
609 const java_object_factory_parameterst &object_factory_parameters,
610 const select_pointer_typet &pointer_type_selector,
611 bool string_refinement_enabled,
613{
614 // check if the entry point is already there
615 if(symbol_table.symbols.find(goto_functionst::entry_point())!=
616 symbol_table.symbols.end())
617 return false; // silently ignore
618
619 messaget message(message_handler);
621 get_main_symbol(symbol_table, main_class, message_handler);
622 if(!res.is_success())
623 return true;
624 symbolt symbol=res.main_function;
625
626 assert(symbol.type.id()==ID_code);
627
629 symbol,
630 symbol_table,
631 message_handler,
632 assert_uncaught_exceptions,
633 object_factory_parameters,
634 pointer_type_selector,
636}
637
639 const symbolt &symbol,
640 symbol_table_baset &symbol_table,
641 message_handlert &message_handler,
642 bool assert_uncaught_exceptions,
643 const java_object_factory_parameterst &object_factory_parameters,
644 const select_pointer_typet &pointer_type_selector,
646{
647 messaget message(message_handler);
649
650 // build call to initialization function
651 {
652 symbol_tablet::symbolst::const_iterator init_it=
653 symbol_table.symbols.find(INITIALIZE_FUNCTION);
654
655 if(init_it==symbol_table.symbols.end())
656 {
657 message.error() << "failed to find " INITIALIZE_FUNCTION " symbol"
658 << messaget::eom;
659 return true; // give up with error
660 }
661
662 code_function_callt call_init(init_it->second.symbol_expr());
663 call_init.add_source_location()=symbol.location;
664
665 init_code.add(std::move(call_init));
666 }
667
668 // build call to the main method, of the form
669 // return = main_method(arg1, arg2, ..., argn)
670 // where return is a new variable
671 // and arg1 ... argn are constructed below as well
672
673 source_locationt loc=symbol.location;
674 loc.set_function(symbol.name);
676
677 // function to call
679 call_main.add_source_location()=dloc;
680 call_main.function().add_source_location()=dloc;
681
682 // if the method return type is not void, store return value in a new variable
683 // named 'return'
685 {
688 return_symbol.is_static_lifetime=false;
690 return_symbol.base_name = "return'";
692
693 symbol_table.add(return_symbol);
694 call_main.lhs()=return_symbol.symbol_expr();
695 }
696
697 // add the exceptional return value
699 exc_symbol.mode=ID_java;
701 exc_symbol.base_name=exc_symbol.name;
703 symbol_table.add(exc_symbol);
704
705 // Zero-initialise the top-level exception catch variable:
707 exc_symbol.symbol_expr(),
709
710 // create code that allocates the objects used as test arguments and
711 // non-deterministically initializes them
712 const std::pair<code_blockt, std::vector<exprt>> main_arguments =
713 build_arguments(symbol, symbol_table);
714 init_code.append(main_arguments.first);
715 call_main.arguments() = main_arguments.second;
716
717 // Create target labels for the toplevel exception handler:
718 code_labelt toplevel_catch("toplevel_catch", code_skipt());
719 code_labelt after_catch("after_catch", code_skipt());
720
722
723 // Push a universal exception handler:
724 // Catch all exceptions:
725 // This is equivalent to catching Throwable, but also works if some of
726 // the class hierarchy is missing so that we can't determine that
727 // the thrown instance is an indirect child of Throwable
729 irep_idt(), toplevel_catch.get_label());
732
733 call_block.add(std::move(push_universal_handler));
734
735 // we insert the call to the method AFTER the argument initialization code
736 call_block.add(std::move(call_main));
737
738 // Pop the handler:
740 call_block.add(std::move(pop_handler));
741 init_code.add(std::move(call_block));
742
743 // Normal return: skip the exception handler:
744 init_code.add(code_gotot(after_catch.get_label()));
745
746 // Exceptional return: catch and assign to exc_symbol.
748 init_code.add(std::move(toplevel_catch));
749 init_code.add(std::move(landingpad));
750
751 // Converge normal and exceptional return:
752 init_code.add(std::move(after_catch));
753
754 // Mark return value, pointer type parameters and the exception as outputs.
755 init_code.append(
756 java_record_outputs(symbol, main_arguments.second, symbol_table));
757
758 // add uncaught-exception check if requested
759 if(assert_uncaught_exceptions)
760 {
762 init_code, exc_symbol, symbol.location);
763 }
764
765 // create a symbol for the __CPROVER__start function, associate the code that
766 // we just built and register it in the symbol table
767 symbolt new_symbol;
768
770 new_symbol.type = java_method_typet({}, java_void_type());
771 new_symbol.value.swap(init_code);
772 new_symbol.mode=ID_java;
773
774 if(!symbol_table.insert(std::move(new_symbol)).second)
775 {
776 message.error() << "failed to move main symbol" << messaget::eom;
777 return true;
778 }
779
780 return false;
781}
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
@ STATIC_GLOBAL
Allocate global objects with static lifetime.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_tablet &symbol_table)
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const struct_tag_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct.
Extract class identifier.
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition symbol.h:147
A codet representing sequential composition of program statements.
Definition std_code.h:130
A codet representing the declaration of a local variable.
A codet representing an assignment in the program.
Definition std_code.h:24
codet representation of a function call statement.
codet representation of a goto statement.
Definition std_code.h:841
A codet representing the declaration that an input of a particular description has a value which corr...
codet representation of a label for branch targets.
Definition std_code.h:959
A statement that catches an exception, assigning the exception in flight to an expression (e....
Definition std_code.h:1936
A codet representing the declaration that an output of a particular description has a value which cor...
Pops an exception handler from the stack of active handlers (i.e.
Definition std_code.h:1899
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
Definition std_code.h:1805
A codet representing a skip statement.
Definition std_code.h:322
const irep_idt & get_base_name() const
Definition std_types.h:595
const irep_idt & get_identifier() const
Definition std_types.h:590
bool has_this() const
Definition std_types.h:616
const parameterst & parameters() const
Definition std_types.h:655
const typet & return_type() const
Definition std_types.h:645
bool get_is_constructor() const
Definition std_types.h:685
Data structure for representing an arbitrary statement in a program.
optionalt< std::string > main
Definition config.h:326
A constant literal expression.
Definition std_expr.h:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:82
source_locationt & add_source_location()
Definition expr.h:235
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
bool is_not_nil() const
Definition irep.h:380
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
std::vector< parametert > parameterst
Definition std_types.h:542
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & error() const
Definition message.h:399
static eomt eom
Definition message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The null pointer constant.
virtual std::set< struct_tag_typet > get_parameter_alternative_types(const irep_idt &function_name, const irep_idt &parameter_name, const namespacet &ns) const
Get alternative types for a method parameter, e.g., based on the casts in the function body.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
An expression containing a side effect.
Definition std_code.h:1450
void set_function(const irep_idt &function)
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:449
irep_idt get_tag() const
Definition std_types.h:168
Expression to hold a symbol (variable)
Definition std_expr.h:80
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
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.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition symbol.h:28
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
exprt value
Initial value of symbol.
Definition symbol.h:34
irep_idt mode
Language mode.
Definition symbol.h:49
Semantic type conversion.
Definition std_expr.h:1920
configt config
Definition config.cpp:25
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
Goto Programs with Functions.
dstringt irep_idt
Definition irep.h:37
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
void java_bytecode_instrument_uncaught_exceptions(code_blockt &init_code, const symbolt &exc_symbol, const source_locationt &source_location)
Instruments the start function with an assertion that checks whether an exception has escaped the ent...
#define JAVA_CLASS_MODEL_SUFFIX
static optionalt< codet > record_return_value(const symbolt &function, const symbol_table_baset &symbol_table)
static code_blockt java_record_outputs(const symbolt &function, const exprt::operandst &main_arguments, symbol_table_baset &symbol_table)
Mark return value, pointer type parameters and the exception as outputs.
bool java_entry_point(symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, bool assert_uncaught_exceptions, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, const build_argumentst &build_arguments)
Given the symbol_table and the main_class to test, this function generates a new function __CPROVER__...
bool is_java_main(const symbolt &function)
Checks whether the given symbol is a valid java main method i.e.
#define JAVA_MAIN_METHOD
static constant_exprt constant_bool(bool val)
void create_java_initialize(symbol_table_baset &symbol_table)
Adds __cprover_initialize to the symbol_table but does not generate code for it yet.
static bool should_init_symbol(const symbolt &sym)
static codet record_exception(const symbolt &function, const symbol_table_baset &symbol_table)
bool generate_java_start_function(const symbolt &symbol, symbol_table_baset &symbol_table, message_handlert &message_handler, bool assert_uncaught_exceptions, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, const build_argumentst &build_arguments)
Generate a _start function for a specific function.
void java_static_lifetime_init(symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, java_object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
Adds the body to __CPROVER_initialize.
static code_blockt record_pointer_parameters(const symbolt &function, const std::vector< exprt > &arguments, const symbol_table_baset &symbol_table)
main_function_resultt get_main_symbol(const symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler)
Figures out the entry point of the code to verify.
irep_idt get_java_class_literal_initializer_signature()
Get the symbol name of java.lang.Class' initializer method.
static std::unordered_set< irep_idt > init_symbol(const symbolt &sym, code_blockt &code_block, symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
std::pair< code_blockt, std::vector< exprt > > java_build_arguments(const symbolt &function, symbol_table_baset &symbol_table, bool assume_init_pointers_not_null, java_object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)
static const symbolt * get_class_literal_initializer(const symbolt &symbol, const symbol_table_baset &symbol_table)
If symbol is a class literal, and an appropriate initializer method exists, return a pointer to its s...
#define JAVA_ENTRY_POINT_RETURN_SYMBOL
#define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL
std::function< std::pair< code_blockt, std::vector< exprt > >(const symbolt &function, symbol_table_baset &symbol_table)> build_argumentst
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place, message_handlert &log)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, lifetimet lifetime, const source_locationt &loc, const select_pointer_typet &pointer_type_selector, message_handlert &log)
Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing th...
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
symbol_exprt get_or_create_string_literal_symbol(const java_string_literal_exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates or gets an existing constant global symbol for a given string literal.
signedbv_typet java_int_type()
empty_typet java_void_type()
optionalt< typet > java_type_from_string(const std::string &src, const std::string &class_name_prefix)
Transforms a string representation of a Java type into an internal type representation thereof.
reference_typet java_reference_type(const typet &subtype)
c_bool_typet java_boolean_type()
bool is_java_array_tag(const irep_idt &tag)
See above.
const java_method_typet & to_java_method_type(const typet &type)
Definition java_types.h:184
const java_class_typet & to_java_class_type(const typet &type)
Definition java_types.h:582
bool is_java_string_literal_id(const irep_idt &id)
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
irep_idt resolve_friendly_method_name(const std::string &friendly_name, const symbol_table_baset &symbol_table, std::string &error)
Resolves a user-friendly method name (like packagename.Class.method) into an internal name (like java...
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
Author: Diffblue Ltd.
code_blockt generate_nondet_switch(const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table)
Pick nondeterministically between imperative actions 'switch_cases'.
Definition nondet.cpp:91
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define INITIALIZE_FUNCTION
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1745
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition std_types.h:381
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
std::list< std::string > string_input_values
Force one of finitely many explicitly given input strings.
size_t min_null_tree_depth
To force a certain depth of non-null objects.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17