Extend state representation to track errno across control-flow
#1284
Conversation
An attempt to handle `errno` in order to prevent Alive2 from treating store-to-load forwarding as valid refinements, if may alias `errno`. This is achieved by adding a new SMT expression to model `errno` meant to be used on malloc failure. Also treat malloc et alia as may write errno via LLVM `errnomem` location kind while translating from LLVM IR.
|
|
||
| // Create a new symbolic variable that represents errno if the allocation | ||
| // fails. | ||
| if (blockKind == MALLOC || blockKind == CXX_NEW) { |
There was a problem hiding this comment.
We don’t seem to model realloc as of now, correct?
| expr errno_on_failure = expr::mkFreshVar("#malloc_errno", | ||
| expr::mkUInt(0, 32)); |
There was a problem hiding this comment.
I’m experiencing the following false positive for test attrs/allocsize.srctgt.ll:
declare ptr @my_malloc(i32) allocsize(0)
define ptr @src() {
#0:
%p = call ptr @my_malloc(i32 23) allocsize(0)
ret ptr %p
}
=>
declare ptr @my_malloc(i32) allocsize(0)
define ptr @tgt() {
#0:
%p = call ptr @my_malloc(i32 23) dereferenceable_or_null(23) allocsize(0)
ret ptr %p
}
src_state.getReturnErrno():
(ite (or malloc_never_fails |#alloc_nondet_nonnull!3|)
errno_init
|#malloc_errno!4|)
tgt_state.getReturnErrno():
(ite (or malloc_never_fails |#alloc_nondet_nonnull!6|)
errno_init
|#malloc_errno!7|)
Transformation doesn't verify!
ERROR: Mismatch in errno at return
Possibly we shouldn’t use fresh unique symbolic variables for malloc_errno: I tried switching from using mkFreshVar w/ addNonDetVar to using the dedicated helper getFreshNondetVar instead. This fixes this issue but in doing so we don’t ; ERROR: Mismatch in errno at return anymore for the two new added tests (so we allow the refinement as valid). Any idea on what I'm missing?
|
this is super cool, I never thought about errno being something special we'd need to handle! |
|
|
||
| declare noalias ptr @malloc(i64) memory(inaccessiblemem: readwrite, errnomem: write) | ||
|
|
||
| ; ERROR: Mismatch in errno at return |
There was a problem hiding this comment.
We generally consider allocation functions to only be called non-deterministically I think -- see llvm/llvm-project#177592.
| } | ||
|
|
||
| expr errno_on_write = expr::mkFreshVar((name + "#errno").c_str(), | ||
| expr::mkUInt(0, 32)); |
There was a problem hiding this comment.
instead of mkUInt, you can use errno_val.
I would also move this call inside mkIf_fold to avoid creating the expression altogether
| std::variant<smt::DisjointExpr<StateValue>, StateValue> return_val; | ||
| std::variant<smt::DisjointExpr<Memory>, Memory> return_memory; | ||
| std::set<smt::expr> return_undef_vars; | ||
| smt::expr return_errno; |
There was a problem hiding this comment.
you can use the std::variant trick above to keep a DisjointExpr during state execution. This can shrink final expr size.
What makes errno special here? |
4 participants
An attempt to handle
errnoin order to prevent Alive2 from treating store-to-load forwarding as valid refinements, if may aliaserrno. This is achieved by adding a new SMT expression to modelerrnomeant to be used on malloc failure. Also treat malloc et alia as may write errno via LLVMerrnomemlocation kind while translating from LLVM IR.A thank to Nuno for direction on this!