CBMC: /home/runner/work/cbmc/cbmc/src/goto-symex/goto_symex.cpp Source File

32 void goto_symext::do_simplify(exprt &expr, const value_sett &value_set)

33{

34 if(symex_config.simplify_opt)

35 {

36 simplify_expr_with_value_sett{value_set, language_mode, ns}.simplify(expr);

37 }

38}

40 void goto_symext::symex_assign(

41 statet &state,

42 const exprt &o_lhs,

43 const exprt &o_rhs)

44{

45 exprt lhs = clean_expr(o_lhs, state, true);

46 exprt rhs = clean_expr(o_rhs, state, false);

47

48 DATA_INVARIANT_WITH_DIAGNOSTICS(

49 lhs.type() == rhs.type(),

50 "assignments must be type consistent, got",

51 lhs.type().pretty(),

52 rhs.type().pretty(),

53 state.source.pc->source_location());

54

55 log.conditional_output(

56 log.debug(), [this, &lhs](messaget::mstreamt &mstream) {

57 mstream << "Assignment to " << format(lhs) << " ["

58 << pointer_offset_bits(lhs.type(), ns).value_or(0) << " bits]"

59 << messaget::eom;

60 });

61

62 // rvalues present within the lhs (for example, "some_array[this_rvalue]" or

63 // "byte_extract <type> from an_lvalue offset this_rvalue") can affect whether

64 // we use field-sensitive symbols or not, so L2-rename them up front:

65 lhs = state.l2_rename_rvalues(lhs, ns);

66 do_simplify(lhs, state.value_set);

67 lhs = state.field_sensitivity.apply(ns, state, std::move(lhs), true);

68

69 if(rhs.id() == ID_side_effect)

70 {

71 const side_effect_exprt &side_effect_expr = to_side_effect_expr(rhs);

72 const irep_idt &statement = side_effect_expr.get_statement();

73

74 if(

75 statement == ID_cpp_new || statement == ID_cpp_new_array ||

76 statement == ID_java_new_array_data)

77 {

78 symex_cpp_new(state, lhs, side_effect_expr);

79 }

80 else if(statement == ID_allocate)

81 symex_allocate(state, lhs, side_effect_expr);

82 else if(statement == ID_va_start)

83 symex_va_start(state, lhs, side_effect_expr);

84 else

85 UNREACHABLE;

86 }

87 else

88 {

89 assignment_typet assignment_type = symex_targett::assignment_typet::STATE;

90

91 // Let's hide return value assignments.

92 if(

93 lhs.id() == ID_symbol &&

94 id2string(to_symbol_expr(lhs).identifier()).find("#return_value!") !=

95 std::string::npos)

96 {

97 assignment_type = symex_targett::assignment_typet::HIDDEN;

98 }

99

100 // We hide if we are in a hidden function.

101 if(state.call_stack().top().hidden_function)

102 assignment_type = symex_targett::assignment_typet::HIDDEN;

103

104 // We hide if we are executing a hidden instruction.

105 if(state.source.pc->source_location().get_hide())

106 assignment_type = symex_targett::assignment_typet::HIDDEN;

107

108 symex_assignt symex_assign{

109 shadow_memory,

110 state,

111 assignment_type,

112 ns,

113 symex_config,

114 language_mode,

115 target};

116

117 // Try to constant propagate potential side effects of the assignment, when

118 // simplification is turned on and there is one thread only. Constant

119 // propagation is only sound for sequential code as here we do not take into

120 // account potential writes from other threads when propagating the values.

121 if(symex_config.simplify_opt && state.threads.size() <= 1)

122 {

123 if(constant_propagate_assignment_with_side_effects(

124 state, symex_assign, lhs, rhs))

125 return;

126 }

127

128 // We may end up reading (and writing) all components of an object composed

129 // of multiple fields. In such cases, we must do so atomically to avoid

130 // overwriting components modified by another thread. Note that this also

131 // implies multiple shared reads on the rhs being treated as atomic.

132 const bool maybe_divisible =

133 lhs.id() == ID_index ||

134 (is_ssa_expr(lhs) &&

135 state.field_sensitivity.is_divisible(to_ssa_expr(lhs), false));

136 const bool need_atomic_section = maybe_divisible &&

137 state.threads.size() > 1 &&

138 state.atomic_section_id == 0;

139

140 if(need_atomic_section)

141 symex_atomic_begin(state);

142

143 exprt::operandst lhs_if_then_else_conditions;

144 symex_assignt{

145 shadow_memory,

146 state,

147 assignment_type,

148 ns,

149 symex_config,

150 language_mode,

151 target}

152 .assign_rec(lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions);

153

154 if(need_atomic_section)

155 symex_atomic_end(state);

156 }

157}

166 static std::string get_alnum_string(const array_exprt &char_array)

167{

168 const auto &ibv_type =

169 to_integer_bitvector_type(to_array_type(char_array.type()).element_type());

170

171 const std::size_t n_bits = ibv_type.get_width();

172 CHECK_RETURN(n_bits % 8 == 0);

173

174 static_assert(CHAR_BIT == 8, "bitwidth of char assumed to be 8");

175

176 const std::size_t n_chars = n_bits / 8;

177

178 INVARIANT(

179 sizeof(std::size_t) >= n_chars,

180 "size_t shall be large enough to represent a character");

181

182 std::string result;

183

184 for(const auto &c : char_array.operands())

185 {

186 const std::size_t c_val = numeric_cast_v<std::size_t>(to_constant_expr(c));

187

188 for(std::size_t i = 0; i < n_chars; i++)

189 {

190 const char c_chunk = static_cast<char>((c_val >> (i * 8)) & 0xff);

191 result.push_back(c_chunk);

192 }

193 }

194

195 return escape_non_alnum(result);

196}

198 bool goto_symext::constant_propagate_assignment_with_side_effects(

199 statet &state,

200 symex_assignt &symex_assign,

201 const exprt &lhs,

202 const exprt &rhs)

