add support for willreturn function calls
issue
MODIFY
ir/state.cpp
ir/state.cpp
@@ -623,6 +623,8 @@ void State::addUB(AndExpr &&ubs) {
}
void State::addNoReturn(const expr &cond) {
+ if (cond.isFalse())
+ return;
return_memory.add(memory, domain.path && cond);
function_domain.add(domain() && cond);
return_undef_vars.insert(undef_vars.begin(), undef_vars.end());
@@ -635,7 +637,7 @@ void State::addNoReturn(const expr &cond) {
expr State::FnCallInput::operator==(const FnCallInput &rhs) const {
if (readsmem != rhs.readsmem ||
argmemonly != rhs.argmemonly ||
- noret != rhs.noret ||
+ noret != rhs.noret || willret != rhs.willret ||
(readsmem && (fncall_ranges != rhs.fncall_ranges || is_neq(m <=> rhs.m))))
return false;
@@ -654,9 +656,11 @@ expr State::FnCallInput::refinedBy(
State &s, const vector<StateValue> &args_nonptr2,
const vector<Memory::PtrInput> &args_ptr2,
const ValueAnalysis::FnCallRanges &fncall_ranges2,
- const Memory &m2, bool readsmem2, bool argmemonly2, bool noret2) const {
+ const Memory &m2, bool readsmem2, bool argmemonly2, bool noret2,
+ bool willret2) const {
- if (readsmem != readsmem2 || argmemonly != argmemonly2 || noret != noret2 ||
+ if (readsmem != readsmem2 || argmemonly != argmemonly2 ||
+ noret != noret2 || willret != willret2 ||
(readsmem && !fncall_ranges.overlaps(fncall_ranges2)))
return false;
@@ -740,8 +744,11 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
bool writes_memory = !attrs.has(FnAttrs::NoWrite);
bool argmemonly = attrs.has(FnAttrs::ArgMemOnly);
bool noret = attrs.has(FnAttrs::NoReturn);
+ bool willret = attrs.has(FnAttrs::WillReturn);
bool noundef = attrs.has(FnAttrs::NoUndef);
+ assert(!noret || !willret);
+
bool all_valid = std::all_of(inputs.begin(), inputs.end(),
[](auto &v) { return v.isValid(); }) &&
std::all_of(ptr_inputs.begin(), ptr_inputs.end(),
@@ -770,7 +777,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
reads_memory ? analysis.ranges_fn_calls
: State::ValueAnalysis::FnCallRanges(),
reads_memory ? memory : Memory(*this),
- reads_memory, argmemonly, noret });
+ reads_memory, argmemonly, noret, willret });
auto &I = call_data_pair.first;
bool inserted = call_data_pair.second;
@@ -794,7 +801,9 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
string noret_name = name + "#noreturn";
I->second
= { move(values), expr::mkFreshVar(ub_name.c_str(), false),
- noret ? expr(true) : expr::mkFreshVar(noret_name.c_str(), false),
+ (noret || willret)
+ ? expr(noret)
+ : expr::mkFreshVar(noret_name.c_str(), false),
writes_memory
? memory.mkCallState(name,
argmemonly ? &I->first.args_ptr : nullptr,
@@ -824,7 +833,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
for (auto &[in, out] : fn_call_data[name]) {
auto refined = in.refinedBy(*this, inputs, ptr_inputs,
analysis.ranges_fn_calls, memory,
- reads_memory, argmemonly, noret);
+ reads_memory, argmemonly, noret, willret);
data.add(out, move(refined));
}

MODIFY
ir/state.h
ir/state.h
@@ -135,14 +135,14 @@ private:
std::vector<Memory::PtrInput> args_ptr;
ValueAnalysis::FnCallRanges fncall_ranges;
Memory m;
- bool readsmem, argmemonly, noret;
+ bool readsmem, argmemonly, noret, willret;
smt::expr operator==(const FnCallInput &rhs) const;
smt::expr refinedBy(State &s, const std::vector<StateValue> &args_nonptr,
const std::vector<Memory::PtrInput> &args_ptr,
const ValueAnalysis::FnCallRanges &fncall_ranges,
const Memory &m, bool readsmem, bool argmemonly,
- bool noret) const;
+ bool noret, bool willret) const;
auto operator<=>(const FnCallInput &rhs) const = default;
};

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -1220,6 +1220,10 @@ public:
attrs.set(FnAttrs::NoReturn);
break;
+ case llvm::Attribute::WillReturn:
+ attrs.set(FnAttrs::WillReturn);
+ break;
+
default:
break;
}

ADD
tests/unit/call-root.opt
+; TEST-ARGS: -root-only
+
+ %c = call i32 @f(i32 3) nowrite willreturn
+ %d = call i32 @f(i32 3) nowrite willreturn
+ %r = icmp eq i32 %c, %d
+ ret %r
+=>
+ ret true

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -232,6 +232,8 @@ space+ {
"call" { return CALL; }
"noread" { return NOREAD; }
"nowrite" { return NOWRITE; }
+"noreturn" { return NORETURN; }
+"willreturn" { return WILLRETURN; }
"freeze" { return FREEZE; }
"malloc" { return MALLOC; }
"free" { return FREE; }

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -1005,6 +1005,8 @@ static unique_ptr<Instr> parse_call(string_view name) {
switch (auto t = *tokenizer) {
case NOREAD: attrs.set(FnAttrs::NoRead); break;
case NOWRITE: attrs.set(FnAttrs::NoWrite); break;
+ case NORETURN: attrs.set(FnAttrs::NoReturn); break;
+ case WILLRETURN: attrs.set(FnAttrs::WillReturn); break;
default:
tokenizer.unget(t);
goto exit;

MODIFY
tools/tokens.h
tools/tokens.h
@@ -86,6 +86,8 @@ TOKEN(NINF)
TOKEN(NNAN)
TOKEN(NOREAD)
TOKEN(NOWRITE)
+TOKEN(NORETURN)
+TOKEN(WILLRETURN)
TOKEN(NSZ)
TOKEN(NSW)
TOKEN(NULLTOKEN)

add support for willreturn function calls
issue #375