diff options
author | Andres Notzli <andres.noetzli@gmail.com> | 2017-03-26 23:39:07 +0200 |
---|---|---|
committer | Andres Notzli <andres.noetzli@gmail.com> | 2017-04-05 07:45:40 -0700 |
commit | 90076eaba27567f7641751a65f0f784ffca317c4 (patch) | |
tree | 7beda4cc71f18d12d402682605d3f715f260321c /proofs | |
parent | c77213eaf165746a3704204ce56915b86c5f2a7a (diff) |
[LFSC] Fix segfault
LFSC did not detect when the number of arguments provided to a side
condition did not match the expected number of arguments, which could
lead to out-of-bounds reads and writes. This commit adds a check and
fixes one of the proof rules that provided the wrong number of
arguments.
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/lfsc_checker/code.cpp | 19 | ||||
-rw-r--r-- | proofs/signatures/th_bv_bitblast.plf | 2 |
2 files changed, 20 insertions, 1 deletions
diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp index ee143a710..48ebc5578 100644 --- a/proofs/lfsc_checker/code.cpp +++ b/proofs/lfsc_checker/code.cpp @@ -1303,7 +1303,9 @@ Expr *run_code(Expr *_e) { return tmp; } + assert(hd->getclass() == CEXPR); CExpr *prog = (CExpr *)hd; + assert(prog->kids[1]->getclass() == CEXPR); Expr **cur = ((CExpr *)prog->kids[1])->kids; vector<Expr *> old_vals; SymExpr *var; @@ -1331,10 +1333,26 @@ Expr *run_code(Expr *_e) { else { while((var = (SymExpr *)*cur++)) { + // Check whether not enough arguments were supplied + if (i >= args.size()) { + for (size_t i = 0; i < args.size(); i++) { + args[i]->dec(); + } + return NULL; + } + old_vals.push_back(var->val); var->val = args[i++]; } + // Check whether too many arguments were supplied + if (i < args.size()) { + for (size_t i = 0; i < args.size(); i++) { + args[i]->dec(); + } + return NULL; + } + if (dbg_prog) { dbg_prog_indent(cout); cout << "["; @@ -1359,6 +1377,7 @@ Expr *run_code(Expr *_e) { cur = ((CExpr *)prog->kids[1])->kids; i = 0; while((var = (SymExpr *)*cur++)) { + assert(i < args.size()); args[i]->dec(); var->val = old_vals[i++]; } diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf index 2b2fe0868..109155a21 100644 --- a/proofs/signatures/th_bv_bitblast.plf +++ b/proofs/signatures/th_bv_bitblast.plf @@ -173,7 +173,7 @@ (! xb bblt (! rb bblt (! xbb (bblast_term m x xb) - (! c ( ^ (bblast_sextend xb k m) rb) + (! c ( ^ (bblast_sextend xb k) rb) (bblast_term n (sign_extend n k m x) rb)))))))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |