Loading...

Searching...

No Matches

java_local_variable_table.cpp

Go to the documentation of this file.

1/*******************************************************************\

2

3Module: Java local variable table processing

4

5Author: Chris Smowton, chris.smowton@diffblue.com

6

7\*******************************************************************/

8

11

12#include "java_bytecode_convert_method_class.h"

13

14#include <util/arith_tools.h>

15#include <util/invariant.h>

16#include <util/string2int.h>

17#include <util/symbol_table_base.h>

18

19#include "java_types.h"

20

21#include <iostream>

22

23// Specialise the CFG representation to work over Java instead of GOTO programs.

24// This must be done at global scope due to template resolution rules.

25

26template <class T>

27 struct procedure_local_cfg_baset<

28 T,

29 java_bytecode_convert_methodt::method_with_amapt,

30 java_bytecode_convert_methodt::method_offsett>

31 : public grapht<

32 cfg_base_nodet<T, java_bytecode_convert_methodt::method_offsett>>

33{

34 typedef grapht<

35 cfg_base_nodet<T, java_bytecode_convert_methodt::method_offsett>>

36 base_grapht;

37 typedef typename base_grapht::nodet nodet;

38 typedef java_bytecode_convert_methodt::method_with_amapt method_with_amapt;

39 typedef std::map<java_bytecode_convert_methodt::method_offsett,

40 java_bytecode_convert_methodt::method_offsett>

41 entry_mapt;

42 typedef std::size_t entryt;

43 entry_mapt entry_map;

44

45 procedure_local_cfg_baset() {}

46

47 void operator()(const method_with_amapt &args)

48 {

49 const auto &method = args.method_with_amap.first;

50 const auto &amap = args.method_with_amap.second;

51 for(const auto &inst : amap)

52 {

53 // Map instruction PCs onto node indices:

54 entry_map[inst.first]=this->add_node();

55 // Map back:

56 (*this)[entry_map[inst.first]].PC=inst.first;

57 }

58 // Add edges declared in the address map:

59 for(const auto &inst : amap)

60 {

61 for(auto succ : inst.second.successors)

62 this->add_edge(entry_map.at(inst.first), entry_map.at(succ));

63 }

64 // Next, add edges declared in the exception table, which

65 // don't figure in the address map successors/predecessors as yet:

66 for(const auto &table_entry : method.exception_table)

67 {

68 auto findit=amap.find(table_entry.start_pc);

69 INVARIANT(

70 findit!=amap.end(),

71 "Exception table entry doesn't point to an instruction?");

72 for(; findit->first<table_entry.end_pc; ++findit)

73 {

74 // For now just assume any non-branch

75 // instruction could potentially throw.

76 auto succit=findit;

77 ++succit;

78 if(succit==amap.end())

79 continue;

80 const auto &thisinst=findit->second;

81 if(thisinst.successors.size()==1 &&

82 thisinst.successors.back()==succit->first)

83 {

84 this->add_edge(

85 entry_map.at(findit->first),

86 entry_map.at(table_entry.handler_pc));

87 }

88 }

89 }

90 }

91

92 java_bytecode_convert_methodt::method_offsett get_node_index(

93 const java_bytecode_convert_methodt::method_offsett &instruction) const

94{

95 return entry_map.at(instruction);

96 }

97

98 nodet &

99 get_node(const java_bytecode_convert_methodt::method_offsett &instruction)

100 {

101 return (*this)[get_node_index(instruction)];

102 }

103 const nodet &get_node(

104 const java_bytecode_convert_methodt::method_offsett &instruction) const

105{

106 return (*this)[get_node_index(instruction)];

107 }

108

109 static java_bytecode_convert_methodt::method_offsett

110 get_first_node(const method_with_amapt &args)

111 {

112 return args.method_with_amap.second.begin()->first;

113 }

114

115 static java_bytecode_convert_methodt::method_offsett

116 get_last_node(const method_with_amapt &args)

117 {

118 return (--args.method_with_amap.second.end())->first;

119 }

120

121 static bool nodes_empty(const method_with_amapt &args)

122 {

123 return args.method_with_amap.second.empty();

124 }

125};

126

127// Grab some class typedefs for brevity:

128typedef java_bytecode_convert_methodt::holet

129 holet;

130typedef java_bytecode_convert_methodt::local_variable_with_holest

131 local_variable_with_holest;

132typedef java_bytecode_convert_methodt::local_variable_table_with_holest

133 local_variable_table_with_holest;

134typedef java_bytecode_convert_methodt::address_mapt

