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

51 void parse_java_language_options(const cmdlinet &cmd, optionst &options)

52{

53 options.set_option(

54 "java-assume-inputs-non-null", cmd.isset("java-assume-inputs-non-null"));

55 options.set_option(

56 "throw-runtime-exceptions", cmd.isset("throw-runtime-exceptions"));

57 options.set_option(

58 "uncaught-exception-check", !cmd.isset("disable-uncaught-exception-check"));

59 options.set_option(

60 "throw-assertion-error", cmd.isset("throw-assertion-error"));

61 options.set_option(

62 "assert-no-exceptions-thrown", cmd.isset("assert-no-exceptions-thrown"));

63 options.set_option("java-threading", cmd.isset("java-threading"));

64

65 if(cmd.isset("java-max-vla-length"))

66 {

67 options.set_option(

68 "java-max-vla-length", cmd.get_value("java-max-vla-length"));

69 }

70

71 options.set_option(

72 "symex-driven-lazy-loading", cmd.isset("symex-driven-lazy-loading"));

73

74 options.set_option(

75 "ignore-manifest-main-class", cmd.isset("ignore-manifest-main-class"));

76

77 if(cmd.isset("context-include"))

78 options.set_option("context-include", cmd.get_values("context-include"));

79

80 if(cmd.isset("context-exclude"))

81 options.set_option("context-exclude", cmd.get_values("context-exclude"));

82

83 if(cmd.isset("java-load-class"))

84 options.set_option("java-load-class", cmd.get_values("java-load-class"));

85

86 if(cmd.isset("java-no-load-class"))

87 {

88 options.set_option(

89 "java-no-load-class", cmd.get_values("java-no-load-class"));

90 }

91 if(cmd.isset("lazy-methods-extra-entry-point"))

92 {

93 options.set_option(

94 "lazy-methods-extra-entry-point",

95 cmd.get_values("lazy-methods-extra-entry-point"));

96 }

97 if(cmd.isset("java-cp-include-files"))

98 {

99 options.set_option(

100 "java-cp-include-files", cmd.get_value("java-cp-include-files"));

101 }

102 if(cmd.isset("static-values"))

103 {

104 options.set_option("static-values", cmd.get_value("static-values"));

105 }

106 options.set_option(

107 "java-lift-clinit-calls", cmd.isset("java-lift-clinit-calls"));

108

109 options.set_option("lazy-methods", !cmd.isset("no-lazy-methods"));

110}

112 prefix_filtert get_context(const optionst &options)

113{

114 std::vector<std::string> context_include;

115 std::vector<std::string> context_exclude;

116 for(const auto &include : options.get_list_option("context-include"))

117 context_include.push_back("java::" + include);

118 for(const auto &exclude : options.get_list_option("context-exclude"))

119 context_exclude.push_back("java::" + exclude);

120 return prefix_filtert(std::move(context_include), std::move(context_exclude));

121}

124 lazy_class_to_declared_symbols_mapt::get(const symbol_table_baset &symbol_table)

125{

126 if(!initialized)

127 {

128 map = class_to_declared_symbols(symbol_table);

129 initialized = true;

130 }

131 return map;

132}

134 void lazy_class_to_declared_symbols_mapt::reinitialize()

135{

136 initialized = false;

137 map.clear();

138}

140 java_bytecode_language_optionst::java_bytecode_language_optionst(

141 const optionst &options,

142 message_handlert &message_handler)

143{

144 assume_inputs_non_null =

145 options.get_bool_option("java-assume-inputs-non-null");

146 string_refinement_enabled = options.get_bool_option("refine-strings");

147 throw_runtime_exceptions =

148 options.get_bool_option("throw-runtime-exceptions");

149 assert_uncaught_exceptions =

150 options.get_bool_option("uncaught-exception-check");

151 throw_assertion_error = options.get_bool_option("throw-assertion-error");

152 assert_no_exceptions_thrown =

153 options.get_bool_option("assert-no-exceptions-thrown");

154 threading_support = options.get_bool_option("java-threading");

155 max_user_array_length =

156 options.get_unsigned_int_option("java-max-vla-length");

157

158 if(options.get_bool_option("symex-driven-lazy-loading"))

159 lazy_methods_mode=LAZY_METHODS_MODE_EXTERNAL_DRIVER;

160 else if(options.get_bool_option("lazy-methods"))

161 lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_INSENSITIVE;

162 else

163 lazy_methods_mode=LAZY_METHODS_MODE_EAGER;

164

165 if(throw_runtime_exceptions)

166 {

167 java_load_classes.insert(

168 java_load_classes.end(),

169 exception_needed_classes.begin(),

170 exception_needed_classes.end());

171 }

172

173 if(options.is_set("java-load-class"))

174 {

175 const auto &load_values = options.get_list_option("java-load-class");

176 java_load_classes.insert(

177 java_load_classes.end(), load_values.begin(), load_values.end());

178 }

179 if(options.is_set("java-no-load-class"))

180 {

181 const auto &no_load_values = options.get_list_option("java-no-load-class");

182 no_load_classes = {no_load_values.begin(), no_load_values.end()};

183 }

184 const std::list<std::string> &extra_entry_points =

185 options.get_list_option("lazy-methods-extra-entry-point");

186 std::transform(

187 extra_entry_points.begin(),

188 extra_entry_points.end(),

189 std::back_inserter(extra_methods),

190 build_load_method_by_regex);

191

192 java_cp_include_files = options.get_option("java-cp-include-files");

193 if(!java_cp_include_files.empty())

194 {

195 // load file list from JSON file

196 if(java_cp_include_files[0]=='@')

197 {

198 jsont json_cp_config;

199 if(parse_json(

200 java_cp_include_files.substr(1), message_handler, json_cp_config))

201 {

202 throw "cannot read JSON input configuration for JAR loading";

203 }

204

205 if(!json_cp_config.is_object())

206 throw "the JSON file has a wrong format";

207 jsont include_files=json_cp_config["jar"];

208 if(!include_files.is_array())

209 throw "the JSON file has a wrong format";

210

211 // add jars from JSON config file to classpath

212 for(const jsont &file_entry : to_json_array(include_files))

213 {

214 DATA_INVARIANT(

215 file_entry.is_string() && has_suffix(file_entry.value, ".jar"),

216 "classpath entry must be jar filename, but '" + file_entry.value +

217 "' found");

218 config.java.classpath.push_back(file_entry.value);

219 }

220 }

221 }

222 else

223 java_cp_include_files=".*";

224

225 nondet_static = options.get_bool_option("nondet-static");

226 if(options.is_set("static-values"))

227 {

228 const std::string filename = options.get_option("static-values");

229 jsont tmp_json;

230 messaget log{message_handler};

231 if(parse_json(filename, message_handler, tmp_json))

232 {

233 log.warning()

234 << "Provided JSON file for static-values cannot be parsed; it"

235 << " will be ignored." << messaget::eom;

236 }

237 else

238 {

239 if(!tmp_json.is_object())

240 {

241 log.warning() << "Provided JSON file for static-values is not a JSON "

242 << "object; it will be ignored." << messaget::eom;

243 }

244 else

245 static_values_json = std::move(to_json_object(tmp_json));

246 }

247 }

248

249 ignore_manifest_main_class =

250 options.get_bool_option("ignore-manifest-main-class");

251

252 if(options.is_set("context-include") || options.is_set("context-exclude"))

253 method_context = get_context(options);

254

255 should_lift_clinit_calls = options.get_bool_option("java-lift-clinit-calls");

256}

259 void java_bytecode_languaget::set_language_options(

260 const optionst &options,

261 message_handlert &message_handler)

262{

263 object_factory_parameters.set(options);

264 language_options = java_bytecode_language_optionst{options, message_handler};

265 const auto &new_points = build_extra_entry_points(options);

266 language_options->extra_methods.insert(

267 language_options->extra_methods.end(),

268 new_points.begin(),

269 new_points.end());

270}

272 std::set<std::string> java_bytecode_languaget::extensions() const

273{

274 return { "class", "jar" };

275}

277 void java_bytecode_languaget::modules_provided(std::set<std::string> &)

278{

279 // modules.insert(translation_unit(parse_path));

280}

283 bool java_bytecode_languaget::preprocess(

284 std::istream &,

285 const std::string &,

286 std::ostream &,

287 message_handlert &)

288{

289 // there is no preprocessing!

290 return true;

291}

293 void java_bytecode_languaget::initialize_class_loader(

294 message_handlert &message_handler)

295{

296 java_class_loader.clear_classpath();

297

298 for(const auto &p : config.java.classpath)

299 java_class_loader.add_classpath_entry(p, message_handler);

300

301 java_class_loader.set_java_cp_include_files(

302 language_options->java_cp_include_files);

303 java_class_loader.add_load_classes(language_options->java_load_classes);

304 if(language_options->string_refinement_enabled)

305 {

306 string_preprocess.initialize_known_type_table();

307

308 auto get_string_base_classes = [this](const irep_idt &id) {

309 return string_preprocess.get_string_type_base_classes(id);

310 };

311

312 java_class_loader.set_extra_class_refs_function(get_string_base_classes);

313 }

314}

316 static void throwMainClassLoadingError(const std::string &main_class)

317{

318 throw system_exceptiont(

319 "Error: Could not find or load main class " + main_class);

320}

322 void java_bytecode_languaget::parse_from_main_class(

323 message_handlert &message_handler)

