CBMC: /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_entry_point.cpp Source File

48 void create_java_initialize(symbol_table_baset &symbol_table)

49{

50 // If __CPROVER_initialize already exists, replace it. It may already exist

51 // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend.

52 symbol_table.remove(INITIALIZE_FUNCTION);

53

54 symbolt initialize{

55 INITIALIZE_FUNCTION, java_method_typet({}, java_void_type()), ID_java};

56 initialize.base_name=INITIALIZE_FUNCTION;

57

58 symbol_table.add(initialize);

59}

61 static bool should_init_symbol(const symbolt &sym)

62{

63 if(sym.type.id()!=ID_code &&

64 sym.is_lvalue &&

65 sym.is_state_var &&

66 sym.is_static_lifetime &&

67 sym.mode==ID_java)

68 {

69 // Consider some sort of annotation indicating a global variable that

70 // doesn't require initialisation?

71 return !sym.type.get_bool(ID_C_no_initialization_required);

72 }

73

74 return is_java_string_literal_id(sym.name);

75}

77 irep_idt get_java_class_literal_initializer_signature()

78{

79 static irep_idt signature =

80 "java::java.lang.Class.cproverInitializeClassLiteral:"

81 "(Ljava/lang/String;ZZZZZZZ)V";

82 return signature;

83}

90 static const symbolt *get_class_literal_initializer(

91 const symbolt &symbol,

92 const symbol_table_baset &symbol_table)

93{

94 if(symbol.value.is_not_nil())

95 return nullptr;

96 if(symbol.type != struct_tag_typet("java::java.lang.Class"))

97 return nullptr;

98 if(!has_suffix(id2string(symbol.name), JAVA_CLASS_MODEL_SUFFIX))

99 return nullptr;

100 return symbol_table.lookup(get_java_class_literal_initializer_signature());

101}

103 static constant_exprt constant_bool(bool val)

104{

105 return from_integer(val ? 1 : 0, java_boolean_type());

106}

108 static std::unordered_set<irep_idt> init_symbol(

109 const symbolt &sym,

110 code_blockt &code_block,

111 symbol_table_baset &symbol_table,

112 const source_locationt &source_location,

113 bool assume_init_pointers_not_null,

114 const java_object_factory_parameterst &object_factory_parameters,

115 const select_pointer_typet &pointer_type_selector,

116 bool string_refinement_enabled,

117 message_handlert &message_handler)

118{

119 std::unordered_set<irep_idt> additional_symbols;

120

121 if(

122 const symbolt *class_literal_init_method =

123 get_class_literal_initializer(sym, symbol_table))

124 {

125 const std::string &name_str = id2string(sym.name);

126 irep_idt class_name =

127 name_str.substr(0, name_str.size() - strlen(JAVA_CLASS_MODEL_SUFFIX));

128 const symbolt &class_symbol = symbol_table.lookup_ref(class_name);

129

130 bool class_is_array = is_java_array_tag(sym.name);

131

132 journalling_symbol_tablet journalling_table =

133 journalling_symbol_tablet::wrap(symbol_table);

134

135 symbol_exprt class_name_literal = get_or_create_string_literal_symbol(

136 to_class_type(class_symbol.type).get_tag(),

137 journalling_table,

138 string_refinement_enabled);

139

140 // If that created any new symbols make sure we initialise those too:

141 additional_symbols = journalling_table.get_inserted();

142

143 // Call the literal initializer method instead of a nondet initializer:

144

145 // For arguments we can't parse yet:

146 side_effect_expr_nondett nondet_bool(java_boolean_type(), sym.location);

147

148 const auto &java_class_type = to_java_class_type(class_symbol.type);

149

150 // Argument order is: name, isAnnotation, isArray, isInterface,

151 // isSynthetic, isLocalClass, isMemberClass, isEnum

152

153 code_function_callt initializer_call(

154 class_literal_init_method->symbol_expr(),

155 {// this:

156 address_of_exprt(sym.symbol_expr()),

157 // name:

158 address_of_exprt(class_name_literal),

159 // isAnnotation:

160 constant_bool(java_class_type.get_is_annotation()),

161 // isArray:

162 constant_bool(class_is_array),

163 // isInterface:

164 constant_bool(java_class_type.get_interface()),

165 // isSynthetic:

166 constant_bool(java_class_type.get_synthetic()),

167 // isLocalClass:

168 nondet_bool,

169 // isMemberClass:

170 nondet_bool,

171 // isEnum:

172 constant_bool(java_class_type.get_is_enumeration())});

173

174 // First initialize the object as prior to a constructor:

175 namespacet ns(symbol_table);

176

177 auto zero_object = zero_initializer(sym.type, source_locationt(), ns);

178 if(!zero_object.has_value())

179 {

180 messaget message(message_handler);

181 message.error() << "failed to zero-initialize " << sym.name

182 << messaget::eom;

183 throw 0;

184 }

185 set_class_identifier(

186 to_struct_expr(*zero_object), ns, to_struct_tag_type(sym.type));

187

188 code_block.add(

189 std::move(code_frontend_assignt(sym.symbol_expr(), *zero_object)));

190

191 // Then call the init function:

192 code_block.add(std::move(initializer_call));

193 }

194 else if(sym.value.is_nil() && sym.type != java_void_type())

195 {

196 const bool is_class_model = has_suffix(id2string(sym.name), "@class_model");

197 const bool not_allow_null = is_java_string_literal_id(sym.name) ||

198 is_non_null_library_global(sym.name) ||

199 assume_init_pointers_not_null;

200

201 java_object_factory_parameterst parameters = object_factory_parameters;

202 if(not_allow_null && !is_class_model)

203 parameters.min_null_tree_depth = 1;

204

205 gen_nondet_init(

206 sym.symbol_expr(),

207 code_block,

208 symbol_table,

209 source_location,

210 false,

211 lifetimet::STATIC_GLOBAL,

212 parameters,

213 pointer_type_selector,

214 update_in_placet::NO_UPDATE_IN_PLACE,

215 message_handler);

216 }

217 else if(sym.value.is_not_nil())

218 {

219 code_frontend_assignt assignment(sym.symbol_expr(), sym.value);

220 assignment.add_source_location() = source_location;

221 code_block.add(assignment);

222 }

223

224 return additional_symbols;

225}