135 address_mapt;

136typedef java_bytecode_convert_methodt::java_cfg_dominatorst

137 java_cfg_dominatorst;

138

139// Comparators for local variables:

140

141 static bool lt_index(

142 const local_variable_with_holest &a,

143 const local_variable_with_holest &b)

144{

145 return a.var.index<b.var.index;

146}

147 static bool lt_startpc(

148 const local_variable_with_holest *a,

149 const local_variable_with_holest *b)

150{

151 return a->var.start_pc<b->var.start_pc;

152}

153

154// The predecessor map, and a top-sorting comparator:

155

156typedef std::map<

157 local_variable_with_holest *,

158 std::set<local_variable_with_holest *> >

159 predecessor_mapt;

160

161 struct is_predecessor_oft

162{

163 const predecessor_mapt &order;

164

165 explicit is_predecessor_oft(const predecessor_mapt &_order) : order(_order) {}

166

167 bool operator()(

168 local_variable_with_holest *a,

169 local_variable_with_holest *b) const

170{

171 auto findit=order.find(a);

172 if(findit==order.end())

173 return false;

174 return findit->second.count(b)>0;

175 }

176};

177

178// Helper routines for the find-initializers code below:

179

185 static void gather_transitive_predecessors(

186 local_variable_with_holest *start,

187 const predecessor_mapt &predecessor_map,

188 std::set<local_variable_with_holest*> &result)

189{

190 if(!result.insert(start).second)

191 return;

192 auto findit=predecessor_map.find(start);

193 if(findit==predecessor_map.end())

194 return;

195 for(const auto pred : findit->second)

196 gather_transitive_predecessors(pred, predecessor_map, result);

197}

198

204 static bool is_store_to_slot(

205 const java_bytecode_convert_methodt::instructiont &inst,

206 unsigned slotidx)

207{

208 const std::string prevstatement = bytecode_info[inst.bytecode].mnemonic;

209

210 if(!(prevstatement.size()>=1 && prevstatement.substr(1, 5)=="store"))

211 return false;

212

213 unsigned storeslotidx;

214 if(inst.args.size()==1)

215 {

216 // Store with an argument:

217 const auto &arg=inst.args[0];

218 storeslotidx = numeric_cast_v<unsigned>(to_constant_expr(arg));

219 }

220 else

221 {

222 // Store shorthands, like "store_0", "store_1"

223 INVARIANT(

224 prevstatement[6]=='_' && prevstatement.size()==8,

225 "expected store instruction looks like store_0, store_1...");

226 std::string storeslot(1, prevstatement[7]);

227 INVARIANT(

228 isdigit(storeslot[0]),

229 "store_? instructions should end in a digit");

230 storeslotidx=safe_string2unsigned(storeslot);

231 }

232 return storeslotidx==slotidx;

233}

234

239 static void maybe_add_hole(

240 local_variable_with_holest &var,

241 java_bytecode_convert_methodt::method_offsett from,

242 java_bytecode_convert_methodt::method_offsett to)

243{

244 PRECONDITION(to>=from);

245 if(to!=from)

246 var.holes.push_back(

247 {from,

248 static_cast<java_bytecode_convert_methodt::method_offsett >(to - from)});

249}

250

258 static void populate_variable_address_map(

259 local_variable_table_with_holest::iterator firstvar,

260 local_variable_table_with_holest::iterator varlimit,

261 std::vector<local_variable_with_holest *> &live_variable_at_address)

262{

263 for(auto it=firstvar, itend=varlimit; it!=itend; ++it)

264 {

265 if(it->var.start_pc+it->var.length>live_variable_at_address.size())

266 live_variable_at_address.resize(it->var.start_pc+it->var.length);

267

268 for(auto idx = it->var.start_pc, idxlim = it->var.start_pc + it->var.length;

269 idx != idxlim;

270 ++idx)

271 {

272 INVARIANT(!live_variable_at_address[idx], "Local variable table clash?");

273 live_variable_at_address[idx]=&*it;

274 }

275 }

276}

277

303 static void populate_predecessor_map(

304 local_variable_table_with_holest::iterator firstvar,

305 local_variable_table_with_holest::iterator varlimit,

306 const std::vector<local_variable_with_holest *> &live_variable_at_address,

307 const address_mapt &amap,

308 predecessor_mapt &predecessor_map,

309 message_handlert &msg_handler)

