Skip to content

Commit

Permalink
symproc: invalidate LHS objects on invalid dereference
Browse files Browse the repository at this point in the history
... 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 <verifier-builtins.h>
     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: #102
  • Loading branch information
kdudka committed Oct 11, 2024
1 parent 7e6ada7 commit ed1a79d
Showing 1 changed file with 15 additions and 0 deletions.
15 changes: 15 additions & 0 deletions sl/symproc.cc
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down

0 comments on commit ed1a79d

Please sign in to comment.