227 void java_static_lifetime_init(

228 symbol_table_baset &symbol_table,

229 const source_locationt &source_location,

230 bool assume_init_pointers_not_null,

231 java_object_factory_parameterst object_factory_parameters,

232 const select_pointer_typet &pointer_type_selector,

233 bool string_refinement_enabled,

234 message_handlert &message_handler)

235{

236 symbolt &initialize_symbol =

237 symbol_table.get_writeable_ref(INITIALIZE_FUNCTION);

238 PRECONDITION(initialize_symbol.value.is_nil());

239 code_blockt code_block;

240

241 const symbol_exprt rounding_mode =

242 symbol_table.lookup_ref(rounding_mode_identifier()).symbol_expr();

243 code_block.add(code_frontend_assignt{rounding_mode,

244 from_integer(0, rounding_mode.type())});

245

246 object_factory_parameters.function_id = initialize_symbol.name;

247

248 // If there are strings given using --string-input-value, we need to add

249 // them to the symbol table now, so that they appear in __CPROVER_initialize

250 // and we can refer to them later when we initialize input values.

251 for(const auto &val : object_factory_parameters.string_input_values)

252 {

253 // We ignore the return value of the following call, we just need to

254 // make sure the string is in the symbol table.

255 get_or_create_string_literal_symbol(

256 val, symbol_table, string_refinement_enabled);

257 }

258

259 // We need to zero out all static variables, or nondet-initialize if they're

260 // external. Iterate over a copy of the symtab, as its iterators are

261 // invalidated by object_factory:

262

263 // sort alphabetically for reproducible results

264 std::set<std::string> symbol_names;

265 for(const auto &entry : symbol_table.symbols)

266 symbol_names.insert(id2string(entry.first));

267

268 std::set<std::string> additional_symbols;

269 while(!symbol_names.empty() || !additional_symbols.empty())

270 {

271 if(!additional_symbols.empty())

272 symbol_names.swap(additional_symbols);

273

274 for(const auto &symbol_name : symbol_names)

275 {

276 const symbolt &sym = symbol_table.lookup_ref(symbol_name);

277 if(should_init_symbol(sym))

278 {

279 auto new_symbols = init_symbol(

280 sym,

281 code_block,

282 symbol_table,

283 source_location,

284 assume_init_pointers_not_null,

285 object_factory_parameters,

286 pointer_type_selector,

287 string_refinement_enabled,

288 message_handler);

289 for(const auto &new_symbol_name : new_symbols)

290 additional_symbols.insert(id2string(new_symbol_name));

291 }

292 }

293

294 symbol_names.clear();

295 }

296

297 initialize_symbol.value = std::move(code_block);

298}

305 bool is_java_main(const symbolt &function)

306{

307 bool named_main = has_suffix(id2string(function.name), JAVA_MAIN_METHOD);

308 const java_method_typet &function_type = to_java_method_type(function.type);

309 const auto string_array_type = java_type_from_string("[Ljava/lang/String;");

310 // checks whether the function is static and has a single String[] parameter

311 bool is_static = !function_type.has_this();

312 // this should be implied by the signature

313 const java_method_typet::parameterst &parameters = function_type.parameters();

314 bool has_correct_type = function_type.return_type().id() == ID_empty &&

315 parameters.size() == 1 &&

316 parameters[0].type().full_eq(*string_array_type);

317 bool public_access = function_type.get(ID_access) == ID_public;

318 return named_main && is_static && has_correct_type && public_access;

319}