324{

325 messaget log{message_handler};

326

327 if(!main_class.empty())

328 {

329 // Try to load class

330 log.status() << "Trying to load Java main class: " << main_class

331 << messaget::eom;

332 if(!java_class_loader.can_load_class(main_class, message_handler))

333 {

334 // Try to extract class name and load class

335 const auto maybe_class_name =

336 class_name_from_method_name(id2string(main_class));

337 if(!maybe_class_name)

338 {

339 throwMainClassLoadingError(id2string(main_class));

340 return;

341 }

342 log.status() << "Trying to load Java main class: "

343 << maybe_class_name.value() << messaget::eom;

344 if(!java_class_loader.can_load_class(

345 maybe_class_name.value(), message_handler))

346 {

347 throwMainClassLoadingError(id2string(main_class));

348 return;

349 }

350 // Everything went well. We have a loadable main class.

351 // The entry point ('main') will be checked later.

352 config.main = id2string(main_class);

353 main_class = maybe_class_name.value();

354 }

355 log.status() << "Found Java main class: " << main_class << messaget::eom;

356 // Now really load it.

357 const auto &parse_trees = java_class_loader(main_class, message_handler);

358 if(parse_trees.empty() || !parse_trees.front().loading_successful)

359 {

360 throwMainClassLoadingError(id2string(main_class));

361 }

362 }

363}

371 bool java_bytecode_languaget::parse(

372 std::istream &instream,

373 const std::string &path,

374 message_handlert &message_handler)

375{

376 PRECONDITION(language_options.has_value());

377 initialize_class_loader(message_handler);

378

379 // look at extension

380 if(has_suffix(path, ".jar"))

381 {

382 std::ifstream jar_file(path);

383 if(!jar_file.good())

384 {

385 throw system_exceptiont("Error: Unable to access jarfile " + path);

386 }

387

388 // build an object to potentially limit which classes are loaded

389 java_class_loader_limitt class_loader_limit(

390 message_handler, language_options->java_cp_include_files);

391 if(config.java.main_class.empty())

392 {

393 // If we have an entry method, we can derive a main class.

394 if(config.main.has_value())

395 {

396 const std::string &entry_method = config.main.value();

397 const auto last_dot_position = entry_method.find_last_of('.');

398 main_class = entry_method.substr(0, last_dot_position);

399 }

400 else

401 {

402 auto manifest = java_class_loader.jar_pool(path).get_manifest();

403 std::string manifest_main_class = manifest["Main-Class"];

404

405 // if the manifest declares a Main-Class line, we got a main class

406 if(

407 !manifest_main_class.empty() &&

408 !language_options->ignore_manifest_main_class)

409 {

410 main_class = manifest_main_class;

411 }

412 }

413 }

414 else

415 main_class=config.java.main_class;

416

417 // do we have one now?

418 if(main_class.empty())

419 {

420 messaget log{message_handler};

421 log.status() << "JAR file without entry point: loading class files"

422 << messaget::eom;

423 const auto classes =

424 java_class_loader.load_entire_jar(path, message_handler);

425 for(const auto &c : classes)

426 main_jar_classes.push_back(c);

427 }

428 else

429 java_class_loader.add_classpath_entry(path, message_handler);

430 }

431 else

432 main_class = config.java.main_class;

433

434 parse_from_main_class(message_handler);

435 return false;

436}

447 static void infer_opaque_type_fields(

448 const java_bytecode_parse_treet &parse_tree,

449 symbol_table_baset &symbol_table)

450{

451 namespacet ns(symbol_table);

452 for(const auto &method : parse_tree.parsed_class.methods)

453 {

454 for(const java_bytecode_parse_treet::instructiont &instruction :

455 method.instructions)

456 {

457 const std::string statement =

458 bytecode_info[instruction.bytecode].mnemonic;

459 if(statement == "getfield" || statement == "putfield")

460 {

461 const fieldref_exprt &fieldref =

462 expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);

463 irep_idt class_symbol_id = fieldref.class_name();

464 const symbolt *class_symbol = symbol_table.lookup(class_symbol_id);

465 INVARIANT(

466 class_symbol != nullptr,

467 "all types containing fields should have been loaded");

468

469 const java_class_typet *class_type =

470 &to_java_class_type(class_symbol->type);

471 const irep_idt &component_name = fieldref.component_name();

472 while(!class_type->has_component(component_name))

473 {

474 if(class_type->get_is_stub())

475 {

476 // Accessing a field of an incomplete (opaque) type.

477 symbolt &writable_class_symbol =

478 symbol_table.get_writeable_ref(class_symbol_id);

479 auto &components =

480 to_java_class_type(writable_class_symbol.type).components();

481 components.emplace_back(component_name, fieldref.type());

482 components.back().set_base_name(component_name);

483 components.back().set_pretty_name(component_name);

484 components.back().set_is_final(true);

485 break;

486 }

487 else

488 {

489 // Not present here: check the superclass.

490 INVARIANT(

491 !class_type->bases().empty(),

492 "class '" + id2string(class_symbol->name) +

493 "' (which was missing a field '" + id2string(component_name) +

494 "' referenced from method '" + id2string(method.name) +

495 "' of class '" + id2string(parse_tree.parsed_class.name) +

496 "') should have an opaque superclass");

497 const auto &superclass_type = class_type->bases().front().type();

498 class_symbol_id = superclass_type.get_identifier();

499 class_type = &to_java_class_type(

500 ns.follow_tag(to_struct_tag_type(superclass_type)));

501 }

502 }

503 }

504 }

505 }

506}

513 static symbol_exprt get_or_create_class_literal_symbol(

514 const irep_idt &class_id,

515 symbol_table_baset &symbol_table)

516{

517 struct_tag_typet java_lang_Class("java::java.lang.Class");

518 symbol_exprt symbol_expr(

519 id2string(class_id) + JAVA_CLASS_MODEL_SUFFIX,

520 java_lang_Class);

521 if(!symbol_table.has_symbol(symbol_expr.identifier()))

522 {

523 symbolt new_class_symbol{

524 symbol_expr.identifier(), symbol_expr.type(), ID_java};

525 INVARIANT(

526 new_class_symbol.name.starts_with("java::"),

527 "class identifier should have 'java::' prefix");

528 new_class_symbol.base_name =

529 id2string(new_class_symbol.name).substr(6);

530 new_class_symbol.is_lvalue = true;

531 new_class_symbol.is_state_var = true;

532 new_class_symbol.is_static_lifetime = true;

533 new_class_symbol.type.set(ID_C_no_nondet_initialization, true);

534 symbol_table.add(new_class_symbol);

535 }

536

537 return symbol_expr;

538}

554 static exprt get_ldc_result(

555 const exprt &ldc_arg0,

556 symbol_table_baset &symbol_table,

557 bool string_refinement_enabled)

558{

559 if(ldc_arg0.id() == ID_type)

560 {

561 const irep_idt &class_id = ldc_arg0.type().get(ID_identifier);

562 return

563 address_of_exprt(

564 get_or_create_class_literal_symbol(class_id, symbol_table));

565 }

566 else if(

567 const auto &literal =

568 expr_try_dynamic_cast<java_string_literal_exprt>(ldc_arg0))

569 {

570 return address_of_exprt(get_or_create_string_literal_symbol(

571 *literal, symbol_table, string_refinement_enabled));

572 }

573 else

574 {

575 INVARIANT(

576 ldc_arg0.is_constant(),

577 "ldc argument should be constant, string literal or class literal");

578 return ldc_arg0;

579 }

580}

591 static void generate_constant_global_variables(

592 java_bytecode_parse_treet &parse_tree,

593 symbol_table_baset &symbol_table,

594 bool string_refinement_enabled)

595{

596 for(auto &method : parse_tree.parsed_class.methods)

597 {

598 for(java_bytecode_parse_treet::instructiont &instruction :

599 method.instructions)

600 {

601 // ldc* instructions are Java bytecode "load constant" ops, which can

602 // retrieve a numeric constant, String literal, or Class literal.

603 const std::string statement =

604 bytecode_info[instruction.bytecode].mnemonic;

605 // clang-format off

606 if(statement == "ldc" ||

607 statement == "ldc2" ||

608 statement == "ldc_w" ||

609 statement == "ldc2_w")

610 {

611 // clang-format on

612 INVARIANT(

613 instruction.args.size() != 0,

614 "ldc instructions should have an argument");

615 instruction.args[0] =

616 get_ldc_result(

617 instruction.args[0],

618 symbol_table,

619 string_refinement_enabled);

620 }

621 }

622 }

623}

636 static void create_stub_global_symbol(

637 symbol_table_baset &symbol_table,

638 const irep_idt &symbol_id,

639 const irep_idt &symbol_basename,

640 const typet &symbol_type,

641 const irep_idt &class_id,

642 bool force_nondet_init)

643{

644 symbolt new_symbol{symbol_id, symbol_type, ID_java};

645 new_symbol.is_static_lifetime = true;

646 new_symbol.is_lvalue = true;

647 new_symbol.is_state_var = true;

648 new_symbol.base_name = symbol_basename;

649 set_declaring_class(new_symbol, class_id);

650 // Public access is a guess; it encourages merging like-typed static fields,

651 // whereas a more restricted visbility would encourage separating them.

652 // Neither is correct, as without the class file we can't know the truth.

653 new_symbol.type.set(ID_C_access, ID_public);

654 // We set the field as final to avoid assuming they can be overridden.

655 new_symbol.type.set(ID_C_constant, true);

656 new_symbol.pretty_name = new_symbol.name;

657 // If pointer-typed, initialise to null and a static initialiser will be

658 // created to initialise on first reference. If primitive-typed, specify

659 // nondeterministic initialisation by setting a nil value.

660 if(symbol_type.id() == ID_pointer && !force_nondet_init)

661 new_symbol.value = null_pointer_exprt(to_pointer_type(symbol_type));

662 else

663 new_symbol.value.make_nil();

664 bool add_failed = symbol_table.add(new_symbol);

665 INVARIANT(

666 !add_failed, "caller should have checked symbol not already in table");

667}