310{

311 messaget msg(msg_handler);

312 for(auto it=firstvar, itend=varlimit; it!=itend; ++it)

313 {

314 // All entries of the "local_variable_table_with_holest" processed in this

315 // function concern the same Java Local Variable Table slot/register. This

316 // is because "find_initializers()" has already sorted them.

317 INVARIANT(

318 it->var.index==firstvar->var.index,

319 "all entries are for the same local variable slot");

320

321 // Parameters are irrelevant to us and shouldn't be changed. This is because

322 // they cannot have live predecessor ranges: they are initialized by the JVM

323 // and no other live variable range can flow into them.

324 if(it->is_parameter)

325 continue;

326

327#ifdef DEBUG

328 msg.debug() << "jcm: ppm: processing var idx " << it->var.index

329 << " name '" << it->var.name << "' start-pc "

330 << it->var.start_pc << " len " << it->var.length

331 << "; holes " << it->holes.size() << messaget::eom;

332#endif

333

334 // Find the last instruction within the live range:

335 const auto end_pc = it->var.start_pc + it->var.length;

336 auto amapit=amap.find(end_pc);

337 INVARIANT(

338 amapit!=amap.begin(),

339 "current bytecode shall not be the first");

340 auto old_amapit=amapit;

341 --amapit;

342 if(old_amapit==amap.end())

343 {

344 INVARIANT(

345 end_pc>amapit->first,

346 "Instruction live range doesn't align to instruction boundary?");

347 }

348

349 // Find vartable entries that flow into this one. For unknown reasons this

350 // loop iterates backwards, walking back from the last bytecode in the live

351 // range of variable it to the first one. For each value of the iterator

352 // "amapit" we search for instructions that jump into amapit's address

353 // (predecessors)

354 auto new_start_pc = it->var.start_pc;

355 for(; amapit->first>=it->var.start_pc; --amapit)

356 {

357 for(auto pred : amapit->second.predecessors)

358 {

359 // pred is the address (byecode offset) of a instruction that jumps into

360 // amapit. Compute now a pointer to the variable-with-holes whose index

361 // equals that of amapit and which was alive on instruction pred, or a

362 // null pointer if no such variable exists (e.g., because no live range

363 // covers that instruction)

364 auto pred_var=

365 (pred<live_variable_at_address.size() ?

366 live_variable_at_address[pred] :

367 nullptr);

368

369 // Three cases are now possible:

370 // 1. The predecessor instruction is in the same live range: nothing to

371 // do.

372 if(pred_var==&*it)

373 {

374 continue;

375 }

376 // 2. The predecessor instruction is in no live range among those for

377 // variable slot it->var.index

378 else if(!pred_var)

379 {

380 // Check if this is an initializer, and if so expand the live range

381 // to include it, but don't check its predecessors:

382 auto inst_before_this=amapit;

383 INVARIANT(

384 inst_before_this!=amap.begin(),

385 "we shall not be on the first bytecode of the method");

386 --inst_before_this;

387 if(amapit->first!=it->var.start_pc || inst_before_this->first!=pred)

388 {

389 // These sorts of infeasible edges can occur because jsr

390 // handling is presently vague (any subroutine is assumed to

391 // be able to return to any callsite)

392 msg.warning() << "Local variable table: ignoring flow from "

393 << "out of range for " << it->var.name << ' '

394 << pred << " -> " << amapit->first

395 << messaget::eom;

396 continue;

397 }

398 if(!is_store_to_slot(

399 *(inst_before_this->second.source),

400 it->var.index))

401 {

402 msg.warning() << "Local variable table: didn't find initializing "

403 << "store for predecessor of bytecode at address "

404 << amapit->first << " ("

405 << amapit->second.predecessors.size()

406 << " predecessors)" << msg.eom;

407 throw "local variable table: unexpected live ranges";

408 }

409 new_start_pc=pred;

410 }

411 // 3. Predecessor instruction is a different range associated to the

412 // same variable slot

413 else

414 {

415 if(pred_var->var.name!=it->var.name ||

416 pred_var->var.descriptor!=it->var.descriptor)

417 {

418 // These sorts of infeasible edges can occur because

419 // jsr handling is presently vague (any subroutine is

420 // assumed to be able to return to any callsite)

421 msg.warning() << "Local variable table: ignoring flow from "

422 << "clashing variable for "

423 << it->var.name << ' ' << pred << " -> "

424 << amapit->first << messaget::eom;

425 continue;

426 }

427 // OK, this is a flow from a similar but

428 // distinct entry in the local var table.

429 predecessor_map[&*it].insert(pred_var);

430 }

431 }

432 }

433

434 // If a simple pre-block initializer was found,

435 // add it to the live range now:

436 it->var.length+=(it->var.start_pc-new_start_pc);

437 it->var.start_pc=new_start_pc;

438 }

439}