203{

204 if(rhs.id() == ID_function_application)

205 {

206 const function_application_exprt &f_l1 = to_function_application_expr(rhs);

207

208 if(f_l1.function().id() == ID_symbol)

209 {

210 const irep_idt &func_id = to_symbol_expr(f_l1.function()).identifier();

211

212 if(func_id == ID_cprover_string_concat_func)

213 {

214 return constant_propagate_string_concat(state, symex_assign, f_l1);

215 }

216 else if(func_id == ID_cprover_string_empty_string_func)

217 {

218 // constant propagating the empty string always succeeds as it does

219 // not depend on potentially non-constant inputs

220 constant_propagate_empty_string(state, symex_assign, f_l1);

221 return true;

222 }

223 else if(func_id == ID_cprover_string_substring_func)

224 {

225 return constant_propagate_string_substring(state, symex_assign, f_l1);

226 }

227 else if(

228 func_id == ID_cprover_string_of_int_func ||

229 func_id == ID_cprover_string_of_long_func)

230 {

231 return constant_propagate_integer_to_string(state, symex_assign, f_l1);

232 }

233 else if(func_id == ID_cprover_string_delete_char_at_func)

234 {

235 return constant_propagate_delete_char_at(state, symex_assign, f_l1);

236 }

237 else if(func_id == ID_cprover_string_delete_func)

238 {

239 return constant_propagate_delete(state, symex_assign, f_l1);

240 }

241 else if(func_id == ID_cprover_string_set_length_func)

242 {

243 return constant_propagate_set_length(state, symex_assign, f_l1);

244 }

245 else if(func_id == ID_cprover_string_char_set_func)

246 {

247 return constant_propagate_set_char_at(state, symex_assign, f_l1);

248 }

249 else if(func_id == ID_cprover_string_trim_func)

250 {

251 return constant_propagate_trim(state, symex_assign, f_l1);

252 }

253 else if(func_id == ID_cprover_string_to_lower_case_func)

254 {

255 return constant_propagate_case_change(state, symex_assign, f_l1, false);

256 }

257 else if(func_id == ID_cprover_string_to_upper_case_func)

258 {

259 return constant_propagate_case_change(state, symex_assign, f_l1, true);

260 }

261 else if(func_id == ID_cprover_string_replace_func)

262 {

263 return constant_propagate_replace(state, symex_assign, f_l1);

264 }

265 }

266 }

267

268 return false;

269}

271 void goto_symext::assign_string_constant(

272 statet &state,

273 symex_assignt &symex_assign,

274 const ssa_exprt &length,

275 const constant_exprt &new_length,

276 const ssa_exprt &char_array,

277 const array_exprt &new_char_array)

278{

279 // We need to make sure that the length of the previous array isn't

280 // unconstrained, otherwise it could be arbitrarily large which causes

281 // invalid traces

282 symex_assume(state, equal_exprt{length, from_integer(0, length.type())});

283

284 // assign length of string

285 symex_assign.assign_symbol(length, expr_skeletont{}, new_length, {});

286

287 const std::string aux_symbol_name =

288 get_alnum_string(new_char_array) + "_constant_char_array";

289

290 const bool string_constant_exists =

291 state.symbol_table.has_symbol(aux_symbol_name);

292

293 const symbolt &aux_symbol =

294 string_constant_exists

295 ? state.symbol_table.lookup_ref(aux_symbol_name)

296 : get_new_string_data_symbol(

297 state, symex_assign, aux_symbol_name, char_array, new_char_array);

298

299 INVARIANT(

300 aux_symbol.value == new_char_array,

301 "symbol shall have value derived from char array content");

302

303 const address_of_exprt string_data(

304 index_exprt(aux_symbol.symbol_expr(), from_integer(0, c_index_type())));

305

306 symex_assign.assign_symbol(char_array, expr_skeletont{}, string_data, {});

307

308 if(!string_constant_exists)

309 {

310 associate_array_to_pointer(

311 state, symex_assign, new_char_array, string_data);

312 }

313}

315 const symbolt &goto_symext::get_new_string_data_symbol(

316 statet &state,

317 symex_assignt &symex_assign,

318 const std::string &aux_symbol_name,

319 const ssa_exprt &char_array,

320 const array_exprt &new_char_array)

321{

322 array_typet new_char_array_type = new_char_array.type();

323 new_char_array_type.set(ID_C_constant, true);

324

325 symbolt &new_aux_symbol = get_fresh_aux_symbol(

326 new_char_array_type,

327 "",

328 aux_symbol_name,

329 source_locationt(),

330 ns.lookup(to_symbol_expr(char_array.get_original_expr())).mode,

331 ns,

332 state.symbol_table);

333

334 CHECK_RETURN(new_aux_symbol.is_state_var);

335 CHECK_RETURN(new_aux_symbol.is_lvalue);

336

337 new_aux_symbol.is_static_lifetime = true;

338 new_aux_symbol.is_file_local = false;

339 new_aux_symbol.is_thread_local = false;

340

341 new_aux_symbol.value = new_char_array;

342

343 const exprt arr = state.rename(new_aux_symbol.symbol_expr(), ns).get();

344

345 symex_assign.assign_symbol(

346 to_ssa_expr(arr).get_l1_object(), expr_skeletont{}, new_char_array, {});

347

348 return new_aux_symbol;

349}

351 void goto_symext::associate_array_to_pointer(

352 statet &state,

353 symex_assignt &symex_assign,

354 const array_exprt &new_char_array,

355 const address_of_exprt &string_data)

356{

357 const symbolt &function_symbol =

358 ns.lookup(ID_cprover_associate_array_to_pointer_func);

359

360 const function_application_exprt array_to_pointer_app{

361 function_symbol.symbol_expr(), {new_char_array, string_data}};

362

363 symbol_exprt return_symbol_expr =

364 get_fresh_aux_symbol(

365 to_mathematical_function_type(function_symbol.type).codomain(),

366 "",

367 "return_value",

368 source_locationt(),

369 function_symbol.mode,

370 ns,

371 state.symbol_table)

372 .symbol_expr();

373

374 const ssa_exprt ssa_expr(return_symbol_expr);

375

376 symex_assign.assign_symbol(

377 ssa_expr, expr_skeletont{}, array_to_pointer_app, {});

378}

381 goto_symext::try_evaluate_constant_string(

382 const statet &state,

383 const exprt &content)

384{

385 if(content.id() != ID_symbol)

386 {

387 return {};

388 }

389

390 const auto s_pointer_opt =

391 state.propagation.find(to_symbol_expr(content).identifier());

392

393 if(!s_pointer_opt)

394 {

395 return {};

396 }

397

398 return try_get_string_data_array(s_pointer_opt->get(), ns);

399}