677 static irep_idt get_any_incomplete_ancestor_for_stub_static_field(

678 const irep_idt &start_class_id,

679 const symbol_table_baset &symbol_table,

680 const class_hierarchyt &class_hierarchy)

681{

682 // Depth-first search: return the first stub ancestor, or irep_idt() if none

683 // found.

684 std::vector<irep_idt> classes_to_check;

685 classes_to_check.push_back(start_class_id);

686

687 while(!classes_to_check.empty())

688 {

689 irep_idt to_check = classes_to_check.back();

690 classes_to_check.pop_back();

691

692 // Exclude java.lang.Object because it can

693 if(

694 to_java_class_type(symbol_table.lookup_ref(to_check).type)

695 .get_is_stub() &&

696 to_check != "java::java.lang.Object")

697 {

698 return to_check;

699 }

700

701 const class_hierarchyt::idst &parents =

702 class_hierarchy.class_map.at(to_check).parents;

703 classes_to_check.insert(

704 classes_to_check.end(), parents.begin(), parents.end());

705 }

706

707 return irep_idt();

708}

719 static void create_stub_global_symbols(

720 const java_bytecode_parse_treet &parse_tree,

721 symbol_table_baset &symbol_table,

722 const class_hierarchyt &class_hierarchy,

723 messaget &log)

724{

725 namespacet ns(symbol_table);

726 for(const auto &method : parse_tree.parsed_class.methods)

727 {

728 for(const java_bytecode_parse_treet::instructiont &instruction :

729 method.instructions)

730 {

731 const std::string statement =

732 bytecode_info[instruction.bytecode].mnemonic;

733 if(statement == "getstatic" || statement == "putstatic")

734 {

735 INVARIANT(

736 instruction.args.size() > 0,

737 "get/putstatic should have at least one argument");

738 const fieldref_exprt &field_ref =

739 expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);

740 irep_idt component = field_ref.component_name();

741 irep_idt class_id = field_ref.class_name();

742

743 // The final 'true' parameter here includes interfaces, as they can

744 // define static fields.

745 const auto referred_component =

746 get_inherited_component(class_id, component, symbol_table, true);

747 if(!referred_component)

748 {

749 // Create a new stub global on an arbitrary incomplete ancestor of the

750 // class that was referred to. This is just a guess, but we have no

751 // better information to go on.

752 irep_idt add_to_class_id =

753 get_any_incomplete_ancestor_for_stub_static_field(

754 class_id, symbol_table, class_hierarchy);

755

756 // If there are no incomplete ancestors to ascribe the missing field

757 // to, we must have an incomplete model of a class or simply a

758 // version mismatch of some kind. Normally this would be an error, but

759 // our models library currently triggers this error in some cases

760 // (notably java.lang.System, which is missing System.in/out/err).

761 // Therefore for this case we ascribe the missing field to the class

762 // it was directly referenced from, and fall back to initialising the

763 // field in __CPROVER_initialize, rather than try to create or augment

764 // a clinit method for a non-stub class.

765

766 bool no_incomplete_ancestors = add_to_class_id.empty();

767 if(no_incomplete_ancestors)

768 {

769 add_to_class_id = class_id;

770

771 // TODO forbid this again once the models library has been checked

772 // for missing static fields.

773 log.warning() << "Stub static field " << component << " found for "

774 << "non-stub type " << class_id << ". In future this "

775 << "will be a fatal error." << messaget::eom;

776 }

777

778 irep_idt identifier =

779 id2string(add_to_class_id) + "." + id2string(component);

780

781 create_stub_global_symbol(

782 symbol_table,

783 identifier,

784 component,

785 instruction.args[0].type(),

786 add_to_class_id,

787 no_incomplete_ancestors);

788 }

789 }

790 }

791 }

792}

794 bool java_bytecode_languaget::typecheck(

795 symbol_table_baset &symbol_table,

796 const std::string &,

797 message_handlert &message_handler)

798{

799 PRECONDITION(language_options.has_value());

800 // There are various cases in the Java front-end where pre-existing symbols

801 // from a previous load are not handled. We just rule this case out for now;

802 // a user wishing to ensure a particular class is loaded should use

803 // --java-load-class (to force class-loading) or

804 // --lazy-methods-extra-entry-point (to ensure a method body is loaded)

805 // instead of creating two instances of the front-end.

806 INVARIANT(

807 symbol_table.begin() == symbol_table.end(),

808 "the Java front-end should only be used with an empty symbol table");

809

810 java_internal_additions(symbol_table);

811 create_java_initialize(symbol_table);

812

813 if(language_options->string_refinement_enabled)

814 string_preprocess.initialize_conversion_table();

815

816 // Must load java.lang.Object first to avoid stubbing

817 // This ordering could alternatively be enforced by

818 // moving the code below to the class loader.

819 java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =

820 java_class_loader.get_class_with_overlays_map().find("java.lang.Object");

821 if(it != java_class_loader.get_class_with_overlays_map().end())

822 {

823 if(java_bytecode_convert_class(

824 it->second,

825 symbol_table,

826 message_handler,

827 language_options->max_user_array_length,

828 method_bytecode,

829 string_preprocess,

830 language_options->no_load_classes))

831 {

832 return true;

833 }

834 }

835

836 // first generate a new struct symbol for each class and a new function symbol

837 // for every method

838 for(const auto &class_trees : java_class_loader.get_class_with_overlays_map())

839 {

840 if(class_trees.second.front().parsed_class.name.empty())

841 continue;

842

843 if(java_bytecode_convert_class(

844 class_trees.second,

845 symbol_table,

846 message_handler,

847 language_options->max_user_array_length,

848 method_bytecode,

849 string_preprocess,

850 language_options->no_load_classes))

851 {

852 return true;

853 }

854 }

855

856 // Register synthetic method that replaces a real definition if one is

857 // available:

858 if(symbol_table.has_symbol(get_create_array_with_type_name()))

859 {

860 synthetic_methods[get_create_array_with_type_name()] =

861 synthetic_method_typet::CREATE_ARRAY_WITH_TYPE;

862 }

863

864 // Now add synthetic classes for every invokedynamic instruction found (it

865 // makes this easier that all interface types and their methods have been

866 // created above):

867 {

868 std::vector<irep_idt> methods_to_check;

869

870 // Careful not to add to the symtab while iterating over it:

871 for(const auto &id_and_symbol : symbol_table)

872 {

873 const auto &symbol = id_and_symbol.second;

874 const auto &id = symbol.name;

875 if(can_cast_type<code_typet>(symbol.type) && method_bytecode.get(id))

876 {

877 methods_to_check.push_back(id);

878 }

879 }

880

881 for(const auto &id : methods_to_check)

882 {

883 create_invokedynamic_synthetic_classes(

884 id,

885 method_bytecode.get(id)->get().method.instructions,

886 symbol_table,

887 synthetic_methods,

888 message_handler);

889 }

890 }

891

892 // Now that all classes have been created in the symbol table we can populate

893 // the class hierarchy:

894 class_hierarchy(symbol_table);

895

896 // find and mark all implicitly generic class types

897 // this can only be done once all the class symbols have been created

898 for(const auto &c : java_class_loader.get_class_with_overlays_map())

899 {

900 if(c.second.front().parsed_class.name.empty())

901 continue;

902 try

903 {

904 mark_java_implicitly_generic_class_type(

905 c.second.front().parsed_class.name, symbol_table);

906 }

907 catch(missing_outer_class_symbol_exceptiont &)

908 {

909 messaget log(message_handler);

910 log.warning() << "Not marking class " << c.first

911 << " implicitly generic due to missing outer class symbols"

912 << messaget::eom;

913 }

914 }

915

916 // Infer fields on opaque types based on the method instructions just loaded.

917 // For example, if we don't have bytecode for field x of class A, but we can

918 // see an int-typed getfield instruction referring to it, add that field now.

919 for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())

920 {

921 for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)

922 infer_opaque_type_fields(parse_tree, symbol_table);

923 }

924

925 // Create global variables for constants (String and Class literals) up front.

926 // This means that when running with lazy loading, we will be aware of these

927 // literal globals' existence when __CPROVER_initialize is generated in

928 // `generate_support_functions`.

929 const std::size_t before_constant_globals_size = symbol_table.symbols.size();

930 for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())

931 {

932 for(java_bytecode_parse_treet &parse_tree : class_to_trees.second)

933 {

934 generate_constant_global_variables(

935 parse_tree, symbol_table, language_options->string_refinement_enabled);

936 }

937 }

938

939 messaget log(message_handler);

940 log.status() << "Java: added "

941 << (symbol_table.symbols.size() - before_constant_globals_size)

942 << " String or Class constant symbols" << messaget::eom;

943

944 // For each reference to a stub global (that is, a global variable declared on

945 // a class we don't have bytecode for, and therefore don't know the static

946 // initialiser for), create a synthetic static initialiser (clinit method)

947 // to nondet initialise it.

948 // Note this must be done before making static initialiser wrappers below, as

949 // this makes a Classname.clinit method, then the next pass makes a wrapper

950 // that ensures it is only run once, and that static initialisation happens

951 // in class-graph topological order.

952

953 {

954 journalling_symbol_tablet symbol_table_journal =

955 journalling_symbol_tablet::wrap(symbol_table);

956 for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())

957 {

958 for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)

959 {

960 create_stub_global_symbols(

961 parse_tree, symbol_table_journal, class_hierarchy, log);

962 }

963 }

964

965 stub_global_initializer_factory.create_stub_global_initializer_symbols(

966 symbol_table, symbol_table_journal.get_inserted(), synthetic_methods);