440

448 static java_bytecode_convert_methodt::method_offsett get_common_dominator(

449 const std::set<local_variable_with_holest *> &merge_vars,

450 const java_cfg_dominatorst &dominator_analysis)

451{

452 PRECONDITION(!merge_vars.empty());

453

454 auto first_pc =

455 std::numeric_limits<java_bytecode_convert_methodt::method_offsett>::max();

456 for(auto v : merge_vars)

457 {

458 if(v->var.start_pc<first_pc)

459 first_pc=v->var.start_pc;

460 }

461

462 std::vector<java_bytecode_convert_methodt::method_offsett>

463 candidate_dominators;

464 for(auto v : merge_vars)

465 {

466 const auto &dominator_nodeidx=

467 dominator_analysis.cfg.entry_map.at(v->var.start_pc);

468 const auto &this_var_doms=

469 dominator_analysis.cfg[dominator_nodeidx].dominators;

470 for(const auto this_var_dom : this_var_doms)

471 if(this_var_dom<=first_pc)

472 candidate_dominators.push_back(this_var_dom);

473 }

474 std::sort(candidate_dominators.begin(), candidate_dominators.end());

475

476 // Working from the back, simply find the first PC

477 // that occurs merge_vars.size() times and therefore

478 // dominates all vars we seek to merge:

479 for(auto domit=candidate_dominators.rbegin(),

480 domitend=candidate_dominators.rend();

481 domit!=domitend;

482 /* Don't increment here */)

483 {

484 std::size_t repeats = 0;

485 auto dom=*domit;

486 while(domit!=domitend && *domit==dom)

487 {

488 ++domit;

489 ++repeats;

490 }

491 INVARIANT(repeats <= merge_vars.size(), "out of bounds");

492 if(repeats==merge_vars.size())

493 return dom;

494 }

495

496 throw "variable live ranges with no common dominator?";

497}

498

507 static void populate_live_range_holes(

508 local_variable_with_holest &merge_into,

509 const std::set<local_variable_with_holest *> &merge_vars,

510 java_bytecode_convert_methodt::method_offsett expanded_live_range_start)

511{

512 std::vector<local_variable_with_holest *> sorted_by_startpc(

513 merge_vars.begin(), merge_vars.end());

514 std::sort(sorted_by_startpc.begin(), sorted_by_startpc.end(), lt_startpc);

515

516 PRECONDITION(!sorted_by_startpc.empty());

517 maybe_add_hole(

518 merge_into,

519 expanded_live_range_start,

520 sorted_by_startpc[0]->var.start_pc);

521 for(auto it = std::next(sorted_by_startpc.begin());

522 it != sorted_by_startpc.end();

523 ++it)

524 {

525 auto &local_var = (*std::prev(it))->var;

526 maybe_add_hole(

527 merge_into, local_var.start_pc + local_var.length, (*it)->var.start_pc);

528 }

529}

530

539 static void merge_variable_table_entries(

540 local_variable_with_holest &merge_into,

541 const std::set<local_variable_with_holest *> &merge_vars,

542 const java_cfg_dominatorst &dominator_analysis,

543 std::ostream &debug_out)

544{

545 // Because we need a lexically-scoped declaration,

546 // we must have the merged variable

547 // enter scope both in a block that dominates all entries, and which

548 // precedes them in program order.

549 const auto found_dominator =

550 get_common_dominator(merge_vars, dominator_analysis);

551

552 // Populate the holes in the live range

553 // (addresses where the new variable will be in scope,

554 // but references to this stack slot should not resolve to it

555 // as it was not visible in the original local variable table)

556 populate_live_range_holes(merge_into, merge_vars, found_dominator);

557

558 java_bytecode_convert_methodt::method_offsett last_pc = 0;

559 for(auto v : merge_vars)

560 {

561 if(v->var.start_pc+v->var.length>last_pc)

562 last_pc=v->var.start_pc+v->var.length;

563 }

564

565 // Apply the changes:

566 merge_into.var.start_pc=found_dominator;

567 merge_into.var.length=last_pc-found_dominator;

568

569#ifdef DEBUG

570 debug_out << "Merged " << merge_vars.size() << " variables named "

571 << merge_into.var.name << "; new live range "

572 << merge_into.var.start_pc << '-'

573 << merge_into.var.start_pc + merge_into.var.length << '\n';

574#else

575 (void)debug_out; // unused parameter

576#endif

577

578 // Nuke the now-subsumed var-table entries:

579 for(auto &v : merge_vars)

580 if(v!=&merge_into)

581 v->var.length=0;

582}