402 goto_symext::try_evaluate_constant(const statet &state, const exprt &expr)

403{

404 if(expr.id() != ID_symbol)

405 {

406 return {};

407 }

408

409 const auto constant_expr_opt =

410 state.propagation.find(to_symbol_expr(expr).identifier());

411

412 if(!constant_expr_opt || !constant_expr_opt->get().is_constant())

413 {

414 return {};

415 }

416

417 return std::optional<std::reference_wrapper<const constant_exprt>>(

418 to_constant_expr(constant_expr_opt->get()));

419}

421 void goto_symext::constant_propagate_empty_string(

422 statet &state,

423 symex_assignt &symex_assign,

424 const function_application_exprt &f_l1)

425{

426 const auto &f_type = f_l1.function_type();

427 const auto &length_type = f_type.domain().at(0);

428 const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();

429

430 const constant_exprt length = from_integer(0, length_type);

431

432 const array_typet char_array_type(char_type, length);

433

434 DATA_INVARIANT(

435 f_l1.arguments().size() >= 2,

436 "empty string primitive requires two output arguments");

437

438 const array_exprt char_array({}, char_array_type);

439

440 assign_string_constant(

441 state,

442 symex_assign,

443 to_ssa_expr(f_l1.arguments().at(0)),

444 length,

445 to_ssa_expr(f_l1.arguments().at(1)),

446 char_array);

447}

449 bool goto_symext::constant_propagate_string_concat(

450 statet &state,

451 symex_assignt &symex_assign,

452 const function_application_exprt &f_l1)

453{

454 const auto &f_type = f_l1.function_type();

455 const auto &length_type = f_type.domain().at(0);

456 const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();

457

458 const refined_string_exprt &s1 = to_string_expr(f_l1.arguments().at(2));

459 const auto s1_data_opt = try_evaluate_constant_string(state, s1.content());

460

461 if(!s1_data_opt)

462 return false;

463

464 const array_exprt &s1_data = s1_data_opt->get();

465

466 const refined_string_exprt &s2 = to_string_expr(f_l1.arguments().at(3));

467 const auto s2_data_opt = try_evaluate_constant_string(state, s2.content());

468

469 if(!s2_data_opt)

470 return false;

471

472 const array_exprt &s2_data = s2_data_opt->get();

473

474 const std::size_t new_size =

475 s1_data.operands().size() + s2_data.operands().size();

476

477 const constant_exprt new_char_array_length =

478 from_integer(new_size, length_type);

479

480 const array_typet new_char_array_type(char_type, new_char_array_length);

481

482 exprt::operandst operands(s1_data.operands());

483 operands.insert(

484 operands.end(), s2_data.operands().begin(), s2_data.operands().end());

485

486 const array_exprt new_char_array(std::move(operands), new_char_array_type);

487

488 assign_string_constant(

489 state,

490 symex_assign,

491 to_ssa_expr(f_l1.arguments().at(0)),

492 new_char_array_length,

493 to_ssa_expr(f_l1.arguments().at(1)),

494 new_char_array);

495

496 return true;

497}

499 bool goto_symext::constant_propagate_string_substring(

500 statet &state,

501 symex_assignt &symex_assign,

502 const function_application_exprt &f_l1)

503{

504 const std::size_t num_operands = f_l1.arguments().size();

505

506 PRECONDITION(num_operands >= 4);

507 PRECONDITION(num_operands <= 5);

508

509 const auto &f_type = f_l1.function_type();

510 const auto &length_type = f_type.domain().at(0);

511 const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();

512

513 const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));

514 const auto s_data_opt = try_evaluate_constant_string(state, s.content());

515

516 if(!s_data_opt)

517 return false;

518

519 const array_exprt &s_data = s_data_opt->get();

520

521 mp_integer end_index;

522

523 if(num_operands == 5)

524 {

525 const auto end_index_expr_opt =

526 try_evaluate_constant(state, f_l1.arguments().at(4));

527

528 if(!end_index_expr_opt)

529 {

530 return false;

531 }

532

533 end_index =

534 numeric_cast_v<mp_integer>(to_constant_expr(*end_index_expr_opt));

535

536 if(end_index < 0 || end_index > s_data.operands().size())

537 {

538 return false;

539 }

540 }

541 else

542 {

543 end_index = s_data.operands().size();

544 }

545

546 const auto start_index_expr_opt =

547 try_evaluate_constant(state, f_l1.arguments().at(3));

548

549 if(!start_index_expr_opt)

550 {

551 return false;

552 }

553

554 const mp_integer start_index =

555 numeric_cast_v<mp_integer>(to_constant_expr(*start_index_expr_opt));

556

557 if(start_index < 0 || start_index > end_index)

558 {

559 return false;

560 }

561

562 const constant_exprt new_char_array_length =

563 from_integer(end_index - start_index, length_type);

564

565 const array_typet new_char_array_type(char_type, new_char_array_length);

566

567 exprt::operandst operands(

568 std::next(

569 s_data.operands().begin(), numeric_cast_v<std::size_t>(start_index)),

570 std::next(

571 s_data.operands().begin(), numeric_cast_v<std::size_t>(end_index)));

572

573 const array_exprt new_char_array(std::move(operands), new_char_array_type);

574

575 assign_string_constant(

576 state,

577 symex_assign,

578 to_ssa_expr(f_l1.arguments().at(0)),

579 new_char_array_length,

580 to_ssa_expr(f_l1.arguments().at(1)),

581 new_char_array);

582

583 return true;

584}

586 bool goto_symext::constant_propagate_integer_to_string(

587 statet &state,

588 symex_assignt &symex_assign,

589 const function_application_exprt &f_l1)