967 }

968

969 create_static_initializer_symbols(

970 symbol_table,

971 synthetic_methods,

972 language_options->threading_support,

973 language_options->static_values_json.has_value());

974

975 lazy_class_to_declared_symbols_mapt class_to_declared_symbols;

976

977 // Now incrementally elaborate methods

978 // that are reachable from this entry point.

979 switch(language_options->lazy_methods_mode)

980 {

981 case LAZY_METHODS_MODE_CONTEXT_INSENSITIVE:

982 // ci = context-insensitive

983 if(do_ci_lazy_method_conversion(symbol_table, message_handler))

984 return true;

985 break;

986 case LAZY_METHODS_MODE_EAGER:

987 {

988 symbol_table_buildert symbol_table_builder =

989 symbol_table_buildert::wrap(symbol_table);

990

991 journalling_symbol_tablet journalling_symbol_table =

992 journalling_symbol_tablet::wrap(symbol_table_builder);

993

994 // Convert all synthetic methods:

995 for(const auto &function_id_and_type : synthetic_methods)

996 {

997 convert_single_method(

998 function_id_and_type.first,

999 journalling_symbol_table,

1000 class_to_declared_symbols,

1001 message_handler);

1002 }

1003 // Convert all methods for which we have bytecode now

1004 for(const auto &method_sig : method_bytecode)

1005 {

1006 convert_single_method(

1007 method_sig.first,

1008 journalling_symbol_table,

1009 class_to_declared_symbols,

1010 message_handler);

1011 }

1012 convert_single_method(

1013 INITIALIZE_FUNCTION,

1014 journalling_symbol_table,

1015 class_to_declared_symbols,

1016 message_handler);

1017 // Now convert all newly added string methods

1018 for(const auto &fn_name : journalling_symbol_table.get_inserted())

1019 {

1020 if(string_preprocess.implements_function(fn_name))

1021 convert_single_method(

1022 fn_name, symbol_table, class_to_declared_symbols, message_handler);

1023 }

1024 }

1025 break;

1026 case LAZY_METHODS_MODE_EXTERNAL_DRIVER:

1027 // Our caller is in charge of elaborating methods on demand.

1028 break;

1029 }

1030

1031 // now instrument runtime exceptions

1032 java_bytecode_instrument(

1033 symbol_table, language_options->throw_runtime_exceptions, message_handler);

1034

1035 // now typecheck all

1036 bool res = java_bytecode_typecheck(

1037 symbol_table, message_handler, language_options->string_refinement_enabled);

1038

1039 // now instrument thread-blocks and synchronized methods.

1040 if(language_options->threading_support)

1041 {

1042 convert_threadblock(symbol_table);

1043 convert_synchronized_methods(symbol_table, message_handler);

1044 }

1045

1046 return res;

1047}

1049 bool java_bytecode_languaget::generate_support_functions(

1050 symbol_table_baset &symbol_table,

1051 message_handlert &message_handler)

1052{

1053 PRECONDITION(language_options.has_value());

1054

1055 symbol_table_buildert symbol_table_builder =

1056 symbol_table_buildert::wrap(symbol_table);

1057

1058 main_function_resultt res =

1059 get_main_symbol(symbol_table, main_class, message_handler);

1060 if(!res.is_success())

1061 return res.is_error();

1062

1063 // Load the main function into the symbol table to get access to its

1064 // parameter names

1065 convert_lazy_method(

1066 res.main_function.name, symbol_table_builder, message_handler);

1067

1068 const symbolt &symbol =

1069 symbol_table_builder.lookup_ref(res.main_function.name);

1070 if(symbol.value.is_nil())

1071 {

1072 throw invalid_command_line_argument_exceptiont(

1073 "the program has no entry point",

1074 "function",

1075 "Check that the specified entry point is included by your "

1076 "--context-include or --context-exclude options");

1077 }

1078

1079 // generate the test harness in __CPROVER__start and a call the entry point

1080 return java_entry_point(

1081 symbol_table_builder,

1082 main_class,

1083 message_handler,

1084 language_options->assume_inputs_non_null,

1085 language_options->assert_uncaught_exceptions,

1086 object_factory_parameters,

1087 get_pointer_type_selector(),

1088 language_options->string_refinement_enabled,

1089 [&](const symbolt &function, symbol_table_baset &symbol_table) {

1090 return java_build_arguments(

1091 function,

1092 symbol_table,

1093 language_options->assume_inputs_non_null,

1094 object_factory_parameters,

1095 get_pointer_type_selector(),

1096 message_handler);

1097 });

1098}

1112 bool java_bytecode_languaget::do_ci_lazy_method_conversion(

1113 symbol_table_baset &symbol_table,

1114 message_handlert &message_handler)

1115{

1116 symbol_table_buildert symbol_table_builder =

1117 symbol_table_buildert::wrap(symbol_table);

1118

1119 lazy_class_to_declared_symbols_mapt class_to_declared_symbols;

1120

1121 const method_convertert method_converter =

1122 [this, &symbol_table_builder, &class_to_declared_symbols, &message_handler](

1123 const irep_idt &function_id,

1124 ci_lazy_methods_neededt lazy_methods_needed) {

1125 return convert_single_method(

1126 function_id,

1127 symbol_table_builder,

1128 std::move(lazy_methods_needed),

1129 class_to_declared_symbols,

1130 message_handler);

1131 };

1132

1133 ci_lazy_methodst method_gather(

1134 symbol_table,

1135 main_class,

1136 main_jar_classes,

1137 language_options->extra_methods,

1138 java_class_loader,

1139 language_options->java_load_classes,

1140 get_pointer_type_selector(),

1141 synthetic_methods);

1142

1143 return method_gather(

1144 symbol_table, method_bytecode, method_converter, message_handler);

1145}

1148 java_bytecode_languaget::get_pointer_type_selector() const

1149{

1150 PRECONDITION(pointer_type_selector.get()!=nullptr);

1151 return *pointer_type_selector;

1152}

1159 void java_bytecode_languaget::methods_provided(

1160 std::unordered_set<irep_idt> &methods) const

1161{

1162 const std::string cprover_class_prefix = "java::org.cprover.CProver.";

1163

1164 // Add all string solver methods to map

1165 string_preprocess.get_all_function_names(methods);

1166 // Add all concrete methods to map

1167 for(const auto &kv : method_bytecode)

1168 methods.insert(kv.first);

1169 // Add all synthetic methods to map

1170 for(const auto &kv : synthetic_methods)

1171 methods.insert(kv.first);

1172 methods.insert(INITIALIZE_FUNCTION);

1173}

1184 void java_bytecode_languaget::convert_lazy_method(

1185 const irep_idt &function_id,

1186 symbol_table_baset &symtab,

1187 message_handlert &message_handler)

1188{

1189 const symbolt &symbol = symtab.lookup_ref(function_id);

1190 if(symbol.value.is_not_nil())

1191 return;

1192

1193 journalling_symbol_tablet symbol_table=

1194 journalling_symbol_tablet::wrap(symtab);

1195

1196 lazy_class_to_declared_symbols_mapt class_to_declared_symbols;

1197 convert_single_method(

1198 function_id, symbol_table, class_to_declared_symbols, message_handler);

1199

1200 // Instrument runtime exceptions (unless symbol is a stub or is the

1201 // INITIALISE_FUNCTION).

1202 if(symbol.value.is_not_nil() && function_id != INITIALIZE_FUNCTION)

1203 {

1204 java_bytecode_instrument_symbol(

1205 symbol_table,

1206 symbol_table.get_writeable_ref(function_id),

1207 language_options->throw_runtime_exceptions,

1208 message_handler);

1209 }

1210

1211 // now typecheck this function

1212 java_bytecode_typecheck_updated_symbols(

1213 symbol_table, message_handler, language_options->string_refinement_enabled);

1214}

1226 static void notify_static_method_calls(

1227 const codet &function_body,

1228 std::optional<ci_lazy_methods_neededt> needed_lazy_methods)

1229{

1230 if(needed_lazy_methods)

1231 {

1232 for(const_depth_iteratort it = function_body.depth_cbegin();

1233 it != function_body.depth_cend();

1234 ++it)

1235 {

1236 if(it->id() == ID_code)

1237 {

1238 const auto fn_call = expr_try_dynamic_cast<code_function_callt>(*it);

1239 if(!fn_call)

1240 continue;

1241 const symbol_exprt *fn_sym =

1242 expr_try_dynamic_cast<symbol_exprt>(fn_call->function());

1243 if(fn_sym)

1244 needed_lazy_methods->add_needed_method(fn_sym->identifier());

1245 }

1246 else if(

1247 it->id() == ID_side_effect &&

1248 to_side_effect_expr(*it).get_statement() == ID_function_call)

1249 {

1250 const auto &call_expr = to_side_effect_expr_function_call(*it);

1251 const symbol_exprt *fn_sym =

1252 expr_try_dynamic_cast<symbol_exprt>(call_expr.function());

1253 if(fn_sym)

1254 {

1255 INVARIANT(

1256 false,

1257 "Java synthetic methods are not "

1258 "expected to produce side_effect_expr_function_callt. If "

1259 "that has changed, remove this invariant. Also note that "

1260 "as of the time of writing remove_virtual_functions did "

1261 "not support this form of function call.");

1262 // needed_lazy_methods->add_needed_method(fn_sym->get_identifier());

1263 }

1264 }

1265 }

1266 }

1267}

1282 bool java_bytecode_languaget::convert_single_method(

1283 const irep_idt &function_id,

1284 symbol_table_baset &symbol_table,

1285 std::optional<ci_lazy_methods_neededt> needed_lazy_methods,

1286 lazy_class_to_declared_symbols_mapt &class_to_declared_symbols,

1287 message_handlert &message_handler)