583

597 void java_bytecode_convert_methodt::find_initializers_for_slot(

598 local_variable_table_with_holest::iterator firstvar,

599 local_variable_table_with_holest::iterator varlimit,

600 const address_mapt &amap,

601 const java_cfg_dominatorst &dominator_analysis)

602{

603 // Build a simple map from instruction PC to the variable

604 // live in this slot at that PC, and a map from each variable

605 // to variables that flow into it:

606 std::vector<local_variable_with_holest *> live_variable_at_address;

607 populate_variable_address_map(firstvar, varlimit, live_variable_at_address);

608

609 // Now find variables that flow together by

610 // walking backwards to find initializers

611 // or branches from other live ranges:

612 predecessor_mapt predecessor_map;

613 populate_predecessor_map(

614 firstvar,

615 varlimit,

616 live_variable_at_address,

617 amap,

618 predecessor_map,

619 log.get_message_handler());

620

621 // OK, we've established the flows all seem sensible.

622 // Now merge vartable entries according to the predecessor_map:

623

624 // Take the transitive closure of the predecessor map:

625 for(auto &kv : predecessor_map)

626 {

627 std::set<local_variable_with_holest *> closed_preds;

628 gather_transitive_predecessors(kv.first, predecessor_map, closed_preds);

629 kv.second=std::move(closed_preds);

630 }

631

632 // Top-sort so that we get the bottom variables first:

633 is_predecessor_oft comp(predecessor_map);

634 std::vector<local_variable_with_holest *> topsorted_vars;

635 for(auto it=firstvar, itend=varlimit; it!=itend; ++it)

636 topsorted_vars.push_back(&*it);

637

638 std::sort(topsorted_vars.begin(), topsorted_vars.end(), comp);

639

640 // Now merge the entries:

641 for(auto merge_into : topsorted_vars)

642 {

643 // Already merged into another variable?

644 if(merge_into->var.length==0)

645 continue;

646

647 auto findit=predecessor_map.find(merge_into);

648 // Nothing to do?

649 if(findit==predecessor_map.end())

650 continue;

651

652 const auto &merge_vars=findit->second;

653 INVARIANT(merge_vars.size()>=2, "merging requires at least 2 variables");

654

655 merge_variable_table_entries(

656 *merge_into, merge_vars, dominator_analysis, log.status());

657 }

658}

659

667 static void walk_to_next_index(

668 local_variable_table_with_holest::iterator &it1,

669 local_variable_table_with_holest::iterator &it2,

670 local_variable_table_with_holest::iterator itend)

671{

672 if(it2==itend)

673 {

674 it1=itend;

675 return;

676 }

677

678 auto old_it2=it2;

679 auto index=it2->var.index;

680 while(it2!=itend && it2->var.index==index)

681 ++it2;

682 it1=old_it2;

683}

684

691 void java_bytecode_convert_methodt::find_initializers(

692 local_variable_table_with_holest &vars,

693 const address_mapt &amap,

694 const java_cfg_dominatorst &dominator_analysis)

695{

696 // Sort table entries by local slot index:

697 std::sort(vars.begin(), vars.end(), lt_index);

698

699 // For each block of entries using a particular index,

700 // try to combine them:

701 auto it1=vars.begin();

702 auto it2=it1;

703 auto itend=vars.end();

704 walk_to_next_index(it1, it2, itend);

705 for(; it1!=itend; walk_to_next_index(it1, it2, itend))

706 find_initializers_for_slot(it1, it2, amap, dominator_analysis);

707}

708

712 static void cleanup_var_table(

713 std::vector<local_variable_with_holest> &vars_with_holes)

714{

715 size_t toremove=0;

716 for(size_t i=0; i<(vars_with_holes.size()-toremove); ++i)

717 {

718 auto &v=vars_with_holes[i];

719 if(v.var.length==0)

720 {

721 // Move to end; consider the new element we've swapped in:

722 ++toremove;

723 if(i!=vars_with_holes.size()-toremove) // Already where it needs to be?

724 std::swap(v, vars_with_holes[vars_with_holes.size()-toremove]);

725 --i; // May make i (size_t)-1, but it will immediately be

726 // re-incremented as the loop iterates.

727 }

728 }

729

730 // Remove un-needed entries.

731 vars_with_holes.resize(vars_with_holes.size()-toremove);

732}