590{

591 // The function application expression f_l1 takes the following arguments:

592 // - result string length (output parameter)

593 // - result string data array (output parameter)

594 // - integer to convert to a string

595 // - radix (optional, default 10)

596 const std::size_t num_operands = f_l1.arguments().size();

597

598 PRECONDITION(num_operands >= 3);

599 PRECONDITION(num_operands <= 4);

600

601 const auto &f_type = f_l1.function_type();

602 const auto &length_type = f_type.domain().at(0);

603 const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();

604

605 const auto &integer_opt =

606 try_evaluate_constant(state, f_l1.arguments().at(2));

607

608 if(!integer_opt)

609 {

610 return false;

611 }

612

613 const mp_integer integer = numeric_cast_v<mp_integer>(integer_opt->get());

614

615 unsigned base = 10;

616

617 if(num_operands == 4)

618 {

619 const auto &base_constant_opt =

620 try_evaluate_constant(state, f_l1.arguments().at(3));

621

622 if(!base_constant_opt)

623 {

624 return false;

625 }

626

627 const auto base_opt = numeric_cast<unsigned>(base_constant_opt->get());

628

629 if(!base_opt)

630 {

631 return false;

632 }

633

634 base = *base_opt;

635 }

636

637 std::string s = integer2string(integer, base);

638

639 const constant_exprt new_char_array_length =

640 from_integer(s.length(), length_type);

641

642 const array_typet new_char_array_type(char_type, new_char_array_length);

643

644 exprt::operandst operands;

645

646 std::transform(

647 s.begin(),

648 s.end(),

649 std::back_inserter(operands),

650 [&char_type](const char c) { return from_integer(tolower(c), char_type); });

651

652 const array_exprt new_char_array(std::move(operands), new_char_array_type);

653

654 assign_string_constant(

655 state,

656 symex_assign,

657 to_ssa_expr(f_l1.arguments().at(0)),

658 new_char_array_length,

659 to_ssa_expr(f_l1.arguments().at(1)),

660 new_char_array);

661

662 return true;

663}

665 bool goto_symext::constant_propagate_delete_char_at(

666 statet &state,

667 symex_assignt &symex_assign,

668 const function_application_exprt &f_l1)

669{

670 // The function application expression f_l1 takes the following arguments:

671 // - result string length (output parameter)

672 // - result string data array (output parameter)

673 // - string to delete char from

674 // - index of char to delete

675 PRECONDITION(f_l1.arguments().size() == 4);

676

677 const auto &f_type = f_l1.function_type();

678 const auto &length_type = f_type.domain().at(0);

679 const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();

680

681 const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));

682 const auto s_data_opt = try_evaluate_constant_string(state, s.content());

683

684 if(!s_data_opt)

685 {

686 return false;

687 }

688

689 const array_exprt &s_data = s_data_opt->get();

690

691 const auto &index_opt = try_evaluate_constant(state, f_l1.arguments().at(3));

692

693 if(!index_opt)

694 {

695 return false;

696 }

697

698 const mp_integer index = numeric_cast_v<mp_integer>(index_opt->get());

699

700 if(index < 0 || index >= s_data.operands().size())

701 {

702 return false;

703 }

704

705 const constant_exprt new_char_array_length =

706 from_integer(s_data.operands().size() - 1, length_type);

707

708 const array_typet new_char_array_type(char_type, new_char_array_length);

709

710 exprt::operandst operands;

711 operands.reserve(s_data.operands().size() - 1);

712

713 const std::size_t i = numeric_cast_v<std::size_t>(index);

714

715 operands.insert(

716 operands.end(),

717 s_data.operands().begin(),

718 std::next(s_data.operands().begin(), i));

719

720 operands.insert(

721 operands.end(),

722 std::next(s_data.operands().begin(), i + 1),

723 s_data.operands().end());

724

725 const array_exprt new_char_array(std::move(operands), new_char_array_type);

726

727 assign_string_constant(

728 state,

729 symex_assign,

730 to_ssa_expr(f_l1.arguments().at(0)),

731 new_char_array_length,

732 to_ssa_expr(f_l1.arguments().at(1)),

733 new_char_array);

734

735 return true;

736}

738 bool goto_symext::constant_propagate_delete(

739 statet &state,

740 symex_assignt &symex_assign,

741 const function_application_exprt &f_l1)

742{

743 // The function application expression f_l1 takes the following arguments:

744 // - result string length (output parameter)

745 // - result string data array (output parameter)

746 // - string to delete substring from

747 // - index of start of substring to delete (inclusive)

748 // - index of end of substring to delete (exclusive)

749 PRECONDITION(f_l1.arguments().size() == 5);

750

751 const auto &f_type = f_l1.function_type();

752 const auto &length_type = f_type.domain().at(0);

753 const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();

754

755 const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));

756 const auto s_data_opt = try_evaluate_constant_string(state, s.content());

757

758 if(!s_data_opt)

759 {

760 return false;

761 }

762

763 const array_exprt &s_data = s_data_opt->get();

764

765 const auto &start_opt = try_evaluate_constant(state, f_l1.arguments().at(3));

766

767 if(!start_opt)

768 {

769 return false;

770 }

771

772 const mp_integer start = numeric_cast_v<mp_integer>(start_opt->get());

773

774 if(start < 0 || start > s_data.operands().size())

775 {

776 return false;

777 }

778

779 const auto &end_opt = try_evaluate_constant(state, f_l1.arguments().at(4));

780

781 if(!end_opt)

782 {

783 return false;

784 }

785

786 const mp_integer end = numeric_cast_v<mp_integer>(end_opt->get());

787

788 if(start > end)

789 {

790 return false;

791 }

792

793 const std::size_t start_index = numeric_cast_v<std::size_t>(start);

794

795 const std::size_t end_index =

796 std::min(numeric_cast_v<std::size_t>(end), s_data.operands().size());

797

798 const std::size_t new_size =

799 s_data.operands().size() - end_index + start_index;

800

801 const constant_exprt new_char_array_length =

802 from_integer(new_size, length_type);

803

804 const array_typet new_char_array_type(char_type, new_char_array_length);

805

806 exprt::operandst operands;

807 operands.reserve(new_size);

808

809 operands.insert(

810 operands.end(),

811 s_data.operands().begin(),

812 std::next(s_data.operands().begin(), start_index));

813

814 operands.insert(

815 operands.end(),

816 std::next(s_data.operands().begin(), end_index),

817 s_data.operands().end());

818

819 const array_exprt new_char_array(std::move(operands), new_char_array_type);

820

821 assign_string_constant(

822 state,

823 symex_assign,

824 to_ssa_expr(f_l1.arguments().at(0)),

825 new_char_array_length,

826 to_ssa_expr(f_l1.arguments().at(1)),

827 new_char_array);

828

829 return true;

830}

832 bool goto_symext::constant_propagate_set_length(

833 statet &state,

834 symex_assignt &symex_assign,

835 const function_application_exprt &f_l1)