1288{

1289 const symbolt &symbol = symbol_table.lookup_ref(function_id);

1290

1291 // Nothing to do if body is already loaded

1292 if(symbol.value.is_not_nil())

1293 return false;

1294

1295 if(function_id == INITIALIZE_FUNCTION)

1296 {

1297 java_static_lifetime_init(

1298 symbol_table,

1299 symbol.location,

1300 language_options->assume_inputs_non_null,

1301 object_factory_parameters,

1302 *pointer_type_selector,

1303 language_options->string_refinement_enabled,

1304 message_handler);

1305 return false;

1306 }

1307

1308 INVARIANT(declaring_class(symbol), "Method must have a declaring class.");

1309

1310 bool ret = convert_single_method_code(

1311 function_id,

1312 symbol_table,

1313 needed_lazy_methods,

1314 class_to_declared_symbols,

1315 message_handler);

1316

1317 if(symbol.value.is_not_nil() && language_options->should_lift_clinit_calls)

1318 {

1319 auto &writable_symbol = symbol_table.get_writeable_ref(function_id);

1320 writable_symbol.value =

1321 lift_clinit_calls(std::move(to_code(writable_symbol.value)));

1322 }

1323

1324 INVARIANT(declaring_class(symbol), "Method must have a declaring class.");

1325

1326 return ret;

1327}

1341 bool java_bytecode_languaget::convert_single_method_code(

1342 const irep_idt &function_id,

1343 symbol_table_baset &symbol_table,

1344 std::optional<ci_lazy_methods_neededt> needed_lazy_methods,

1345 lazy_class_to_declared_symbols_mapt &class_to_declared_symbols,

1346 message_handlert &message_handler)

1347{

1348 const auto &symbol = symbol_table.lookup_ref(function_id);

1349 PRECONDITION(symbol.value.is_nil());

1350

1351 // Get bytecode for specified function if we have it

1352 method_bytecodet::opt_reft cmb = method_bytecode.get(function_id);

1353

1354 synthetic_methods_mapt::iterator synthetic_method_it;

1355

1356 // Check if have a string solver implementation

1357 if(string_preprocess.implements_function(function_id))

1358 {

1359 symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);

1360 // Load parameter names from any extant bytecode before filling in body

1361 if(cmb)

1362 {

1363 java_bytecode_initialize_parameter_names(

1364 writable_symbol, cmb->get().method.local_variable_table, symbol_table);

1365 }

1366 // Populate body of the function with code generated by string preprocess

1367 codet generated_code = string_preprocess.code_for_function(

1368 writable_symbol, symbol_table, message_handler);

1369 // String solver can make calls to functions that haven't yet been seen.

1370 // Add these to the needed_lazy_methods collection

1371 notify_static_method_calls(generated_code, needed_lazy_methods);

1372 writable_symbol.value = std::move(generated_code);

1373 return false;

1374 }

1375 else if(

1376 (synthetic_method_it = synthetic_methods.find(function_id)) !=

1377 synthetic_methods.end())

1378 {

1379 // Synthetic method (i.e. one generated by the Java frontend and which

1380 // doesn't occur in the source bytecode):

1381 symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);

1382 switch(synthetic_method_it->second)

1383 {

1384 case synthetic_method_typet::STATIC_INITIALIZER_WRAPPER:

1385 if(language_options->threading_support)

1386 writable_symbol.value = get_thread_safe_clinit_wrapper_body(

1387 function_id,

1388 symbol_table,

1389 language_options->nondet_static,

1390 language_options->static_values_json.has_value(),

1391 object_factory_parameters,

1392 get_pointer_type_selector(),

1393 message_handler);

1394 else

1395 writable_symbol.value = get_clinit_wrapper_body(

1396 function_id,

1397 symbol_table,

1398 language_options->nondet_static,

1399 language_options->static_values_json.has_value(),

1400 object_factory_parameters,

1401 get_pointer_type_selector(),

1402 message_handler);

1403 break;

1404 case synthetic_method_typet::USER_SPECIFIED_STATIC_INITIALIZER:

1405 {

1406 const auto class_name =

1407 declaring_class(symbol_table.lookup_ref(function_id));

1408 INVARIANT(

1409 class_name, "user_specified_clinit must be declared by a class.");

1410 INVARIANT(

1411 language_options->static_values_json.has_value(),

1412 "static-values JSON must be available");

1413 writable_symbol.value = get_user_specified_clinit_body(

1414 *class_name,

1415 *language_options->static_values_json,

1416 symbol_table,

1417 needed_lazy_methods,

1418 language_options->max_user_array_length,

1419 references,

1420 class_to_declared_symbols.get(symbol_table));

1421 break;

1422 }

1423 case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:

1424 writable_symbol.value =

1425 stub_global_initializer_factory.get_stub_initializer_body(

1426 function_id,

1427 symbol_table,

1428 object_factory_parameters,

1429 get_pointer_type_selector(),

1430 message_handler);

1431 break;

1432 case synthetic_method_typet::INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR:

1433 writable_symbol.value = invokedynamic_synthetic_constructor(

1434 function_id, symbol_table, message_handler);

1435 break;

1436 case synthetic_method_typet::INVOKEDYNAMIC_METHOD:

1437 writable_symbol.value = invokedynamic_synthetic_method(

1438 function_id, symbol_table, message_handler);

1439 break;

1440 case synthetic_method_typet::CREATE_ARRAY_WITH_TYPE:

1441 {

1442 INVARIANT(

1443 cmb,

1444 "CProver.createArrayWithType should only be registered if "

1445 "we have a real implementation available");

1446 java_bytecode_initialize_parameter_names(

1447 writable_symbol, cmb->get().method.local_variable_table, symbol_table);

1448 writable_symbol.value =

1449 create_array_with_type_body(function_id, symbol_table, message_handler);

1450 break;

1451 }

1452 }

1453 // Notify lazy methods of static calls made from the newly generated

1454 // function:

1455 notify_static_method_calls(

1456 to_code(writable_symbol.value), needed_lazy_methods);

1457 return false;

1458 }

1459

1460 // No string solver or static init wrapper implementation;

1461 // check if have bytecode for it

1462 if(cmb)

1463 {

1464 java_bytecode_convert_method(

1465 symbol_table.lookup_ref(cmb->get().class_id),

1466 cmb->get().method,

1467 symbol_table,

1468 message_handler,

1469 language_options->max_user_array_length,

1470 language_options->throw_assertion_error,

1471 std::move(needed_lazy_methods),

1472 string_preprocess,

1473 class_hierarchy,

1474 language_options->threading_support,

1475 language_options->method_context,

1476 language_options->assert_no_exceptions_thrown);

1477 return false;

1478 }

1479

1480 if(needed_lazy_methods)

1481 {

1482 // The return of an opaque function is a source of an otherwise invisible

1483 // instantiation, so here we ensure we've loaded the appropriate classes.

1484 const java_method_typet function_type = to_java_method_type(symbol.type);

1485 if(

1486 const pointer_typet *pointer_return_type =

1487 type_try_dynamic_cast<pointer_typet>(function_type.return_type()))

1488 {

1489 // If the return type is abstract, we won't forcibly instantiate it here

1490 // otherwise this can cause abstract methods to be explictly called

1491 // TODO(tkiley): Arguably no abstract class should ever be added to

1492 // TODO(tkiley): ci_lazy_methods_neededt, but this needs further

1493 // TODO(tkiley): investigation

1494 namespacet ns{symbol_table};

1495 const java_class_typet &underlying_type = to_java_class_type(

1496 ns.follow_tag(to_struct_tag_type(pointer_return_type->base_type())));

1497

1498 if(!underlying_type.is_abstract())

1499 needed_lazy_methods->add_all_needed_classes(*pointer_return_type);

1500 }

1501 }

1502

1503 return true;

1504}

1506 bool java_bytecode_languaget::final(symbol_table_baset &)

1507{

1508 PRECONDITION(language_options.has_value());

1509 return false;

1510}

1512 void java_bytecode_languaget::show_parse(

1513 std::ostream &out,

1514 message_handlert &message_handler)

1515{

1516 java_class_loadert::parse_tree_with_overlayst &parse_trees =

1517 java_class_loader(main_class, message_handler);

1518 parse_trees.front().output(out);

1519 if(parse_trees.size() > 1)

1520 {

1521 out << "\n\nClass has the following overlays:\n\n";

1522 for(auto parse_tree_it = std::next(parse_trees.begin());

1523 parse_tree_it != parse_trees.end();

1524 ++parse_tree_it)

1525 {

1526 parse_tree_it->output(out);

1527 }

1528 out << "End of class overlays.\n";

1529 }

1530}

1532 std::unique_ptr<languaget> new_java_bytecode_language()

1533{

1534 return std::make_unique<java_bytecode_languaget>();

1535}

1537 bool java_bytecode_languaget::from_expr(

1538 const exprt &expr,

1539 std::string &code,

1540 const namespacet &ns)

1541{

1542 code=expr2java(expr, ns);

1543 return false;

1544}

1546 bool java_bytecode_languaget::from_type(

1547 const typet &type,

1548 std::string &code,

1549 const namespacet &ns)

1550{

1551 code=type2java(type, ns);

1552 return false;

1553}

1555 bool java_bytecode_languaget::to_expr(

1556 const std::string &code,

1557 const std::string &module,

1558 exprt &expr,

1559 const namespacet &ns,

1560 message_handlert &message_handler)