321 std::pair<code_blockt, std::vector<exprt>> java_build_arguments(

322 const symbolt &function,

323 symbol_table_baset &symbol_table,

324 bool assume_init_pointers_not_null,

325 java_object_factory_parameterst object_factory_parameters,

326 const select_pointer_typet &pointer_type_selector,

327 message_handlert &message_handler)

328{

329 const java_method_typet &function_type = to_java_method_type(function.type);

330 const java_method_typet::parameterst &parameters = function_type.parameters();

331

332 code_blockt init_code;

333 exprt::operandst main_arguments;

334 main_arguments.resize(parameters.size());

335

336 // certain method arguments cannot be allowed to be null, we set the following

337 // variable to true iff the method under test is the "main" method, which will

338 // be called (by the jvm) with arguments that are never null

339 bool is_main = is_java_main(function);

340

341 // we iterate through all the parameters of the function under test, allocate

342 // an object for that parameter (recursively allocating other objects

343 // necessary to initialize it), and mark such object using `code_inputt`.

344 for(std::size_t param_number=0;

345 param_number<parameters.size();

346 param_number++)

347 {

348 const java_method_typet::parametert &p = parameters[param_number];

349 const irep_idt base_name=p.get_base_name().empty()?

350 ("argument#"+std::to_string(param_number)):p.get_base_name();

351

352 // true iff this parameter is the `this` pointer of the method, which cannot

353 // be null

354 bool is_this=(param_number==0) && parameters[param_number].get_this();

355

356 if(is_this && function_type.get_is_constructor())

357 {

358 const symbol_exprt result = fresh_java_symbol(

359 p.type(),

360 "this_parameter",

361 function.location,

362 function.name,

363 symbol_table)

364 .symbol_expr();

365 main_arguments[param_number] = result;

366 init_code.add(code_declt{result});

367 init_code.add(code_frontend_assignt{

368 result,

369 side_effect_exprt{ID_java_new, {}, p.type(), function.location}});

370 continue;

371 }

372

373 java_object_factory_parameterst factory_parameters =

374 object_factory_parameters;

375 // only pointer must be non-null

376 if(assume_init_pointers_not_null || is_this)

377 factory_parameters.min_null_tree_depth = 1;

378 // in main() also the array elements of the argument must be non-null

379 if(is_main)

380 factory_parameters.min_null_tree_depth = 2;

381

382 factory_parameters.function_id = goto_functionst::entry_point();

383

384 namespacet ns(symbol_table);

385

386 // Generate code to allocate and non-deterministicaly initialize the

387 // argument, if the argument has different possible object types (e.g., from

388 // casts in the function body), then choose one in a non-deterministic way.

389 const auto alternatives =

390 pointer_type_selector.get_parameter_alternative_types(

391 function.name, p.get_identifier(), ns);

392 if(alternatives.empty())

393 {

394 main_arguments[param_number] = object_factory(

395 p.type(),

396 base_name,

397 init_code,

398 symbol_table,

399 factory_parameters,

400 lifetimet::DYNAMIC,

401 function.location,

402 pointer_type_selector,

403 message_handler);

404 }

405 else

406 {

407 INVARIANT(!is_this, "We cannot have different types for `this` here");

408 // create a non-deterministic switch between all possible values for the

409 // type of the parameter.

410

411 // the idea is to get a new symbol for the parameter value `tmp`

412

413 // then add a non-deterministic switch over all possible input types,

414 // construct the object type at hand and assign to `tmp`

415

416 // switch(...)

417 // {

418 // case obj1:

419 // tmp_expr = object_factory(...)

420 // param = tmp_expr

421 // break

422 // ...

423 // }

424 // method(..., param, ...)

425 //

426

427 const symbolt result_symbol = fresh_java_symbol(

428 p.type(),

429 "nondet_parameter_" + std::to_string(param_number),

430 function.location,

431 function.name,

432 symbol_table);

433 main_arguments[param_number] = result_symbol.symbol_expr();

434

435 std::vector<codet> cases;

436 cases.reserve(alternatives.size());

437 for(const auto &type : alternatives)

438 {

439 code_blockt init_code_for_type;

440 exprt init_expr_for_parameter = object_factory(

441 java_reference_type(type),

442 id2string(base_name) + "_alternative_" +

443 id2string(type.get_identifier()),

444 init_code_for_type,

445 symbol_table,

446 factory_parameters,

447 lifetimet::DYNAMIC,

448 function.location,

449 pointer_type_selector,

450 message_handler);

451 init_code_for_type.add(code_frontend_assignt(

452 result_symbol.symbol_expr(),

453 typecast_exprt(init_expr_for_parameter, p.type())));

454 cases.push_back(init_code_for_type);

455 }

456

457 init_code.add(

458 generate_nondet_switch(

459 id2string(function.name) + "_" + std::to_string(param_number),

460 cases,

461 java_int_type(),

462 ID_java,

463 function.location,

464 symbol_table));

465 }

466

467 // record as an input

468 init_code.add(

469 code_inputt{base_name, main_arguments[param_number], function.location});

470 }

471

472 return make_pair(init_code, main_arguments);

473}