836{

837 // The function application expression f_l1 takes the following arguments:

838 // - result string length (output parameter)

839 // - result string data array (output parameter)

840 // - current string

841 // - new length of the string

842 PRECONDITION(f_l1.arguments().size() == 4);

843

844 const auto &f_type = f_l1.function_type();

845 const auto &length_type = f_type.domain().at(0);

846 const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();

847

848 const auto &new_length_opt =

849 try_evaluate_constant(state, f_l1.arguments().at(3));

850

851 if(!new_length_opt)

852 {

853 return false;

854 }

855

856 const mp_integer new_length =

857 numeric_cast_v<mp_integer>(new_length_opt->get());

858

859 if(new_length < 0)

860 {

861 return false;

862 }

863

864 const std::size_t new_size = numeric_cast_v<std::size_t>(new_length);

865

866 const constant_exprt new_char_array_length =

867 from_integer(new_size, length_type);

868

869 const array_typet new_char_array_type(char_type, new_char_array_length);

870

871 exprt::operandst operands;

872

873 if(new_size != 0)

874 {

875 operands.reserve(new_size);

876

877 const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));

878 const auto s_data_opt = try_evaluate_constant_string(state, s.content());

879

880 if(!s_data_opt)

881 {

882 return false;

883 }

884

885 const array_exprt &s_data = s_data_opt->get();

886

887 operands.insert(

888 operands.end(),

889 s_data.operands().begin(),

890 std::next(

891 s_data.operands().begin(),

892 std::min(new_size, s_data.operands().size())));

893

894 operands.insert(

895 operands.end(),

896 new_size - std::min(new_size, s_data.operands().size()),

897 from_integer(0, char_type));

898 }

899

900 const array_exprt new_char_array(std::move(operands), new_char_array_type);

901

902 assign_string_constant(

903 state,

904 symex_assign,

905 to_ssa_expr(f_l1.arguments().at(0)),

906 new_char_array_length,

907 to_ssa_expr(f_l1.arguments().at(1)),

908 new_char_array);

909

910 return true;

911}

913 bool goto_symext::constant_propagate_set_char_at(

914 statet &state,

915 symex_assignt &symex_assign,

916 const function_application_exprt &f_l1)

917{

918 // The function application expression f_l1 takes the following arguments:

919 // - result string length (output parameter)

920 // - result string data array (output parameter)

921 // - current string

922 // - index of char to set

923 // - new char

924 PRECONDITION(f_l1.arguments().size() == 5);

925

926 const auto &f_type = f_l1.function_type();

927 const auto &length_type = f_type.domain().at(0);

928 const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();

929

930 const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));

931 const auto s_data_opt = try_evaluate_constant_string(state, s.content());

932

933 if(!s_data_opt)

934 {

935 return false;

936 }

937

938 array_exprt s_data = s_data_opt->get();

939

940 const auto &index_opt = try_evaluate_constant(state, f_l1.arguments().at(3));

941

942 if(!index_opt)

943 {

944 return false;

945 }

946

947 const mp_integer index = numeric_cast_v<mp_integer>(index_opt->get());

948

949 if(index < 0 || index >= s_data.operands().size())

950 {

951 return false;

952 }

953

954 const auto &new_char_opt =

955 try_evaluate_constant(state, f_l1.arguments().at(4));

956

957 if(!new_char_opt)

958 {

959 return false;

960 }

961

962 const constant_exprt new_char_array_length =

963 from_integer(s_data.operands().size(), length_type);

964

965 const array_typet new_char_array_type(char_type, new_char_array_length);

966

967 s_data.operands()[numeric_cast_v<std::size_t>(index)] = new_char_opt->get();

968

969 const array_exprt new_char_array(

970 std::move(s_data.operands()), new_char_array_type);

971

972 assign_string_constant(

973 state,

974 symex_assign,

975 to_ssa_expr(f_l1.arguments().at(0)),

976 new_char_array_length,

977 to_ssa_expr(f_l1.arguments().at(1)),

978 new_char_array);

979

980 return true;

981}

983 bool goto_symext::constant_propagate_case_change(

984 statet &state,

985 symex_assignt &symex_assign,

986 const function_application_exprt &f_l1,

987 bool to_upper)

988{

989 const auto &f_type = f_l1.function_type();

990 const auto &length_type = f_type.domain().at(0);

991 const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();

992

993 const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));

994 const auto s_data_opt = try_evaluate_constant_string(state, s.content());

995

996 if(!s_data_opt)

997 return false;

998

999 array_exprt string_data = s_data_opt->get();

1000

1001 auto &operands = string_data.operands();

1002 for(auto &operand : operands)

1003 {

1004 auto &constant_value = to_constant_expr(operand);

1005 auto character = numeric_cast_v<unsigned int>(constant_value);

1006

1007 // Can't guarantee matches against non-ASCII characters.

1008 if(character >= 128)

1009 return false;

1010

1011 if(isalpha(character))

1012 {

1013 if(to_upper)

1014 {

1015 if(islower(character))

1016 constant_value =

1017 from_integer(toupper(character), constant_value.type());

1018 }

1019 else

1020 {

1021 if(isupper(character))

1022 constant_value =

1023 from_integer(tolower(character), constant_value.type());

1024 }

1025 }

1026 }

1027

1028 const constant_exprt new_char_array_length =

1029 from_integer(operands.size(), length_type);

1030

1031 const array_typet new_char_array_type(char_type, new_char_array_length);

1032 const array_exprt new_char_array(std::move(operands), new_char_array_type);

1033

1034 assign_string_constant(

1035 state,

1036 symex_assign,

1037 to_ssa_expr(f_l1.arguments().at(0)),

1038 new_char_array_length,

1039 to_ssa_expr(f_l1.arguments().at(1)),

1040 new_char_array);

1041

1042 return true;

1043}

1045 bool goto_symext::constant_propagate_replace(

1046 statet &state,

1047 symex_assignt &symex_assign,

1048 const function_application_exprt &f_l1)

1049{

1050 const auto &f_type = f_l1.function_type();

1051 const auto &length_type = f_type.domain().at(0);

1052 const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();

1053

1054 const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));

1055 const auto s_data_opt = try_evaluate_constant_string(state, s.content());

1056

1057 if(!s_data_opt)

1058 return false;

1059

1060 auto &new_data = f_l1.arguments().at(4);

1061 auto &old_data = f_l1.arguments().at(3);

1062

1063 array_exprt::operandst characters_to_find;

