don't mark the transformation as wrong when doing semantic over-approximations
also, change the limit of const inits to be over number of stores instead of number of bytes
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2990,7 +2990,7 @@ StateValue Store::toSMT(State &s) const {
// skip large initializers. FIXME: this should be moved to memory so it can
// fold subsequent trivial loads
if (s.isInitializationPhase() &&
- Memory::getStoreByteSize(val->getType()) > 128) {
+ Memory::getStoreByteSize(val->getType()) / (bits_byte / 8) > 128) {
s.doesApproximation("Large constant initializer removed");
return {};
}

MODIFY
tests/alive-tv/constexpr/large-const-opt.srctgt.ll
tests/alive-tv/constexpr/large-const-opt.srctgt.ll
; FIXME: this should work some day..
-; ERROR: Value mismatch
-; CHECK: Alive2 approximated the semantics
+; ERROR: Couldn't prove the correctness of the transformation
-@str = constant [129 x i8] c"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa\00", align 16
+@str = constant [129 x i8] c"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", align 16
define i8 @src(i32 %idx) {
%arrayidx = getelementptr inbounds [129 x i8], [129 x i8]* @str, i64 0, i32 %idx

MODIFY
tests/alive-tv/constexpr/large-const.srctgt.ll
tests/alive-tv/constexpr/large-const.srctgt.ll
-@str = constant [129 x i8] c"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa\00", align 16
+@str = constant [129 x i8] c"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", align 16
define i8 @src(i32 %idx) {
%arrayidx = getelementptr inbounds [129 x i8], [129 x i8]* @str, i64 0, i32 %idx

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -147,22 +147,25 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
auto &var_name = var ? var->getName() : empty;
auto &m = r.getModel();
- s << msg;
- if (!var_name.empty())
- s << " for " << *var;
-
auto &src_approx = src_state.getApproximations();
auto &tgt_approx = tgt_state.getApproximations();
if (!src_approx.empty() || !tgt_approx.empty()) {
- s << "\n\nNOTE: Alive2 approximated the semantics of this program.\n"
- "The bug found may be spurious. Approximations done:\n";
+ s << "Couldn't prove the correctness of the transformation\n"
+ "Alive2 approximated the semantics of the programs and therefore we\n"
+ "cannot conclude whether the bug found is valid or not.\n\n"
+ "Approximations done:\n";
auto approx = src_approx;
approx.insert(tgt_approx.begin(), tgt_approx.end());
for (auto *a : approx) {
s << " - " << a << '\n';
}
+ errs.add(s.str(), false);
+ return;
}
+ s << msg;
+ if (!var_name.empty())
+ s << " for " << *var;
s << "\n\nExample:\n";
for (auto &[var, val] : src_state.getValues()) {

don't mark the transformation as wrong when doing semantic over-approximations
also, change the limit of const inits to be over number of stores instead of number of bytes