476 static code_blockt java_record_outputs(

477 const symbolt &function,

478 const exprt::operandst &main_arguments,

479 symbol_table_baset &symbol_table)

480{

481 code_blockt init_code;

482

483 if(auto return_value = record_return_value(function, symbol_table))

484 {

485 init_code.add(std::move(*return_value));

486 }

487

488 init_code.append(

489 record_pointer_parameters(function, main_arguments, symbol_table));

490

491 init_code.add(record_exception(function, symbol_table));

492

493 return init_code;

494}

496 static std::optional<codet> record_return_value(

497 const symbolt &function,

498 const symbol_table_baset &symbol_table)

499{

500 if(to_java_method_type(function.type).return_type() == java_void_type())

501 return {};

502

503 const symbolt &return_symbol =

504 symbol_table.lookup_ref(JAVA_ENTRY_POINT_RETURN_SYMBOL);

505

506 return code_outputt{

507 return_symbol.base_name, return_symbol.symbol_expr(), function.location};

508}

510 static code_blockt record_pointer_parameters(

511 const symbolt &function,

512 const std::vector<exprt> &arguments,

513 const symbol_table_baset &symbol_table)

514{

515 const java_method_typet::parameterst &parameters =

516 to_java_method_type(function.type).parameters();

517

518 code_blockt init_code;

519

520 for(std::size_t param_number = 0; param_number < parameters.size();

521 param_number++)

522 {

523 const symbolt &p_symbol =

524 symbol_table.lookup_ref(parameters[param_number].get_identifier());

525

526 if(!can_cast_type<pointer_typet>(p_symbol.type))

527 continue;

528

529 init_code.add(code_outputt{

530 p_symbol.base_name, arguments[param_number], function.location});

531 }

532 return init_code;

533}

535 static codet record_exception(

536 const symbolt &function,

537 const symbol_table_baset &symbol_table)

538{

539 // retrieve the exception variable

540 const symbolt &exc_symbol =

541 symbol_table.lookup_ref(JAVA_ENTRY_POINT_EXCEPTION_SYMBOL);

542

543 // record exceptional return variable as output

544 return code_outputt{

545 exc_symbol.base_name, exc_symbol.symbol_expr(), function.location};

546}

548 main_function_resultt get_main_symbol(

549 const symbol_table_baset &symbol_table,

550 const irep_idt &main_class,

551 message_handlert &message_handler)

552{

553 messaget message(message_handler);

554

555 // find main symbol

556 if(config.main.has_value())

557 {

558 std::string error_message;

559 irep_idt main_symbol_id = resolve_friendly_method_name(

560 config.main.value(), symbol_table, error_message);

561

562 if(main_symbol_id.empty())

563 {

564 message.error()

565 << "main symbol resolution failed: " << error_message << messaget::eom;

566 return main_function_resultt::Error;

567 }

568

569 const symbolt *symbol = symbol_table.lookup(main_symbol_id);

570 INVARIANT(

571 symbol != nullptr,

572 "resolve_friendly_method_name should return a symbol-table identifier");

573

574 return *symbol; // Return found function

575 }

576 else

577 {

578 // are we given a main class?

579 if(main_class.empty())

580 {

581 // no, but we allow this situation to output symbol table,

582 // goto functions, etc

583 return main_function_resultt::NotFound;

584 }

585

586 std::string entry_method =

587 "java::" + id2string(main_class) + "." + JAVA_MAIN_METHOD;

588 const symbolt *symbol = symbol_table.lookup(entry_method);

589

590 // has the class a correct main method?

591 if(!symbol || !is_java_main(*symbol))

592 {

593 // no, but we allow this situation to output symbol table,

594 // goto functions, etc

595 return main_function_resultt::NotFound;

596 }

597

598 return *symbol;

599 }

600}

602 bool java_entry_point(

603 symbol_table_baset &symbol_table,

604 const irep_idt &main_class,

605 message_handlert &message_handler,

606 bool assume_init_pointers_not_null,

607 bool assert_uncaught_exceptions,

608 const java_object_factory_parameterst &object_factory_parameters,

609 const select_pointer_typet &pointer_type_selector,

610 bool string_refinement_enabled,

611 const build_argumentst &build_arguments)

612{

613 // check if the entry point is already there

614 if(symbol_table.symbols.find(goto_functionst::entry_point())!=

615 symbol_table.symbols.end())

616 return false; // silently ignore

617

618 messaget message(message_handler);

619 main_function_resultt res=

620 get_main_symbol(symbol_table, main_class, message_handler);

621 if(!res.is_success())

622 return true;

623 symbolt symbol=res.main_function;

624

625 DATA_INVARIANT(symbol.type.id() == ID_code, "expected code-typed symbol");

626

627 return generate_java_start_function(

628 symbol,

629 symbol_table,

630 message_handler,

631 assert_uncaught_exceptions,

632 object_factory_parameters,

633 pointer_type_selector,

634 build_arguments);

635}