733

740 void java_bytecode_convert_methodt::setup_local_variables(

741 const methodt &m,

742 const address_mapt &amap)

743{

744 // Compute CFG dominator tree

745 java_cfg_dominatorst dominator_analysis;

746 method_with_amapt dominator_args(m, amap);

747 dominator_analysis(dominator_args);

748

749#ifdef DEBUG

750 log.debug() << "jcm: setup-local-vars: m.is_static " << m.is_static

751 << " m.descriptor " << m.descriptor << messaget::eom;

752 log.debug() << "jcm: setup-local-vars: lv arg slots " << slots_for_parameters

753 << messaget::eom;

754 log.debug() << "jcm: setup-local-vars: lvt size "

755 << m.local_variable_table.size() << messaget::eom;

756#endif

757

758 // Find out which local variable table entries should be merged:

759 // Wrap each entry so we have a data structure to work during function calls,

760 // where we record live ranges with holes:

761 std::vector<local_variable_with_holest> vars_with_holes;

762 for(const auto &v : m.local_variable_table)

763 vars_with_holes.push_back({v, is_parameter(v), {}});

764

765 // Merge variable records. See documentation of in

766 // `find_initializers_for_slot` for more details. If the strategy employed

767 // there fails with an exception, we just ignore the LVT for this method, no

768 // variable is generated in `this->variables[]` (because we return here and

769 // dont let the for loop below to execute), and as a result the method

770 // this->variable() will be forced to create new `anonlocal::` variables, as

771 // the only source of variable names for that method is `this->variables[]`.

772 try

773 {

774 find_initializers(vars_with_holes, amap, dominator_analysis);

775 }

776 catch(const char *message)

777 {

778 log.warning() << "Bytecode -> codet translation error: " << message

779 << messaget::eom

780 << "This is probably due to an unexpected LVT, "

781 << "falling back to translation without LVT" << messaget::eom;

782 return;

783 }

784

785 // Clean up removed records from the variable table:

786 cleanup_var_table(vars_with_holes);

787

788 // Do the locals and parameters in the variable table, which is available when

789 // compiled with -g or for methods with many local variables in the latter

790 // case, different variables can have the same index, depending on the

791 // context.

792 //

793 // to calculate which variable to use, one uses the address of the instruction

794 // that uses the variable, the size of the instruction and the start_pc /

795 // length values in the local variable table

796 for(auto &v : vars_with_holes)

797 {

798 if(v.is_parameter)

799 continue;

800

801#ifdef DEBUG

802 log.debug() << "jcm: setup-local-vars: merged variable: idx " << v.var.index

803 << " name " << v.var.name << " v.var.descriptor '"

804 << v.var.descriptor << "' holes " << v.holes.size()

805 << messaget::eom;

806#endif

807

808 const std::string &method_name = id2string(method_id);

809 const size_t method_name_end = method_name.rfind(":(");

810 const size_t class_name_end = method_name.rfind('.', method_name_end);

811 INVARIANT(

812 method_name_end != std::string::npos &&

813 class_name_end != std::string::npos,

814 "A method name has the format class `.` method `:(`signature`)`.");

815 const std::string class_name = method_name.substr(0, class_name_end);

816

817 const typet t = v.var.signature.has_value()

818 ? *java_type_from_string_with_exception(

819 v.var.descriptor, v.var.signature, class_name)

820 : *java_type_from_string(v.var.descriptor);

821

822 std::ostringstream id_oss;

823 id_oss << method_id << "::" << v.var.start_pc << "::" << v.var.name;

824 irep_idt identifier(id_oss.str());

825 symbol_exprt result(identifier, t);

826 result.set(ID_C_base_name, v.var.name);

827

828 // Create a new local variable in the variables[] array, the result of

829 // merging multiple local variables with equal name (parameters excluded)

830 // into a single local variable with holes

831 variables[v.var.index].emplace_back(

832 result, v.var.start_pc, v.var.length, false, std::move(v.holes));

833

834 // Register the local variable in the symbol table

835 symbolt new_symbol{identifier, t, ID_java};

836 new_symbol.base_name=v.var.name;

837 new_symbol.pretty_name=id2string(identifier).substr(6, std::string::npos);

838 new_symbol.is_file_local=true;

839 new_symbol.is_thread_local=true;

840 new_symbol.is_lvalue=true;

841 symbol_table.add(new_symbol);

842 }

843}

844

851const java_bytecode_convert_methodt::variablet &