1561{

1562#if 0

1563 expr.make_nil();

1564

1565 // no preprocessing yet...

1566

1567 std::istringstream i_preprocessed(code);

1568

1569 // parsing

1570

1571 java_bytecode_parser.clear();

1572 java_bytecode_parser.filename="";

1573 java_bytecode_parser.in=&i_preprocessed;

1574 java_bytecode_parser.set_message_handler(message_handler);

1575 java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;

1576 java_bytecode_parser.mode=java_bytecode_parsert::GCC;

1577 java_bytecode_scanner_init();

1578

1579 bool result=java_bytecode_parser.parse();

1580

1581 if(java_bytecode_parser.parse_tree.items.empty())

1582 result=true;

1583 else

1584 {

1585 expr=java_bytecode_parser.parse_tree.items.front().value();

1586

1587 result=java_bytecode_convert(expr, "", message_handler);

1588

1589 // typecheck it

1590 if(!result)

1591 result=java_bytecode_typecheck(expr, message_handler, ns);

1592 }

1593

1594 // save some memory

1595 java_bytecode_parser.clear();

1596

1597 return result;

1598#else

1599 // unused parameters

1600 (void)code;

1601 (void)module;

1602 (void)expr;

1603 (void)ns;

1604 (void)message_handler;

1605#endif

1606

1607 return true; // fail for now

1608}

1610 java_bytecode_languaget::~java_bytecode_languaget()

1611{

1612}

1618 java_bytecode_languaget::build_extra_entry_points(const optionst &options) const

1619{

1620 (void)options; // unused parameter

1621 return {};

1622}

config

configt config

Definition config.cpp:25

bytecode_info

struct bytecode_infot const bytecode_info[]

Definition bytecode_info.cpp:16

ci_lazy_methods.h

Collect methods needed to be loaded using the lazy method.

method_convertert

std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert

Definition ci_lazy_methods.h:93

class_hierarchy.h

Class Hierarchy.

address_of_exprt

Operator to return the address of an object.

Definition pointer_expr.h:540

ai_baset::output

virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const

Output the abstract states for a single function.

Definition ai.cpp:39

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

ci_lazy_methods_neededt

Definition ci_lazy_methods_needed.h:26

ci_lazy_methodst

Definition ci_lazy_methods.h:99

class_hierarchyt

Non-graph-based representation of the class hierarchy.

Definition class_hierarchy.h:41

class_hierarchyt::class_map

class_mapt class_map

Definition class_hierarchy.h:53

class_hierarchyt::idst

std::vector< irep_idt > idst

Definition class_hierarchy.h:43

class_typet::is_abstract

bool is_abstract() const

Definition std_types.h:357

cmdlinet

Definition cmdline.h:20

code_typet::return_type

const typet & return_type() const

Definition std_types.h:688

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

configt::java

struct configt::javat java

const_depth_iteratort

Definition expr_iterator.h:221

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

typet & type()

Return the type of the expression.

Definition expr.h:85

fieldref_exprt

Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...

Definition java_bytecode_parse_tree.h:334

invalid_command_line_argument_exceptiont

Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...

Definition exception_utils.h:51

irept::is_not_nil

bool is_not_nil() const

Definition irep.h:372

irept::make_nil

void make_nil()

Definition irep.h:446

irept::is_nil

bool is_nil() const

Definition irep.h:368

java_bytecode_languaget::methods_provided

virtual void methods_provided(std::unordered_set< irep_idt > &methods) const override

Provide feedback to language_filest so that when asked for a lazy method, it can delegate to this ins...

Definition java_bytecode_language.cpp:1159

java_bytecode_languaget::synthetic_methods

synthetic_methods_mapt synthetic_methods

Maps synthetic method names on to the particular type of synthetic method (static initializer,...

Definition java_bytecode_language.h:382

java_bytecode_languaget::main_jar_classes

std::vector< irep_idt > main_jar_classes

Definition java_bytecode_language.h:368

java_bytecode_languaget::to_expr

bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns, message_handlert &message_handler) override

Parses the given string into an expression.

Definition java_bytecode_language.cpp:1555

java_bytecode_languaget::final

virtual bool final(symbol_table_baset &context) override

Final adjustments, e.g.

Definition java_bytecode_language.cpp:1506

java_bytecode_languaget::id

std::string id() const override

Definition java_bytecode_language.h:324

java_bytecode_languaget::stub_global_initializer_factory

stub_global_initializer_factoryt stub_global_initializer_factory

Definition java_bytecode_language.h:383

java_bytecode_languaget::extensions

std::set< std::string > extensions() const override

Definition java_bytecode_language.cpp:272

java_bytecode_languaget::~java_bytecode_languaget

virtual ~java_bytecode_languaget()

Definition java_bytecode_language.cpp:1610

java_bytecode_languaget::from_type

bool from_type(const typet &type, std::string &code, const namespacet &ns) override

Formats the given type in a language-specific way.

Definition java_bytecode_language.cpp:1546

java_bytecode_languaget::set_language_options

void set_language_options(const optionst &, message_handlert &) override

Consume options that are java bytecode specific.

Definition java_bytecode_language.cpp:259

java_bytecode_languaget::method_bytecode

method_bytecodet method_bytecode

Definition java_bytecode_language.h:371

java_bytecode_languaget::main_class

irep_idt main_class

Definition java_bytecode_language.h:367

java_bytecode_languaget::pointer_type_selector

const std::unique_ptr< const select_pointer_typet > pointer_type_selector

Definition java_bytecode_language.h:377

java_bytecode_languaget::class_hierarchy

class_hierarchyt class_hierarchy

Definition java_bytecode_language.h:384

java_bytecode_languaget::object_factory_parameters

java_object_factory_parameterst object_factory_parameters

Definition java_bytecode_language.h:370

java_bytecode_languaget::show_parse

void show_parse(std::ostream &out, message_handlert &) override

Definition java_bytecode_language.cpp:1512

java_bytecode_languaget::initialize_class_loader

void initialize_class_loader(message_handlert &)

Definition java_bytecode_language.cpp:293

java_bytecode_languaget::string_preprocess

java_string_library_preprocesst string_preprocess

Definition java_bytecode_language.h:372

java_bytecode_languaget::modules_provided

void modules_provided(std::set< std::string > &modules) override

Definition java_bytecode_language.cpp:277

java_bytecode_languaget::java_class_loader

java_class_loadert java_class_loader

Definition java_bytecode_language.h:369

java_bytecode_languaget::convert_lazy_method

virtual void convert_lazy_method(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler) override

Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a...

Definition java_bytecode_language.cpp:1184

java_bytecode_languaget::build_extra_entry_points

virtual std::vector< load_extra_methodst > build_extra_entry_points(const optionst &) const

This method should be overloaded to provide alternative approaches for specifying extra entry points.

Definition java_bytecode_language.cpp:1618

java_bytecode_languaget::language_options

std::optional< java_bytecode_language_optionst > language_options

Definition java_bytecode_language.h:366

java_bytecode_languaget::get_pointer_type_selector

const select_pointer_typet & get_pointer_type_selector() const

Definition java_bytecode_language.cpp:1148

java_bytecode_languaget::parse_from_main_class

void parse_from_main_class(message_handlert &)

Definition java_bytecode_language.cpp:322

java_bytecode_languaget::convert_single_method_code

bool convert_single_method_code(const irep_idt &function_id, symbol_table_baset &symbol_table, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, message_handlert &)

Convert a method (one whose type is known but whose body hasn't been converted) but don't run typeche...

Definition java_bytecode_language.cpp:1341

java_bytecode_languaget::from_expr

bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override

Formats the given expression in a language-specific way.

Definition java_bytecode_language.cpp:1537

java_bytecode_languaget::convert_single_method

void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, message_handlert &message_handler)

Definition java_bytecode_language.h:337

java_bytecode_languaget::references

std::unordered_map< std::string, object_creation_referencet > references

Map used in all calls to functions that deterministically create objects (currently only assign_from_...

Definition java_bytecode_language.h:390

java_bytecode_languaget::typecheck

bool typecheck(symbol_table_baset &context, const std::string &module, message_handlert &message_handler) override

Definition java_bytecode_language.cpp:794

java_bytecode_languaget::preprocess

virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream, message_handlert &message_handler) override

ANSI-C preprocessing.

Definition java_bytecode_language.cpp:283

java_bytecode_languaget::generate_support_functions

bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler) override

Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...

Definition java_bytecode_language.cpp:1049

java_bytecode_languaget::do_ci_lazy_method_conversion

bool do_ci_lazy_method_conversion(symbol_table_baset &, message_handlert &)

Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...

Definition java_bytecode_language.cpp:1112

java_bytecode_languaget::parse

bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override

We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...

Definition java_bytecode_language.cpp:371

java_class_loader_baset::add_classpath_entry

void add_classpath_entry(const std::string &, message_handlert &)

Appends an entry to the class path, used for loading classes.

Definition java_class_loader_base.cpp:22

java_class_loader_baset::clear_classpath

void clear_classpath()

Clear all classpath entries.

Definition java_class_loader_base.h:26

java_class_loader_baset::jar_pool

jar_poolt jar_pool

a cache for jar_filet, by path name

Definition java_class_loader_base.h:42

java_class_loader_limitt

Class representing a filter for class file loading.

Definition java_class_loader_limit.h:22

java_class_loadert::java_load_classes

std::vector< irep_idt > java_load_classes

Classes to be explicitly loaded.

Definition java_class_loader.h:102

java_class_loadert::load_entire_jar

std::vector< irep_idt > load_entire_jar(const std::string &jar_path, message_handlert &)

Load all class files from a .jar file.

Definition java_class_loader.cpp:212

java_class_loadert::can_load_class

bool can_load_class(const irep_idt &class_name, message_handlert &)

Checks whether class_name is parseable from the classpath, ignoring class loading limits.

Definition java_class_loader.cpp:107