637 bool generate_java_start_function(

638 const symbolt &symbol,

639 symbol_table_baset &symbol_table,

640 message_handlert &message_handler,

641 bool assert_uncaught_exceptions,

642 const java_object_factory_parameterst &object_factory_parameters,

643 const select_pointer_typet &pointer_type_selector,

644 const build_argumentst &build_arguments)

645{

646 messaget message(message_handler);

647 code_blockt init_code;

648

649 // build call to initialization function

650 {

651 symbol_table_baset::symbolst::const_iterator init_it =

652 symbol_table.symbols.find(INITIALIZE_FUNCTION);

653

654 if(init_it==symbol_table.symbols.end())

655 {

656 message.error() << "failed to find " INITIALIZE_FUNCTION " symbol"

657 << messaget::eom;

658 return true; // give up with error

659 }

660

661 code_function_callt call_init(init_it->second.symbol_expr());

662 call_init.add_source_location()=symbol.location;

663

664 init_code.add(std::move(call_init));

665 }

666

667 // build call to the main method, of the form

668 // return = main_method(arg1, arg2, ..., argn)

669 // where return is a new variable

670 // and arg1 ... argn are constructed below as well

671

672 source_locationt loc=symbol.location;

673 loc.set_function(symbol.name);

674 source_locationt &dloc=loc;

675

676 // function to call

677 code_function_callt call_main(symbol.symbol_expr());

678 call_main.add_source_location()=dloc;

679 call_main.function().add_source_location()=dloc;

680

681 // if the method return type is not void, store return value in a new variable

682 // named 'return'

683 if(to_java_method_type(symbol.type).return_type() != java_void_type())

684 {

685 auxiliary_symbolt return_symbol;

686 return_symbol.mode=ID_java;

687 return_symbol.is_static_lifetime=false;

688 return_symbol.name=JAVA_ENTRY_POINT_RETURN_SYMBOL;

689 return_symbol.base_name = "return'";

690 return_symbol.type = to_java_method_type(symbol.type).return_type();

691

692 symbol_table.add(return_symbol);

693 call_main.lhs()=return_symbol.symbol_expr();

694 }

695

696 // add the exceptional return value

697 auxiliary_symbolt exc_symbol;

698 exc_symbol.mode=ID_java;

699 exc_symbol.name=JAVA_ENTRY_POINT_EXCEPTION_SYMBOL;

700 exc_symbol.base_name=exc_symbol.name;

701 exc_symbol.type = java_reference_type(java_void_type());

702 symbol_table.add(exc_symbol);

703

704 // Zero-initialise the top-level exception catch variable:

705 init_code.add(code_frontend_assignt(

706 exc_symbol.symbol_expr(),

707 null_pointer_exprt(to_pointer_type(exc_symbol.type))));

708

709 // create code that allocates the objects used as test arguments and

710 // non-deterministically initializes them

711 const std::pair<code_blockt, std::vector<exprt>> main_arguments =

712 build_arguments(symbol, symbol_table);

713 init_code.append(main_arguments.first);

714 call_main.arguments() = main_arguments.second;

715

716 // Create target labels for the toplevel exception handler:

717 code_labelt toplevel_catch("toplevel_catch", code_skipt());

718 code_labelt after_catch("after_catch", code_skipt());

719

720 code_blockt call_block;

721

722 // Push a universal exception handler:

723 // Catch all exceptions:

724 // This is equivalent to catching Throwable, but also works if some of

725 // the class hierarchy is missing so that we can't determine that

726 // the thrown instance is an indirect child of Throwable

727 code_push_catcht push_universal_handler(

728 irep_idt(), toplevel_catch.get_label());

729 irept catch_type_list(ID_exception_list);

730 irept catch_target_list(ID_label);

731

732 call_block.add(std::move(push_universal_handler));

733

734 // we insert the call to the method AFTER the argument initialization code

735 call_block.add(std::move(call_main));

736

737 // Pop the handler:

738 code_pop_catcht pop_handler;

739 call_block.add(std::move(pop_handler));

740 init_code.add(std::move(call_block));

741

742 // Normal return: skip the exception handler:

743 init_code.add(code_gotot(after_catch.get_label()));

744

745 // Exceptional return: catch and assign to exc_symbol.

746 code_landingpadt landingpad(exc_symbol.symbol_expr());

747 init_code.add(std::move(toplevel_catch));

748 init_code.add(std::move(landingpad));

749

750 // Converge normal and exceptional return:

751 init_code.add(std::move(after_catch));

752

753 // Mark return value, pointer type parameters and the exception as outputs.

754 init_code.append(

755 java_record_outputs(symbol, main_arguments.second, symbol_table));

756

757 // add uncaught-exception check if requested

758 if(assert_uncaught_exceptions)

759 {

760 java_bytecode_instrument_uncaught_exceptions(

761 init_code, exc_symbol, symbol.location);

762 }

763

764 // create a symbol for the __CPROVER__start function, associate the code that

765 // we just built and register it in the symbol table

766 symbolt new_symbol{

767 goto_functionst::entry_point(),

768 java_method_typet{{}, java_void_type()},

769 ID_java};

770 new_symbol.base_name = goto_functionst::entry_point();

771 new_symbol.value.swap(init_code);

772

773 if(!symbol_table.insert(std::move(new_symbol)).second)

774 {

775 message.error() << "failed to move main symbol" << messaget::eom;

776 return true;

777 }

778

779 return false;

780}

