[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.

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))))))))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;