852 java_bytecode_convert_methodt::find_variable_for_slot(

853 size_t address,

854 variablest &var_list)

855{

856 for(const variablet &var : var_list)

857 {

858 size_t start_pc=var.start_pc;

859 size_t length=var.length;

860 if(address>=start_pc && address<(start_pc+length))

861 {

862 bool found_hole=false;

863 for(auto &hole : var.holes)

864 if(address>=hole.start_pc && address<(hole.start_pc+hole.length))

865 {

866 found_hole=true;

867 break;

868 }

869 if(found_hole)

870 continue;

871 return var;

872 }

873 }

874 // add unnamed local variable to end of list at this index

875 // with scope from 0 to SIZE_T_MAX

876 // as it is at the end of the vector, it will only be taken into account

877 // if no other variable is valid

878 var_list.emplace_back(

879 symbol_exprt(irep_idt(), typet()), 0, std::numeric_limits<size_t>::max());

880 return var_list.back();

881}

arith_tools.h

bytecode_info

struct bytecode_infot const bytecode_info[]

Definition bytecode_info.cpp:16

ait

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

Definition ai.h:566

cfg_baset::entry_mapt::at

entryt & at(const goto_programt::const_targett &t)

Definition cfg.h:137

cfg_baset::nodet

base_grapht::nodet nodet

Definition cfg.h:92

cfg_baset::get_node_index

entryt get_node_index(const goto_programt::const_targett &program_point) const

Get the graph node index for program_point.

Definition cfg.h:239

cfg_baset::entry_map

entry_mapt entry_map

Definition cfg.h:152

cfg_dominators_templatet

Dominator graph.

Definition cfg_dominators.h:37

dstringt

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

Definition dstring.h:38

grapht

A generic directed graph with a parametric node type.

Definition graph.h:167

grapht::add_node

node_indext add_node(arguments &&... values)

Definition graph.h:180

grapht::add_edge

void add_edge(node_indext a, node_indext b)

Definition graph.h:232

java_bytecode_convert_methodt::variablet

Definition java_bytecode_convert_method_class.h:126

java_bytecode_convert_methodt

Definition java_bytecode_convert_method_class.h:36

java_bytecode_convert_methodt::slots_for_parameters

method_offsett slots_for_parameters

Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...

Definition java_bytecode_convert_method_class.h:106

java_bytecode_convert_methodt::variablest

std::vector< variablet > variablest

Definition java_bytecode_convert_method_class.h:170

java_bytecode_convert_methodt::setup_local_variables

void setup_local_variables(const methodt &m, const address_mapt &amap)

See find_initializers_for_slot above for more detail.

Definition java_local_variable_table.cpp:740

java_bytecode_convert_methodt::find_variable_for_slot

const variablet & find_variable_for_slot(size_t address, variablest &var_list)

See above.

Definition java_local_variable_table.cpp:852

java_bytecode_convert_methodt::find_initializers

void find_initializers(local_variable_table_with_holest &vars, const address_mapt &amap, const java_cfg_dominatorst &doms)

See find_initializers_for_slot above for more detail.

Definition java_local_variable_table.cpp:691

java_bytecode_convert_methodt::local_variable_table_with_holest

std::vector< local_variable_with_holest > local_variable_table_with_holest

Definition java_bytecode_convert_method_class.h:123

java_bytecode_convert_methodt::find_initializers_for_slot

void find_initializers_for_slot(local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, const address_mapt &amap, const java_cfg_dominatorst &doms)

Given a sequence of users of the same local variable slot, this figures out which ones are related by...

Definition java_local_variable_table.cpp:597

java_bytecode_convert_methodt::is_parameter

bool is_parameter(const local_variablet &v)

Returns true iff the slot index of the local variable of a method (coming from the LVT) is a paramete...

Definition java_bytecode_convert_method_class.h:219

java_bytecode_convert_methodt::log

messaget log

Definition java_bytecode_convert_method_class.h:80

java_bytecode_convert_methodt::address_mapt

std::map< method_offsett, converted_instructiont > address_mapt

Definition java_bytecode_convert_method_class.h:242

java_bytecode_convert_methodt::method_offsett

uint16_t method_offsett

Definition java_bytecode_convert_method_class.h:77

message_handlert

Definition message.h:27

messaget

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

Definition message.h:154

messaget::debug

mstreamt & debug() const

Definition message.h:431

messaget::get_message_handler

message_handlert & get_message_handler()

Definition message.h:183

messaget::eom

static eomt eom

Definition message.h:289

messaget::status

mstreamt & status() const

Definition message.h:416