rounding_mode_identifier

irep_idt rounding_mode_identifier()

Return the identifier of the program symbol used to store the current rounding mode.

Definition adjust_float_expressions.cpp:24

adjust_float_expressions.h

Symbolic Execution.

lifetimet::DYNAMIC

@ DYNAMIC

Allocate dynamic objects (using ALLOCATE)

lifetimet::STATIC_GLOBAL

@ STATIC_GLOBAL

Allocate global objects with static lifetime.

config

configt config

Definition config.cpp:25

from_integer

constant_exprt from_integer(const mp_integer &int_value, const typet &type)

Definition arith_tools.cpp:100

result_symbol

static symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_table_baset &symbol_table)

Definition c_typecheck_gcc_polymorphic_builtins.cpp:610

set_class_identifier

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.

Definition class_identifier.cpp:83

class_identifier.h

Extract class identifier.

ai_baset::clear

virtual void clear()

Reset the abstract state.

Definition ai.h:269

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

auxiliary_symbolt

Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...

Definition symbol.h:153

code_blockt

A codet representing sequential composition of program statements.

Definition std_code.h:130

code_declt

A goto_instruction_codet representing the declaration of a local variable.

Definition goto_instruction_code.h:204

code_frontend_assignt

A codet representing an assignment in the program.

Definition std_code.h:24

code_function_callt

goto_instruction_codet representation of a function call statement.

Definition goto_instruction_code.h:271

code_gotot

codet representation of a goto statement.

Definition std_code.h:841

code_inputt

A goto_instruction_codet representing the declaration that an input of a particular description has a...

Definition goto_instruction_code.h:407

code_labelt

codet representation of a label for branch targets.

Definition std_code.h:959

code_landingpadt