1064 array_exprt::operandst characters_to_replace;

1065

1066 // Two main ways to perform a replace: characters or strings.

1067 bool is_single_character = new_data.type().id() == ID_unsignedbv &&

1068 old_data.type().id() == ID_unsignedbv;

1069 if(is_single_character)

1070 {

1071 const auto new_char_pointer = try_evaluate_constant(state, new_data);

1072 const auto old_char_pointer = try_evaluate_constant(state, old_data);

1073

1074 if(!new_char_pointer || !old_char_pointer)

1075 {

1076 return {};

1077 }

1078

1079 characters_to_find.emplace_back(old_char_pointer->get());

1080 characters_to_replace.emplace_back(new_char_pointer->get());

1081 }

1082 else

1083 {

1084 auto &new_char_array = to_string_expr(new_data);

1085 auto &old_char_array = to_string_expr(old_data);

1086

1087 const auto new_char_array_opt =

1088 try_evaluate_constant_string(state, new_char_array.content());

1089

1090 const auto old_char_array_opt =

1091 try_evaluate_constant_string(state, old_char_array.content());

1092

1093 if(!new_char_array_opt || !old_char_array_opt)

1094 {

1095 return {};

1096 }

1097

1098 characters_to_find = old_char_array_opt->get().operands();

1099 characters_to_replace = new_char_array_opt->get().operands();

1100 }

1101

1102 // Copy data, then do initial search for a replace sequence.

1103 array_exprt existing_data = s_data_opt->get();

1104 auto found_pattern = std::search(

1105 existing_data.operands().begin(),

1106 existing_data.operands().end(),

1107 characters_to_find.begin(),

1108 characters_to_find.end());

1109

1110 // If we've found a match, proceed to perform a replace on all instances.

1111 while(found_pattern != existing_data.operands().end())

1112 {

1113 // Find the difference between our first/last match iterator.

1114 auto match_end = found_pattern + characters_to_find.size();

1115

1116 // Erase them.

1117 found_pattern = existing_data.operands().erase(found_pattern, match_end);

1118

1119 // Insert our replacement characters, then move the iterator to the end of

1120 // our new sequence.

1121 found_pattern = existing_data.operands().insert(

1122 found_pattern,

1123 characters_to_replace.begin(),

1124 characters_to_replace.end()) +

1125 characters_to_replace.size();

1126

1127 // Then search from there for any additional matches.

1128 found_pattern = std::search(

1129 found_pattern,

1130 existing_data.operands().end(),

1131 characters_to_find.begin(),

1132 characters_to_find.end());

1133 }

1134

1135 const constant_exprt new_char_array_length =

1136 from_integer(existing_data.operands().size(), length_type);

1137

1138 const array_typet new_char_array_type(char_type, new_char_array_length);

1139 const array_exprt new_char_array(

1140 std::move(existing_data.operands()), new_char_array_type);

1141

1142 assign_string_constant(

1143 state,

1144 symex_assign,

1145 to_ssa_expr(f_l1.arguments().at(0)),

1146 new_char_array_length,

1147 to_ssa_expr(f_l1.arguments().at(1)),

1148 new_char_array);

1149

1150 return true;

1151}

1153 bool goto_symext::constant_propagate_trim(

1154 statet &state,

1155 symex_assignt &symex_assign,

1156 const function_application_exprt &f_l1)

1157{

1158 const auto &f_type = f_l1.function_type();

1159 const auto &length_type = f_type.domain().at(0);

1160 const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();

1161

1162 const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));

1163 const auto s_data_opt = try_evaluate_constant_string(state, s.content());

1164

1165 if(!s_data_opt)

1166 return false;

1167

1168 auto is_not_whitespace = [](const exprt &expr) {

1169 auto character = numeric_cast_v<unsigned int>(to_constant_expr(expr));

1170 return character > ' ';

1171 };

1172

1173 // Note the points where a trim would trim too.

1174 auto &operands = s_data_opt->get().operands();

1175 auto end_iter =

1176 std::find_if(operands.rbegin(), operands.rend(), is_not_whitespace);

1177 auto start_iter =

1178 std::find_if(operands.begin(), operands.end(), is_not_whitespace);

1179

1180 // Then copy in the string with leading/trailing whitespace removed.

1181 // Note: if start_iter == operands.end it means the entire string is

1182 // whitespace, so we'll trim it to be empty anyway.

1183 exprt::operandst new_operands;

1184 if(start_iter != operands.end())

1185 new_operands = exprt::operandst{start_iter, end_iter.base()};

1186

1187 const constant_exprt new_char_array_length =

1188 from_integer(new_operands.size(), length_type);

1189

1190 const array_typet new_char_array_type(char_type, new_char_array_length);

1191 const array_exprt new_char_array(

1192 std::move(new_operands), new_char_array_type);

1193

1194 assign_string_constant(

1195 state,

1196 symex_assign,

1197 to_ssa_expr(f_l1.arguments().at(0)),

1198 new_char_array_length,

1199 to_ssa_expr(f_l1.arguments().at(1)),

1200 new_char_array);

1201

1202 return true;

1203}

from_integer

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

Definition arith_tools.cpp:100

arith_tools.h

to_integer_bitvector_type

const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)

Cast a typet to an integer_bitvector_typet.

Definition bitvector_types.h:214

char_type

bitvector_typet char_type()

Definition c_types.cpp:106

c_index_type

bitvector_typet c_index_type()

Definition c_types.cpp:16

c_types.h

address_of_exprt

Operator to return the address of an object.

Definition pointer_expr.h:540

ait

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

Definition ai.h:566

array_exprt

Array constructor from list of elements.

Definition std_expr.h:1570

array_typet

Arrays with given size.

Definition std_types.h:806

call_stackt::top

framet & top()

Definition call_stack.h:17

constant_exprt

A constant literal expression.

Definition std_expr.h:3007

dstringt

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

Definition dstring.h:38

equal_exprt

Equality.

Definition std_expr.h:1339

expr_skeletont

Expression in which some part is missing and can be substituted for another expression.

Definition expr_skeleton.h:26

exprt

Base class for all expressions.

Definition expr.h:57

exprt::operandst

std::vector< exprt > operandst

Definition expr.h:59

exprt::type

typet & type()

Return the type of the expression.

Definition expr.h:85

field_sensitivityt::apply

exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const

