From e61b8f476f9bdc6ace6138753f06c55b8f7f12db Mon Sep 17 00:00:00 2001 From: Kamil Dudka Date: Fri, 11 Oct 2024 17:59:17 +0200 Subject: [PATCH 1/4] sl: disable certain shortcuts with full error recovery Predator keeps error recovery cheap in the default configuration. The special handling of `VO_DEREF_FAILED` on three places can now be disabled by setting `SE_ERROR_RECOVERY_MODE == 2`. Related: https://github.com/kdudka/predator/pull/102 --- sl/symexec.cc | 2 +- sl/symjoin.cc | 3 ++- sl/symproc.cc | 3 ++- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/sl/symexec.cc b/sl/symexec.cc index 6c230bd64..47a6563bf 100644 --- a/sl/symexec.cc +++ b/sl/symexec.cc @@ -512,7 +512,7 @@ void SymExecEngine::execCondInsn() } const EValueOrigin origin = sh.valOrigin(val); - if (VO_DEREF_FAILED == origin) { + if (GlConf::data.errorRecoveryMode < 2 && VO_DEREF_FAILED == origin) { // error should have been already emitted CL_DEBUG_MSG(lw_, "ignored VO_DEREF_FAILED"); return; diff --git a/sl/symjoin.cc b/sl/symjoin.cc index cc49c5c0a..7d886e653 100644 --- a/sl/symjoin.cc +++ b/sl/symjoin.cc @@ -643,7 +643,8 @@ EValueOrigin joinOrigin(const EValueOrigin vo1, const EValueOrigin vo2) // use any return vo2; - if (VO_DEREF_FAILED == vo1 || VO_DEREF_FAILED == vo2) + if (GlConf::data.errorRecoveryMode < 2 + && (VO_DEREF_FAILED == vo1 || VO_DEREF_FAILED == vo2)) // keep the error recovery as cheap as possible return VO_DEREF_FAILED; diff --git a/sl/symproc.cc b/sl/symproc.cc index 9bc0dfecb..30974a3eb 100644 --- a/sl/symproc.cc +++ b/sl/symproc.cc @@ -1389,7 +1389,8 @@ void SymExecCore::execFree( // fall through! case VT_UNKNOWN: - if (VO_DEREF_FAILED == sh_.valOrigin(val)) + if (GlConf::data.errorRecoveryMode < 2 + && VO_DEREF_FAILED == sh_.valOrigin(val)) return; CL_ERROR_MSG(lw_, "invalid " << fnc); From 99918595723b2abe38522261b06aac0e0ec62cef Mon Sep 17 00:00:00 2001 From: Kamil Dudka Date: Fri, 11 Oct 2024 18:09:28 +0200 Subject: [PATCH 2/4] symproc: make `lhsFromOperand()` a member function ... so that it can call `objByOperand()`, which is protected. Related: https://github.com/kdudka/predator/pull/102 --- sl/symproc.cc | 26 ++++++++++++++------------ sl/symproc.hh | 7 +++++-- 2 files changed, 19 insertions(+), 14 deletions(-) diff --git a/sl/symproc.cc b/sl/symproc.cc index 30974a3eb..7305d7725 100644 --- a/sl/symproc.cc +++ b/sl/symproc.cc @@ -1473,17 +1473,19 @@ void SymExecCore::execStackRestore() } } -bool lhsFromOperand(FldHandle *pLhs, SymProc &proc, const struct cl_operand &op) +bool SymProc::lhsFromOperand(FldHandle *pLhs, const struct cl_operand &op) { if (seekRefAccessor(op.accessor)) CL_BREAK_IF("lhs not an l-value"); - *pLhs = proc.fldByOperand(op); - if (FLD_DEREF_FAILED == pLhs->fieldId()) - return false; + *pLhs = this->fldByOperand(op); + if (FLD_DEREF_FAILED != pLhs->fieldId()) { + // propagate the field returned by fldByOperand() + CL_BREAK_IF(!pLhs->isValidHandle()); + return true; + } - CL_BREAK_IF(!pLhs->isValidHandle()); - return true; + return false; } void SymExecCore::execStackAlloc( @@ -1492,7 +1494,7 @@ void SymExecCore::execStackAlloc( { // resolve lhs FldHandle lhs; - if (CL_OPERAND_VOID != opLhs.code && !lhsFromOperand(&lhs, *this, opLhs)) + if (CL_OPERAND_VOID != opLhs.code && !this->lhsFromOperand(&lhs, opLhs)) // error alredy emitted return; @@ -1503,7 +1505,7 @@ void SymExecCore::execStackAlloc( return; } - // now create an annonymous stack object + // now create an anonymous stack object const CallInst callInst(this->bt_); const TObjId obj = sh_.stackAlloc(size, callInst); @@ -1532,8 +1534,8 @@ void SymExecCore::execHeapAlloc( // resolve lhs FldHandle lhs; const struct cl_operand &opLhs = insn.operands[/* dst */ 0]; - if (CL_OPERAND_VOID != opLhs.code && !lhsFromOperand(&lhs, *this, opLhs)) - // error alredy emitted + if (CL_OPERAND_VOID != opLhs.code && !this->lhsFromOperand(&lhs, opLhs)) + // error already emitted return; if (ep_.oomSimulation || /* malloc(0) may return NULL */ !size.hi) { @@ -1650,7 +1652,7 @@ void SymExecCore::execHeapRealloc( // resolve lhs FldHandle lhs; const struct cl_operand &opLhs = insn.operands[/* dst */ 0]; - if (CL_OPERAND_VOID != opLhs.code && !lhsFromOperand(&lhs, *this, opLhs)) + if (CL_OPERAND_VOID != opLhs.code && !this->lhsFromOperand(&lhs, opLhs)) // error alredy emitted return; @@ -2842,7 +2844,7 @@ void SymExecCore::execOp(const CodeStorage::Insn &insn) // resolve lhs FldHandle lhs; const struct cl_operand &dst = insn.operands[/* dst */ 0]; - if (!lhsFromOperand(&lhs, *this, dst)) + if (!this->lhsFromOperand(&lhs, dst)) // error alredy emitted return; diff --git a/sl/symproc.hh b/sl/symproc.hh index 88ae8cdf3..5f1d9946b 100644 --- a/sl/symproc.hh +++ b/sl/symproc.hh @@ -125,10 +125,13 @@ class SymProc { } public: - /// obtain a heap object corresponding to the given operand + /// obtain a field corresponding to the given operand FldHandle fldByOperand(const struct cl_operand &op); - /// obtain a heap value corresponding to the given operand + /// obtain a left-hand-side field corresponding to the given operand + bool lhsFromOperand(FldHandle *pLhs, const struct cl_operand &op); + + /// obtain a SymHeap value corresponding to the given operand TValId valFromOperand(const struct cl_operand &op); /// resolve Fnc uid from the given operand, return true on success From 0bde2d0f42eb37ca1e8c6b32b60e9983d0323b78 Mon Sep 17 00:00:00 2001 From: Kamil Dudka Date: Thu, 10 Oct 2024 13:10:51 +0200 Subject: [PATCH 3/4] symproc: invalidate LHS objects on invalid dereference ... to simulate that invalid operations may by chance write to the target object within the allocated bounds. Nevertheless, the same situation may happen with `executeMemset()`, `executeMemmove()`, etc. With this change and `SE_ERROR_RECOVERY_MODE == 2`, Predator reports one more error in the following example: ``` % nl -ba xxx.c 1 #include 2 3 int main() 4 { 5 int a[10] = {0}; 6 int i = __VERIFIER_nondet_int(); 7 a[i] = 11; 8 a[a[1]] = 1; 9 } % ./slgcc xxx.c Trying to compile xxx.c ... OK Running Predator ... xxx.c:7:10: error: invalid dereference xxx.c:8:13: error: invalid dereference cl/cl_easy.cc:83: note: clEasyRun() took 0.000 s FAILED ``` Related: https://github.com/kdudka/predator/pull/102 --- sl/symproc.cc | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/sl/symproc.cc b/sl/symproc.cc index 7305d7725..84bb49e15 100644 --- a/sl/symproc.cc +++ b/sl/symproc.cc @@ -1485,6 +1485,21 @@ bool SymProc::lhsFromOperand(FldHandle *pLhs, const struct cl_operand &op) return true; } + if (2 <= GlConf::data.errorRecoveryMode) { + // if the dereference failed due to out of range (or unknown) offset, + // try to resolve the allocated object and invalidate its contents in + // order to detect more errors in one run with full error recovery + const TObjId obj = this->objByVar(op); + if (sh_.isValid(obj)) { + const UniformBlock ub = { + /* off */ 0, + /* size */ sh_.objSize(obj).hi, + /* tplValue */ sh_.valCreate(VT_UNKNOWN, VO_UNKNOWN) + }; + sh_.writeUniformBlock(obj, ub); + } + } + return false; } From 8b8964d8a83ea0c564b9590698857c33e94cf534 Mon Sep 17 00:00:00 2001 From: Kamil Dudka Date: Fri, 11 Oct 2024 18:28:09 +0200 Subject: [PATCH 4/4] glconf: introduce the `full_error_recovery` option ... so that one does not need to rebuild Predator from source code to enable full error recovery. Closes: https://github.com/kdudka/predator/pull/102 --- sl/glconf.cc | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/sl/glconf.cc b/sl/glconf.cc index 4dce15563..db077f894 100644 --- a/sl/glconf.cc +++ b/sl/glconf.cc @@ -195,6 +195,12 @@ void handleNoErrorRecovery(const string &name, const string &value) data.errorRecoveryMode = /* no_error_recovery */ 0; } +void handleFullErrorRecovery(const string &name, const string &value) +{ + assumeNoValue(name, value); + data.errorRecoveryMode = /* full_error_recovery */ 2; +} + void handleVerifierErrorIsError(const string &name, const string &value) { assumeNoValue(name, value); @@ -244,6 +250,7 @@ ConfigStringParser::ConfigStringParser() tbl_["error_label"] = handleErrorLabel; tbl_["exit_leaks"] = handleExitLeaks; tbl_["forbid_heap_replace"] = handleForbidHeapReplace; + tbl_["full_error_recovery"] = handleFullErrorRecovery; tbl_["int_arithmetic_limit"] = handleIntArithmeticLimit; tbl_["join_on_loop_edges_only"] = handleJoinOnLoopEdgesOnly; tbl_["memleak_is_error"] = handleMemLeakIsError;