procedure_local_cfg_baset

Definition cfg.h:295

symbol_exprt

Expression to hold a symbol (variable)

Definition std_expr.h:132

symbolt

Symbol table entry.

Definition symbol.h:28

typet

The type of an expression, extends irept.

Definition type.h:29

isdigit

int isdigit(int c)

Definition ctype.c:24

id2string

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

Definition irep.h:44

java_bytecode_convert_method_class.h

JAVA Bytecode Language Conversion.

maybe_add_hole

static void maybe_add_hole(local_variable_with_holest &var, java_bytecode_convert_methodt::method_offsett from, java_bytecode_convert_methodt::method_offsett to)

See above.

Definition java_local_variable_table.cpp:239

predecessor_mapt

std::map< local_variable_with_holest *, std::set< local_variable_with_holest * > > predecessor_mapt

Definition java_local_variable_table.cpp:159

lt_index

static bool lt_index(const local_variable_with_holest &a, const local_variable_with_holest &b)

Definition java_local_variable_table.cpp:141

java_cfg_dominatorst

java_bytecode_convert_methodt::java_cfg_dominatorst java_cfg_dominatorst

Definition java_local_variable_table.cpp:137

populate_variable_address_map

static void populate_variable_address_map(local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, std::vector< local_variable_with_holest * > &live_variable_at_address)

See above.

Definition java_local_variable_table.cpp:258

is_store_to_slot

static bool is_store_to_slot(const java_bytecode_convert_methodt::instructiont &inst, unsigned slotidx)

See above.

Definition java_local_variable_table.cpp:204

populate_predecessor_map

static void populate_predecessor_map(local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, const std::vector< local_variable_with_holest * > &live_variable_at_address, const address_mapt &amap, predecessor_mapt &predecessor_map, message_handlert &msg_handler)

Populates the predecessor_map with a graph from local variable table entries to their predecessors (t...

Definition java_local_variable_table.cpp:303

populate_live_range_holes

static void populate_live_range_holes(local_variable_with_holest &merge_into, const std::set< local_variable_with_holest * > &merge_vars, java_bytecode_convert_methodt::method_offsett expanded_live_range_start)

See above.

Definition java_local_variable_table.cpp:507

lt_startpc

static bool lt_startpc(const local_variable_with_holest *a, const local_variable_with_holest *b)

Definition java_local_variable_table.cpp:147

address_mapt

java_bytecode_convert_methodt::address_mapt address_mapt

Definition java_local_variable_table.cpp:135

holet

java_bytecode_convert_methodt::holet holet

Definition java_local_variable_table.cpp:129

cleanup_var_table

static void cleanup_var_table(std::vector< local_variable_with_holest > &vars_with_holes)

See above.

Definition java_local_variable_table.cpp:712

get_common_dominator

static java_bytecode_convert_methodt::method_offsett get_common_dominator(const std::set< local_variable_with_holest * > &merge_vars, const java_cfg_dominatorst &dominator_analysis)

Used to find out where to put a variable declaration that subsumes several variable live ranges.

Definition java_local_variable_table.cpp:448

local_variable_with_holest

java_bytecode_convert_methodt::local_variable_with_holest local_variable_with_holest

Definition java_local_variable_table.cpp:131

walk_to_next_index

static void walk_to_next_index(local_variable_table_with_holest::iterator &it1, local_variable_table_with_holest::iterator &it2, local_variable_table_with_holest::iterator itend)

Walk a vector, a contiguous block of entries with equal slot index at a time.

Definition java_local_variable_table.cpp:667

merge_variable_table_entries

static void merge_variable_table_entries(local_variable_with_holest &merge_into, const std::set< local_variable_with_holest * > &merge_vars, const java_cfg_dominatorst &dominator_analysis, std::ostream &debug_out)

See above.

Definition java_local_variable_table.cpp:539

local_variable_table_with_holest

java_bytecode_convert_methodt::local_variable_table_with_holest local_variable_table_with_holest

Definition java_local_variable_table.cpp:133

gather_transitive_predecessors

static void gather_transitive_predecessors(local_variable_with_holest *start, const predecessor_mapt &predecessor_map, std::set< local_variable_with_holest * > &result)

See above.

Definition java_local_variable_table.cpp:185

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

java_type_from_string_with_exception

std::optional< typet > java_type_from_string_with_exception(const std::string &descriptor, const std::optional< std::string > &signature, const std::string &class_name)

Definition java_types.h:1140

log

double log(double x)

Definition math.c:2416

invariant.h

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