Turn an expression expr into a field-sensitive SSA expression.

Definition field_sensitivity.cpp:154

field_sensitivityt::is_divisible

bool is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const

Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...

Definition field_sensitivity.cpp:617

framet::hidden_function

bool hidden_function

Definition frame.h:40

function_application_exprt

Application of (mathematical) function.

Definition mathematical_expr.h:213

goto_statet::atomic_section_id

unsigned atomic_section_id

Threads.

Definition goto_state.h:76

goto_statet::propagation

sharing_mapt< irep_idt, exprt > propagation

Definition goto_state.h:71

goto_statet::value_set

value_sett value_set

Uses level 1 names, and is used to do dereferencing.

Definition goto_state.h:51

goto_symex_statet

Central data structure: state.

Definition goto_symex_state.h:42

goto_symex_statet::call_stack

call_stackt & call_stack()

Definition goto_symex_state.h:147

goto_symex_statet::l2_rename_rvalues

exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)

Definition goto_symex_state.cpp:305

goto_symex_statet::rename

renamedt< exprt, level > rename(exprt expr, const namespacet &ns)

Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...

Definition goto_symex_state.cpp:163

goto_symex_statet::symbol_table

symbol_tablet symbol_table

contains symbols that are minted during symbolic execution, such as dynamically created objects etc.

Definition goto_symex_state.h:67

goto_symex_statet::field_sensitivity

field_sensitivityt field_sensitivity

Definition goto_symex_state.h:122

goto_symex_statet::source

symex_targett::sourcet source

Definition goto_symex_state.h:62

goto_symex_statet::threads

std::vector< threadt > threads

Definition goto_symex_state.h:199

goto_symext::symex_assume

virtual void symex_assume(statet &state, const exprt &cond)

Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption.

Definition symex_main.cpp:199

goto_symext::symex_atomic_begin

virtual void symex_atomic_begin(statet &state)

Symbolically execute an ATOMIC_BEGIN instruction.

Definition symex_atomic_section.cpp:16

goto_symext::language_mode

irep_idt language_mode

language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...

Definition goto_symex.h:240

goto_symext::constant_propagate_delete_char_at

bool constant_propagate_delete_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)

Attempt to constant propagate deleting a character from a string.

Definition goto_symex.cpp:665

goto_symext::constant_propagate_set_char_at

bool constant_propagate_set_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)

Attempt to constant propagate setting the char at the given index.

Definition goto_symex.cpp:913

goto_symext::constant_propagate_assignment_with_side_effects

bool constant_propagate_assignment_with_side_effects(statet &state, symex_assignt &symex_assign, const exprt &lhs, const exprt &rhs)

Attempt to constant propagate side effects of the assignment (if any)

Definition goto_symex.cpp:198

goto_symext::constant_propagate_delete

bool constant_propagate_delete(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)

Attempt to constant propagate deleting a substring from a string.

Definition goto_symex.cpp:738

goto_symext::try_evaluate_constant

static std::optional< std::reference_wrapper< const constant_exprt > > try_evaluate_constant(const statet &state, const exprt &expr)

Definition goto_symex.cpp:402

goto_symext::constant_propagate_empty_string

void constant_propagate_empty_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)

Create an empty string constant.

Definition goto_symex.cpp:421

goto_symext::target

symex_target_equationt & target

The equation that this execution is building up.

Definition goto_symex.h:264

goto_symext::constant_propagate_case_change

bool constant_propagate_case_change(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1, bool to_upper)

Attempt to constant propagate case changes, both upper and lower.

Definition goto_symex.cpp:983

goto_symext::symex_allocate

virtual void symex_allocate(statet &state, const exprt &lhs, const side_effect_exprt &code)

Symbolically execute an assignment instruction that has an allocate on the right hand side.

Definition symex_builtin_functions.cpp:48

goto_symext::constant_propagate_integer_to_string

bool constant_propagate_integer_to_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)

Attempt to constant propagate converting an integer to a string.

Definition goto_symex.cpp:586

goto_symext::clean_expr

exprt clean_expr(exprt expr, statet &state, bool write)

Clean up an expression.

Definition symex_clean_expr.cpp:231

goto_symext::constant_propagate_trim

bool constant_propagate_trim(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)

Attempt to constant propagate trim operations.

Definition goto_symex.cpp:1153

goto_symext::shadow_memory

shadow_memoryt shadow_memory

Shadow memory instrumentation API.

Definition goto_symex.h:837

goto_symext::symex_va_start

virtual void symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &)

Definition symex_builtin_functions.cpp:248

goto_symext::ns

namespacet ns

Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...

Definition goto_symex.h:256

goto_symext::do_simplify

virtual void do_simplify(exprt &expr, const value_sett &value_set)

Definition goto_symex.cpp:32

goto_symext::symex_assign

void symex_assign(statet &state, const exprt &lhs, const exprt &rhs)

Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.

Definition goto_symex.cpp:40

goto_symext::get_new_string_data_symbol

const symbolt & get_new_string_data_symbol(statet &state, symex_assignt &symex_assign, const std::string &aux_symbol_name, const ssa_exprt &char_array, const array_exprt &new_char_array)

Installs a new symbol in the symbol table to represent the given character array, and assigns the cha...

Definition goto_symex.cpp:315

goto_symext::associate_array_to_pointer

void associate_array_to_pointer(statet &state, symex_assignt &symex_assign, const array_exprt &new_char_array, const address_of_exprt &string_data)

Generate array to pointer association primitive.

Definition goto_symex.cpp:351

goto_symext::symex_cpp_new

virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)

Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes.

Definition symex_builtin_functions.cpp:493

goto_symext::constant_propagate_set_length

bool constant_propagate_set_length(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)

Attempt to constant propagate setting the length of a string.

Definition goto_symex.cpp:832

goto_symext::log

messaget log

The messaget to write log messages to.

Definition goto_symex.h:276

goto_symext::symex_config

const symex_configt symex_config

The configuration to use for this symbolic execution.

Definition goto_symex.h:186

goto_symext::constant_propagate_string_substring

bool constant_propagate_string_substring(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)

Attempt to constant propagate getting a substring of a string.

Definition goto_symex.cpp:499

goto_symext::constant_propagate_replace

bool constant_propagate_replace(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)

Attempt to constant proagate character replacement.

Definition goto_symex.cpp:1045

goto_symext::constant_propagate_string_concat