java_class_loadert::get_class_with_overlays_map

fixed_keys_map_wrappert< parse_tree_with_overridest_mapt > get_class_with_overlays_map()

Map from class names to the bytecode parse trees.

Definition java_class_loader.h:83

java_class_loadert::set_extra_class_refs_function

void set_extra_class_refs_function(get_extra_class_refs_functiont func)

Sets a function that provides extra dependencies for a particular class.

Definition java_class_loader.h:65

java_class_loadert::set_java_cp_include_files

void set_java_cp_include_files(const std::string &cp_include_files)

Set the argument of the class loader limit java_class_loader_limitt.

Definition java_class_loader.h:57

java_class_loadert::parse_tree_with_overlayst

std::list< java_bytecode_parse_treet > parse_tree_with_overlayst

A list of parse trees supporting overlay classes.

Definition java_class_loader.h:29

java_class_loadert::add_load_classes

void add_load_classes(const std::vector< irep_idt > &classes)

Adds the list of classes to the load queue, forcing them to be loaded even without explicit reference...

Definition java_class_loader.h:72

java_class_typet

Definition java_types.h:196

java_method_typet

Definition java_types.h:100

java_string_library_preprocesst::get_all_function_names

void get_all_function_names(std::unordered_set< irep_idt > &methods) const

Definition java_string_library_preprocess.cpp:1446

java_string_library_preprocesst::implements_function

bool implements_function(const irep_idt &function_id) const

Definition java_string_library_preprocess.cpp:1422

java_string_library_preprocesst::get_string_type_base_classes

std::vector< irep_idt > get_string_type_base_classes(const irep_idt &class_name)

Gets the base classes for known String and String-related types, or returns an empty list for other t...

Definition java_string_library_preprocess.cpp:187

java_string_library_preprocesst::initialize_conversion_table

void initialize_conversion_table()

fill maps with correspondence from java method names to conversion functions

Definition java_string_library_preprocess.cpp:1520

java_string_library_preprocesst::code_for_function

codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table, message_handlert &message_handler)

Should be called to provide code for string functions that are used in the code but for which no impl...

Definition java_string_library_preprocess.cpp:1462

java_string_library_preprocesst::initialize_known_type_table

void initialize_known_type_table()

Definition java_string_library_preprocess.cpp:1511

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

jsont

Definition json.h:27

jsont::is_array

bool is_array() const

Definition json.h:61

lazy_class_to_declared_symbols_mapt

Map classes to the symbols they declare but is only computed once it is needed and the map is then ke...

Definition java_bytecode_language.h:187

lazy_class_to_declared_symbols_mapt::reinitialize

void reinitialize()

Definition java_bytecode_language.cpp:134

lazy_class_to_declared_symbols_mapt::get

std::unordered_multimap< irep_idt, symbolt > & get(const symbol_table_baset &symbol_table)

Definition java_bytecode_language.cpp:124

lazy_class_to_declared_symbols_mapt::initialized

bool initialized

Definition java_bytecode_language.h:197

lazy_class_to_declared_symbols_mapt::map

std::unordered_multimap< irep_idt, symbolt > map

Definition java_bytecode_language.h:198

message_handlert

Definition message.h:27

messaget

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

Definition message.h:154

messaget::eom

static eomt eom

Definition message.h:289

method_bytecodet::get

opt_reft get(const irep_idt &method_id)

Definition ci_lazy_methods.h:82

method_bytecodet::opt_reft

std::optional< std::reference_wrapper< const class_method_and_bytecodet > > opt_reft

Definition ci_lazy_methods.h:46

missing_outer_class_symbol_exceptiont

An exception that is raised checking whether a class is implicitly generic if a symbol for an outer c...

Definition java_bytecode_convert_class.h:56

namespace_baset::follow_tag

const union_typet & follow_tag(const union_tag_typet &) const

Follow type tag of union type.

Definition namespace.cpp:49

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

optionst

Definition options.h:23

optionst::get_unsigned_int_option

unsigned int get_unsigned_int_option(const std::string &option) const

Definition options.cpp:56

optionst::is_set

bool is_set(const std::string &option) const

N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")

Definition options.cpp:62

optionst::get_bool_option

bool get_bool_option(const std::string &option) const

Definition options.cpp:44

optionst::set_option

void set_option(const std::string &option, const bool value)

Definition options.cpp:28

optionst::get_option

const std::string get_option(const std::string &option) const

Definition options.cpp:67

optionst::get_list_option

const value_listt & get_list_option(const std::string &option) const

Definition options.cpp:80

pointer_typet

The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...

Definition pointer_expr.h:24

prefix_filtert

Provides filtering of strings vai inclusion/exclusion lists of prefixes.

Definition prefix_filter.h:20

select_pointer_typet

Definition select_pointer_type.h:23

side_effect_exprt::get_statement

const irep_idt & get_statement() const

Definition std_code.h:1472

struct_tag_typet

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

Definition std_types.h:492

stub_global_initializer_factoryt::create_stub_global_initializer_symbols

void create_stub_global_initializer_symbols(symbol_table_baset &symbol_table, const std::unordered_set< irep_idt > &stub_globals_set, synthetic_methods_mapt &synthetic_methods)

Create static initializer symbols for each distinct class that has stub globals.

Definition java_static_initializers.cpp:925

stub_global_initializer_factoryt::get_stub_initializer_body

code_blockt get_stub_initializer_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)

Create the body of a synthetic static initializer (clinit method), which initialise stub globals in t...

Definition java_static_initializers.cpp:1002

symbol_exprt

Expression to hold a symbol (variable)

Definition std_expr.h:132

symbol_exprt::identifier

void identifier(const irep_idt &identifier)

Definition std_expr.h:160

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

virtual iteratort begin()=0

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

virtual iteratort end()=0

symbol_table_baset::has_symbol

bool has_symbol(const irep_idt &name) const

Check whether a symbol exists in the symbol table.

Definition symbol_table_base.h:88

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

symbol_table_buildert

Author: Diffblue Ltd.

Definition symbol_table_builder.h:14

symbol_table_buildert::wrap

static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)

Definition symbol_table_builder.h:42

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

exprt value

Initial value of symbol.

Definition symbol.h:34

system_exceptiont

Thrown when some external system fails unexpectedly.

Definition exception_utils.h:72

typet

The type of an expression, extends irept.

Definition type.h:29

cmdline.h

config.h

get_create_array_with_type_name

irep_idt get_create_array_with_type_name()

Returns the symbol name for org.cprover.CProver.createArrayWithType

Definition create_array_with_type_intrinsic.cpp:23

create_array_with_type_body

codet create_array_with_type_body(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)

Returns the internal implementation for org.cprover.CProver.createArrayWithType.

Definition create_array_with_type_intrinsic.cpp:41

create_array_with_type_intrinsic.h

Implementation of CProver.createArrayWithType intrinsic.

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

expr2java.h

expr_iterator.h

Forward depth-first search iterators These iterators' copy operations are expensive,...

id2string

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

Definition irep.h:44

convert_synchronized_methods

void convert_synchronized_methods(symbol_table_baset &symbol_table, message_handlert &message_handler)

Iterate through the symbol table to find and instrument synchronized methods.

Definition java_bytecode_concurrency_instrumentation.cpp:602

convert_threadblock

void convert_threadblock(symbol_table_baset &symbol_table)

Iterate through the symbol table to find and appropriately instrument thread-blocks.

Definition java_bytecode_concurrency_instrumentation.cpp:484

java_bytecode_concurrency_instrumentation.h

mark_java_implicitly_generic_class_type

void mark_java_implicitly_generic_class_type(const irep_idt &class_name, symbol_table_baset &symbol_table)

Checks if the class is implicitly generic, i.e., it is an inner class of any generic class.

Definition java_bytecode_convert_class.cpp:1180

java_bytecode_convert_class

bool java_bytecode_convert_class(const java_class_loadert::parse_tree_with_overlayst &parse_trees, symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, method_bytecodet &method_bytecode, java_string_library_preprocesst &string_preprocess, const std::unordered_set< std::string > &no_load_classes)

See class java_bytecode_convert_classt.

Definition java_bytecode_convert_class.cpp:995

java_bytecode_convert_class.h

JAVA Bytecode Language Conversion.

java_bytecode_initialize_parameter_names

void java_bytecode_initialize_parameter_names(symbolt &method_symbol, const java_bytecode_parse_treet::methodt::local_variable_tablet &local_variable_table, symbol_table_baset &symbol_table)

This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize sym...

Definition java_bytecode_convert_method.cpp:3203

java_bytecode_convert_method

void java_bytecode_convert_method(const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, bool throw_assertion_error, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, const std::optional< prefix_filtert > &method_context, bool assert_no_exceptions_thrown)

Definition java_bytecode_convert_method.cpp:3281

java_bytecode_convert_method.h

JAVA Bytecode Language Conversion.

java_bytecode_instrument_symbol

void java_bytecode_instrument_symbol(symbol_table_baset &symbol_table, symbolt &symbol, const bool throw_runtime_exceptions, message_handlert &message_handler)

Instruments the code attached to symbol with runtime exceptions or corresponding assertions.

Definition java_bytecode_instrument.cpp:544

java_bytecode_instrument

void java_bytecode_instrument(symbol_table_baset &symbol_table, const bool throw_runtime_exceptions, message_handlert &message_handler)

Instruments all the code in the symbol_table with runtime exceptions or corresponding assertions.

Definition java_bytecode_instrument.cpp:594

exception_needed_classes

const std::vector< std::string > exception_needed_classes

Definition java_bytecode_instrument.cpp:77

java_bytecode_instrument.h

java_internal_additions

void java_internal_additions(symbol_table_baset &dest)