A statement that catches an exception, assigning the exception in flight to an expression (e....

Definition std_code.h:1936

code_outputt

A goto_instruction_codet representing the declaration that an output of a particular description has ...

Definition goto_instruction_code.h:454

code_pop_catcht

Pops an exception handler from the stack of active handlers (i.e.

Definition std_code.h:1899

code_push_catcht

Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....

Definition std_code.h:1805

code_skipt

A codet representing a skip statement.

Definition std_code.h:322

code_typet::parametert

Definition std_types.h:599

code_typet::parametert::get_base_name

const irep_idt & get_base_name() const

Definition std_types.h:638

code_typet::parametert::get_identifier

const irep_idt & get_identifier() const

Definition std_types.h:633

code_typet::has_this

bool has_this() const

Definition std_types.h:659

code_typet::parameters

const parameterst & parameters() const

Definition std_types.h:698

code_typet::return_type

const typet & return_type() const

Definition std_types.h:688

code_typet::get_is_constructor

bool get_is_constructor() const

Definition std_types.h:728

codet

Data structure for representing an arbitrary statement in a program.

Definition std_code_base.h:29

configt::main

std::optional< std::string > main

Definition config.h:391

constant_exprt

A constant literal expression.

Definition std_expr.h:3007

dstringt

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

Definition dstring.h:38

dstringt::empty

bool empty() const

Definition dstring.h:101

exprt

Base class for all expressions.

Definition expr.h:57

exprt::operandst

std::vector< exprt > operandst

Definition expr.h:59

exprt::type

typet & type()

Return the type of the expression.

Definition expr.h:85

exprt::add_source_location

source_locationt & add_source_location()

Definition expr.h:241

goto_functionst::entry_point

static irep_idt entry_point()

Get the identifier of the entry point to a goto model.

Definition goto_functions.h:97

irept

There are a large number of kinds of tree structured or tree-like data in CPROVER.

Definition irep.h:364

irept::get

const irep_idt & get(const irep_idt &name) const

Definition irep.cpp:44

irept::is_not_nil

bool is_not_nil() const

Definition irep.h:372

irept::id

const irep_idt & id() const

Definition irep.h:388

java_method_typet

Definition java_types.h:100

java_method_typet::parameterst

std::vector< parametert > parameterst

Definition std_types.h:585

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:37

journalling_symbol_tablet::wrap

static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)

Definition journalling_symbol_table.h:81

message_handlert

Definition message.h:27

messaget

Class that provides messages with a built-in verbosity 'level'.

Definition message.h:154

messaget::error

mstreamt & error() const

Definition message.h:401

messaget::eom

static eomt eom

Definition message.h:289

namespacet

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...

Definition namespace.h:91

null_pointer_exprt

The null pointer constant.

Definition pointer_expr.h:909

select_pointer_typet

Definition select_pointer_type.h:23

select_pointer_typet::get_parameter_alternative_types

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.

Definition select_pointer_type.cpp:84

side_effect_expr_nondett

A side_effect_exprt that returns a non-deterministically chosen value.

Definition std_code.h:1520

side_effect_exprt

An expression containing a side effect.

Definition std_code.h:1450

source_locationt

Definition source_location.h:20

source_locationt::set_function

void set_function(const irep_idt &function)

Definition source_location.h:135

struct_tag_typet

A struct tag type, i.e., struct_typet with an identifier.

Definition std_types.h:492

symbol_exprt

Expression to hold a symbol (variable)

Definition std_expr.h:132

symbol_table_baset

The symbol table base class interface.

Definition symbol_table_base.h:23

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:149

symbol_table_baset::remove

bool remove(const irep_idt &name)

Remove a symbol from the symbol table.

Definition symbol_table_base.cpp:27

symbol_table_baset::lookup

const symbolt * lookup(const irep_idt &name) const

Find a symbol in the symbol table for read-only access.

Definition symbol_table_base.h:96

symbol_table_baset::insert

virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0

Move or copy a new symbol to the symbol table.

symbol_table_baset::symbols

const symbolst & symbols

Read-only field, used to look up symbols given their names.

Definition symbol_table_base.h:31

symbol_table_baset::add

bool add(const symbolt &symbol)

Add a new symbol to the symbol table.

Definition symbol_table_base.cpp:18

symbol_table_baset::lookup_ref

const symbolt & lookup_ref(const irep_idt &name) const

Find a symbol in the symbol table for read-only access.

Definition symbol_table_base.h:105

symbolt

Symbol table entry.

Definition symbol.h:28

symbolt::location

source_locationt location

Source code location of definition of symbol.

Definition symbol.h:37

symbolt::symbol_expr

class symbol_exprt symbol_expr() const

Produces a symbol_exprt for a symbol.

Definition symbol.cpp:121

symbolt::type

typet type

Type of symbol.

Definition symbol.h:31

symbolt::name

irep_idt name

The unique identifier.

Definition symbol.h:40

symbolt::value

exprt value

Initial value of symbol.

Definition symbol.h:34

typecast_exprt

Semantic type conversion.

Definition std_expr.h:1995

config.h

zero_initializer

std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)

Create the equivalent of zero for type type.

Definition expr_initializer.cpp:308

expr_initializer.h

Expression Initialization.

goto_functions.h

Goto Programs with Functions.

id2string

const std::string & id2string(const irep_idt &d)

Definition irep.h:44

java_bytecode_instrument_uncaught_exceptions

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...

Definition java_bytecode_instrument.cpp:567

java_bytecode_instrument.h

java_bytecode_language.h

JAVA_CLASS_MODEL_SUFFIX

#define JAVA_CLASS_MODEL_SUFFIX

Definition java_bytecode_language.h:257

java_record_outputs

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.

Definition java_entry_point.cpp:476

java_entry_point

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__...

Definition java_entry_point.cpp:602

is_java_main

bool is_java_main(const symbolt &function)

Checks whether the given symbol is a valid java main method i.e.

Definition java_entry_point.cpp:305

record_return_value

static std::optional< codet > record_return_value(const symbolt &function, const symbol_table_baset &symbol_table)

Definition java_entry_point.cpp:496

JAVA_MAIN_METHOD

#define JAVA_MAIN_METHOD

Definition java_entry_point.cpp:33

constant_bool

static constant_exprt constant_bool(bool val)

Definition java_entry_point.cpp:103

create_java_initialize

void create_java_initialize(symbol_table_baset &symbol_table)

Adds __cprover_initialize to the symbol_table but does not generate code for it yet.

Definition java_entry_point.cpp:48

should_init_symbol

static bool should_init_symbol(const symbolt &sym)

Definition java_entry_point.cpp:61

record_exception

static codet record_exception(const symbolt &function, const symbol_table_baset &symbol_table)

Definition java_entry_point.cpp:535

generate_java_start_function

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.

Definition java_entry_point.cpp:637

java_static_lifetime_init

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.

Definition java_entry_point.cpp:227

record_pointer_parameters

static code_blockt record_pointer_parameters(const symbolt &function, const std::vector< exprt > &arguments, const symbol_table_baset &symbol_table)

Definition java_entry_point.cpp:510

get_main_symbol

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.