bool constant_propagate_string_concat(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)

Attempt to constant propagate string concatenation.

Definition goto_symex.cpp:449

goto_symext::symex_atomic_end

virtual void symex_atomic_end(statet &state)

Symbolically execute an ATOMIC_END instruction.

Definition symex_atomic_section.cpp:36

goto_symext::assign_string_constant

void assign_string_constant(statet &state, symex_assignt &symex_assign, const ssa_exprt &length, const constant_exprt &new_length, const ssa_exprt &char_array, const array_exprt &new_char_array)

Assign constant string length and string data given by a char array to given ssa variables.

Definition goto_symex.cpp:271

goto_symext::try_evaluate_constant_string

std::optional< std::reference_wrapper< const array_exprt > > try_evaluate_constant_string(const statet &state, const exprt &content)

Definition goto_symex.cpp:381

index_exprt

Array index operator.

Definition std_expr.h:1431

irept::pretty

std::string pretty(unsigned indent=0, unsigned max_indent=0) const

Definition irep.cpp:482

irept::id

const irep_idt & id() const

Definition irep.h:388

messaget::mstreamt

Definition message.h:216

messaget::debug

mstreamt & debug() const

Definition message.h:431

messaget::conditional_output

void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const

Generate output to message_stream using output_generator if the configured verbosity is at least as h...

Definition message.cpp:149

namespacet::lookup

bool lookup(const irep_idt &name, const symbolt *&symbol) const override

See documentation for namespace_baset::lookup().

Definition namespace.cpp:134

refined_string_exprt

Definition string_expr.h:110

refined_string_exprt::content

const exprt & content() const

Definition string_expr.h:139

side_effect_exprt

An expression containing a side effect.

Definition std_code.h:1450

simplify_expr_with_value_sett

Definition simplify_expr_with_value_set.h:17

source_locationt

Definition source_location.h:20

ssa_exprt

Expression providing an SSA-renamed symbol of expressions.

Definition ssa_expr.h:17

symbol_exprt

Expression to hold a symbol (variable)

Definition std_expr.h:132

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

const symbolt & lookup_ref(const irep_idt &name) const

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

Definition symbol_table_base.h:105

symbolt

Symbol table entry.

Definition symbol.h:28

symbolt::symbol_expr

class symbol_exprt symbol_expr() const

Produces a symbol_exprt for a symbol.

Definition symbol.cpp:121

symex_assignt

Functor for symex assignment.

Definition symex_assign.h:28

symex_targett::assignment_typet

assignment_typet

Definition symex_target.h:69

symex_targett::assignment_typet::STATE

@ STATE

symex_targett::assignment_typet::HIDDEN

@ HIDDEN

value_sett

State type in value_set_domaint, used in value-set analysis and goto-symex.

Definition value_set.h:43

isalpha

int isalpha(int c)

Definition ctype.c:9

islower

int islower(int c)

Definition ctype.c:34

toupper

int toupper(int c)

Definition ctype.c:134

tolower

int tolower(int c)

Definition ctype.c:109

isupper

int isupper(int c)

Definition ctype.c:90

expr_skeleton.h

Expression skeleton.

format_expr.h

get_fresh_aux_symbol

symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)

Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...

Definition fresh_symbol.cpp:32

fresh_symbol.h

Fresh auxiliary symbol creation.

get_alnum_string

static std::string get_alnum_string(const array_exprt &char_array)

Maps the given array expression containing constant characters to a string containing only alphanumer...

Definition goto_symex.cpp:166

goto_symex.h

Symbolic Execution.

id2string

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

Definition irep.h:44

mathematical_expr.h

API to expression classes for 'mathematical' expressions.

to_function_application_expr

const function_application_exprt & to_function_application_expr(const exprt &expr)

Cast an exprt to a function_application_exprt.

Definition mathematical_expr.h:263

mathematical_types.h

Mathematical types.

to_mathematical_function_type

const mathematical_function_typet & to_mathematical_function_type(const typet &type)

Cast a typet to a mathematical_function_typet.

Definition mathematical_types.h:134

integer2string

const std::string integer2string(const mp_integer &n, unsigned base)

Definition mp_arith.cpp:103

to_pointer_type

const pointer_typet & to_pointer_type(const typet &type)

Cast a typet to a pointer_typet.

Definition pointer_expr.h:93

pointer_offset_size.h

Pointer Logic.

simplify_expr_with_value_set.h

try_get_string_data_array

std::optional< std::reference_wrapper< const array_exprt > > try_get_string_data_array(const exprt &content, const namespacet &ns)

Get char sequence from content field of a refined string expression.

Definition simplify_utils.cpp:489

simplify_utils.h

CHECK_RETURN

#define CHECK_RETURN(CONDITION)

Definition invariant.h:495

UNREACHABLE

#define UNREACHABLE

This should be used to mark dead code.

Definition invariant.h:525

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

DATA_INVARIANT_WITH_DIAGNOSTICS

#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)

Definition invariant.h:535

is_ssa_expr

bool is_ssa_expr(const exprt &expr)

Definition ssa_expr.h:125

to_ssa_expr

const ssa_exprt & to_ssa_expr(const exprt &expr)

Cast a generic exprt to an ssa_exprt.

Definition ssa_expr.h:145

std_code.h

to_side_effect_expr

side_effect_exprt & to_side_effect_expr(exprt &expr)

Definition std_code.h:1506

to_constant_expr

const constant_exprt & to_constant_expr(const exprt &expr)

Cast an exprt to a constant_exprt.

Definition std_expr.h:3078

to_symbol_expr

const symbol_exprt & to_symbol_expr(const exprt &expr)

Cast an exprt to a symbol_exprt.

Definition std_expr.h:221

to_array_type

const array_typet & to_array_type(const typet &type)

Cast a typet to an array_typet.

Definition std_types.h:887

string_expr.h

String expressions for the string solver.

to_string_expr

refined_string_exprt & to_string_expr(exprt &expr)

Definition string_expr.h:151

escape_non_alnum

std::string escape_non_alnum(std::string_view to_escape)

Replace non-alphanumeric characters with _xx escapes, where xx are hex digits.

Definition string_utils.cpp:155

string_utils.h

symex_targett::sourcet::pc

goto_programt::const_targett pc

Definition symex_target.h:42

symex_assign.h

Symbolic Execution of assignments.