MCPcopy Create free account
hub / github.com/AliveToolkit/alive2 / valueToBytes

Function valueToBytes

ir/memory.cpp:591–629  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

589}
590
591static vector<Byte> valueToBytes(const StateValue &val, const Type &fromType,
592 const Memory &mem, State &s) {
593 vector<Byte> bytes;
594 if (fromType.isPtrType()) {
595 Pointer p(mem, val.value);
596 unsigned bytesize = bits_program_pointer / bits_byte;
597
598 // constant global can't store pointers that alias with local blocks
599 if (s.isInitializationPhase() && !p.isLocal().isFalse()) {
600 expr bid = expr::mkUInt(0, 1).concat(p.getShortBid());
601 p = Pointer(mem, bid, p.getOffset(), p.getAttrs());
602 }
603
604 for (unsigned i = 0; i < bytesize; ++i)
605 bytes.emplace_back(mem, StateValue(expr(p()), expr(val.non_poison)), i);
606 } else {
607 assert(!fromType.isAggregateType() || isNonPtrVector(fromType));
608 StateValue bvval = fromType.toInt(s, val);
609 unsigned bitsize = bvval.bits();
610 unsigned bytesize = divide_up(bitsize, bits_byte);
611
612 // There are no sub-byte accesses in assembly
613 if (mem.isAsmMode() && (bitsize % 8) != 0) {
614 s.addUB(expr(false));
615 }
616
617 pad(bvval, bytesize * bits_byte - bitsize, s);
618 unsigned np_mul = bits_poison_per_byte;
619
620 for (unsigned i = 0; i < bytesize; ++i) {
621 StateValue data {
622 bvval.value.extract((i + 1) * bits_byte - 1, i * bits_byte),
623 bvval.non_poison.extract((i + 1) * np_mul - 1, i * np_mul)
624 };
625 bytes.emplace_back(mem, data, bitsize, i);
626 }
627 }
628 return bytes;
629}
630
631static StateValue bytesToValue(const Memory &m, const vector<Byte> &bytes,
632 const Type &toType) {

Callers 2

storeMethod · 0.85
memsetMethod · 0.85

Calls 15

PointerClass · 0.85
isNonPtrVectorFunction · 0.85
divide_upFunction · 0.85
padFunction · 0.85
isPtrTypeMethod · 0.80
isInitializationPhaseMethod · 0.80
isFalseMethod · 0.80
isLocalMethod · 0.80
getShortBidMethod · 0.80
getOffsetMethod · 0.80
getAttrsMethod · 0.80
isAggregateTypeMethod · 0.80

Tested by

no test coverage detected