Definition java_entry_point.cpp:548

get_java_class_literal_initializer_signature

irep_idt get_java_class_literal_initializer_signature()

Get the symbol name of java.lang.Class' initializer method.

Definition java_entry_point.cpp:77

init_symbol

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)

Definition java_entry_point.cpp:108

java_build_arguments

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)

Definition java_entry_point.cpp:321

get_class_literal_initializer

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...

Definition java_entry_point.cpp:90

java_entry_point.h

JAVA_ENTRY_POINT_RETURN_SYMBOL

#define JAVA_ENTRY_POINT_RETURN_SYMBOL

Definition java_entry_point.h:21

JAVA_ENTRY_POINT_EXCEPTION_SYMBOL

#define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL

Definition java_entry_point.h:22

build_argumentst

std::function< std::pair< code_blockt, std::vector< exprt > >(const symbolt &function, symbol_table_baset &symbol_table)> build_argumentst

Definition java_entry_point.h:27

gen_nondet_init

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...

Definition java_object_factory.cpp:1621

object_factory

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...

Definition java_object_factory.cpp:1544

java_object_factory.h

This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...

update_in_placet::NO_UPDATE_IN_PLACE

@ NO_UPDATE_IN_PLACE

get_or_create_string_literal_symbol

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.

Definition java_string_literals.cpp:36

java_string_literals.h

java_int_type

signedbv_typet java_int_type()

Definition java_types.cpp:31

java_void_type

empty_typet java_void_type()

Definition java_types.cpp:37

java_type_from_string

std::optional< 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.

Definition java_types.cpp:561

java_reference_type

reference_typet java_reference_type(const typet &subtype)

Definition java_types.cpp:88

java_boolean_type

c_bool_typet java_boolean_type()

Definition java_types.cpp:79

is_java_array_tag

bool is_java_array_tag(const irep_idt &tag)

See above.

Definition java_types.cpp:233

java_types.h

to_java_method_type

const java_method_typet & to_java_method_type(const typet &type)

Definition java_types.h:183

to_java_class_type

const java_class_typet & to_java_class_type(const typet &type)

Definition java_types.h:581

is_java_string_literal_id

bool is_java_string_literal_id(const irep_idt &id)

Definition java_utils.cpp:207

is_non_null_library_global

bool is_non_null_library_global(const irep_idt &symbolid)

Check if a symbol is a well-known non-null global.

Definition java_utils.cpp:519

resolve_friendly_method_name

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...

Definition java_utils.cpp:212

fresh_java_symbol

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)

Definition java_utils.cpp:555

java_utils.h

journalling_symbol_table.h

Author: Diffblue Ltd.

generate_nondet_switch

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

nondet.h

to_pointer_type

const pointer_typet & to_pointer_type(const typet &type)

Cast a typet to a pointer_typet.

Definition pointer_expr.h:93

DATA_INVARIANT

#define DATA_INVARIANT(CONDITION, REASON)

This condition should be used to document that assumptions that are made on goto_functions,...

Definition invariant.h:534

PRECONDITION

#define PRECONDITION(CONDITION)

Definition invariant.h:463

INVARIANT

#define INVARIANT(CONDITION, REASON)

This macro uses the wrapper function 'invariant_violated_string'.

Definition invariant.h:423

message.h

static_lifetime_init.h

INITIALIZE_FUNCTION

#define INITIALIZE_FUNCTION

Definition static_lifetime_init.h:24

to_struct_expr

const struct_exprt & to_struct_expr(const exprt &expr)

Cast an exprt to a struct_exprt.

Definition std_expr.h:1843

to_struct_tag_type

const struct_tag_typet & to_struct_tag_type(const typet &type)

Cast a typet to a struct_tag_typet.

Definition std_types.h:517

to_class_type

const class_typet & to_class_type(const typet &type)

Cast a typet to a class_typet.

Definition std_types.h:380

strlen

size_t strlen(const char *s)

Definition string.c:561

java_object_factory_parameterst

Definition java_object_factory_parameters.h:16

main_function_resultt

Definition java_entry_point.h:89

main_function_resultt::NotFound

@ NotFound

Definition java_entry_point.h:94

main_function_resultt::Error

@ Error

Definition java_entry_point.h:93

object_factory_parameterst::function_id

irep_idt function_id

Function id, used as a prefix for identifiers of temporaries.

Definition object_factory_parameters.h:79

object_factory_parameterst::string_input_values

std::list< std::string > string_input_values

Force one of finitely many explicitly given input strings.

Definition object_factory_parameters.h:76

object_factory_parameterst::min_null_tree_depth

size_t min_null_tree_depth

To force a certain depth of non-null objects.

Definition object_factory_parameters.h:70

suffix.h

has_suffix

bool has_suffix(const std::string &s, const std::string &suffix)

Definition suffix.h:17

irep_idt

dstringt irep_idt

Definition verification_result.h:16