Definition java_bytecode_internal_additions.cpp:22

java_bytecode_internal_additions.h

generate_constant_global_variables

static void generate_constant_global_variables(java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table, bool string_refinement_enabled)

Creates global variables for constants mentioned in a given method.

Definition java_bytecode_language.cpp:591

get_ldc_result

static exprt get_ldc_result(const exprt &ldc_arg0, symbol_table_baset &symbol_table, bool string_refinement_enabled)

Get result of a Java load-constant (ldc) instruction.

Definition java_bytecode_language.cpp:554

parse_java_language_options

void parse_java_language_options(const cmdlinet &cmd, optionst &options)

Parse options that are java bytecode specific.

Definition java_bytecode_language.cpp:51

new_java_bytecode_language

std::unique_ptr< languaget > new_java_bytecode_language()

Definition java_bytecode_language.cpp:1532

get_or_create_class_literal_symbol

static symbol_exprt get_or_create_class_literal_symbol(const irep_idt &class_id, symbol_table_baset &symbol_table)

Create if necessary, then return the constant global java.lang.Class symbol for a given class id.

Definition java_bytecode_language.cpp:513

infer_opaque_type_fields

static void infer_opaque_type_fields(const java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table)

Infer fields that must exist on opaque types from field accesses against them.

Definition java_bytecode_language.cpp:447

create_stub_global_symbol

static void create_stub_global_symbol(symbol_table_baset &symbol_table, const irep_idt &symbol_id, const irep_idt &symbol_basename, const typet &symbol_type, const irep_idt &class_id, bool force_nondet_init)

Add a stub global symbol to the symbol table, initialising pointer-typed symbols with null and primit...

Definition java_bytecode_language.cpp:636

throwMainClassLoadingError

static void throwMainClassLoadingError(const std::string &main_class)

Definition java_bytecode_language.cpp:316

get_context

prefix_filtert get_context(const optionst &options)

Definition java_bytecode_language.cpp:112

create_stub_global_symbols

static void create_stub_global_symbols(const java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, messaget &log)

Search for getstatic and putstatic instructions in a class' bytecode and create stub symbols for any ...

Definition java_bytecode_language.cpp:719

get_any_incomplete_ancestor_for_stub_static_field

static irep_idt get_any_incomplete_ancestor_for_stub_static_field(const irep_idt &start_class_id, const symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy)

Find any incomplete ancestor of a given class that can have a stub static field attached to it.

Definition java_bytecode_language.cpp:677

notify_static_method_calls

static void notify_static_method_calls(const codet &function_body, std::optional< ci_lazy_methods_neededt > needed_lazy_methods)

Notify ci_lazy_methods, if present, of any static function calls made by the given function body.

Definition java_bytecode_language.cpp:1226

java_bytecode_language.h

LAZY_METHODS_MODE_EAGER

@ LAZY_METHODS_MODE_EAGER

Definition java_bytecode_language.h:171

LAZY_METHODS_MODE_EXTERNAL_DRIVER

@ LAZY_METHODS_MODE_EXTERNAL_DRIVER

Definition java_bytecode_language.h:173

LAZY_METHODS_MODE_CONTEXT_INSENSITIVE

@ LAZY_METHODS_MODE_CONTEXT_INSENSITIVE

Definition java_bytecode_language.h:172

JAVA_CLASS_MODEL_SUFFIX

#define JAVA_CLASS_MODEL_SUFFIX

Definition java_bytecode_language.h:257

get_context

prefix_filtert get_context(const optionst &options)

Definition java_bytecode_language.cpp:112

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

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

java_bytecode_typecheck.h

JAVA Bytecode Language Type Checking.

java_class_loader.h

java_class_loader_limit.h

limit class path loading

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

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

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

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

java_entry_point.h

class_to_declared_symbols

std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_table_baset &symbol_table)

Definition java_static_initializers.cpp:779

get_user_specified_clinit_body

code_blockt get_user_specified_clinit_body(const irep_idt &class_id, const json_objectt &static_values_json, symbol_table_baset &symbol_table, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, size_t max_user_array_length, std::unordered_map< std::string, object_creation_referencet > &references, const std::unordered_multimap< irep_idt, symbolt > &class_to_declared_symbols_map)

Create the body of a user_specified_clinit function for a given class, which includes assignments for...

Definition java_static_initializers.cpp:791

create_static_initializer_symbols

void create_static_initializer_symbols(symbol_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe, const bool is_user_clinit_needed)

Create static initializer wrappers and possibly user-specified functions for initial static field val...

Definition java_static_initializers.cpp:874

get_clinit_wrapper_body

code_ifthenelset get_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)

Produces the static initializer wrapper body for the given function.

Definition java_static_initializers.cpp:718

get_thread_safe_clinit_wrapper_body

code_blockt get_thread_safe_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)

Thread safe version of the static initializer.

Definition java_static_initializers.cpp:520

java_static_initializers.h

java_string_literal_expr.h

Representation of a constant Java string.

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

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

declaring_class

std::optional< irep_idt > declaring_class(const symbolt &symbol)

Gets the identifier of the class which declared a given symbol.

Definition java_utils.cpp:568

set_declaring_class

void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)

Sets the identifier of the class which declared a given symbol to declaring_class.

Definition java_utils.cpp:574

class_name_from_method_name

std::optional< std::string > class_name_from_method_name(const std::string &method_name)

Get JVM type name of the class in which method_name is defined.

Definition java_utils.cpp:580

get_inherited_component

std::optional< resolve_inherited_componentt::inherited_componentt > get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_table_baset &symbol_table, bool include_interfaces)

Finds an inherited component (method or field), taking component visibility into account.

Definition java_utils.cpp:448

java_utils.h

journalling_symbol_table.h

Author: Diffblue Ltd.

to_json_object

json_objectt & to_json_object(jsont &json)

Definition json.h:442

to_json_array

json_arrayt & to_json_array(jsont &json)

Definition json.h:424

parse_json

bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)

Definition json_parser.cpp:27

json_parser.h

create_invokedynamic_synthetic_classes

void create_invokedynamic_synthetic_classes(const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt::instructionst &instructions, symbol_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods, message_handlert &message_handler)

Definition lambda_synthesis.cpp:395

invokedynamic_synthetic_constructor

codet invokedynamic_synthetic_constructor(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)

Create invokedynamic synthetic constructor.

Definition lambda_synthesis.cpp:475

invokedynamic_synthetic_method

codet invokedynamic_synthetic_method(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)

Create the body for the synthetic method implementing an invokedynamic method.

Definition lambda_synthesis.cpp:773

lambda_synthesis.h

Java lambda code synthesis.

lift_clinit_calls

codet lift_clinit_calls(codet input)

file Static initializer call lifting

Definition lift_clinit_calls.cpp:21

lift_clinit_calls.h

build_load_method_by_regex

std::function< std::vector< irep_idt >(const symbol_table_baset &symbol_table)> build_load_method_by_regex(const std::string &pattern)

Create a lambda that returns the symbols that the given pattern should be loaded.If the pattern doesn...

Definition load_method_by_regex.cpp:58

load_method_by_regex.h

Process a pattern to use as a regex for selecting extra entry points for ci_lazy_methodst.

log

double log(double x)

Definition math.c:2416

options.h

Options.

to_pointer_type

const pointer_typet & to_pointer_type(const typet &type)

Cast a typet to a pointer_typet.

Definition pointer_expr.h:93

invariant.h

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

static_lifetime_init.h

INITIALIZE_FUNCTION

#define INITIALIZE_FUNCTION

Definition static_lifetime_init.h:24

to_side_effect_expr

side_effect_exprt & to_side_effect_expr(exprt &expr)

Definition std_code.h:1506

to_side_effect_expr_function_call

side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)

Definition std_code.h:1739

to_code

const codet & to_code(const exprt &expr)

Definition std_code_base.h:104

component

auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())

Definition std_expr.cpp:291

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

java_bytecode_language_optionst

Definition java_bytecode_language.h:202

java_bytecode_language_optionst::assert_uncaught_exceptions

bool assert_uncaught_exceptions

Definition java_bytecode_language.h:211

java_bytecode_language_optionst::assert_no_exceptions_thrown

bool assert_no_exceptions_thrown

Transform athrow bytecode instructions into assert FALSE followed by assume FALSE.

Definition java_bytecode_language.h:219

java_bytecode_language_optionst::nondet_static

bool nondet_static

Definition java_bytecode_language.h:214

java_bytecode_language_optionst::throw_runtime_exceptions

bool throw_runtime_exceptions

Definition java_bytecode_language.h:210

java_bytecode_language_optionst::should_lift_clinit_calls

bool should_lift_clinit_calls

Should we lift clinit calls in function bodies to the top? For example, turning if(x) A....

Definition java_bytecode_language.h:251

java_bytecode_language_optionst::java_cp_include_files

std::string java_cp_include_files

Definition java_bytecode_language.h:228

java_bytecode_language_optionst::method_context

std::optional< prefix_filtert > method_context

If set, method bodies are only elaborated if they pass the filter.

Definition java_bytecode_language.h:246

java_bytecode_language_optionst::lazy_methods_mode

lazy_methods_modet lazy_methods_mode

Definition java_bytecode_language.h:223

java_bytecode_language_optionst::string_refinement_enabled

bool string_refinement_enabled

Definition java_bytecode_language.h:209

java_bytecode_language_optionst::throw_assertion_error

bool throw_assertion_error

Definition java_bytecode_language.h:212

java_bytecode_language_optionst::assume_inputs_non_null

bool assume_inputs_non_null

assume inputs variables to be non-null

Definition java_bytecode_language.h:208

java_bytecode_language_optionst::ignore_manifest_main_class