Merge branch 'master' into heapster/no_errors_mbox_randomize

heapster-saw/examples/arrays.c

@@ -91,3 +91,14 @@ uint64_t sum_2d (int64_t **arr, uint64_t l1, uint64_t l2) {
   }
   return sum;
 }
+
+/* Finds the sum of the elements of an array by incrementing the given pointer
+   instead of using a for loop over an index */
+uint64_t sum_inc_ptr(const uint8_t *arr, size_t len) {
+  uint64_t sum = 0;
+  while (len--) {
+    sum += arr[0];
+    arr += 1;
+  }
+  return sum;
+}

heapster-saw/examples/arrays.saw

@@ -47,4 +47,8 @@ heapster_typecheck_fun env "sum_2d"
                       \ arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> int64<>])]), \
                       \ arg1:true, arg2:true, ret:int64<>";
 
+heapster_typecheck_fun env "sum_inc_ptr"
+  "(len:bv 64). arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:eq(llvmword(len)) -o \
+              \ arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:true, ret:int64<>";
+
 heapster_export_coq env "arrays_gen.v";

heapster-saw/examples/arrays_proofs.v

@@ -137,3 +137,74 @@ Admitted.
 (*   * apply isBvslt_to_isBvsle_suc; assumption. *)
 (*   * apply isBvult_to_isBvslt_pos; assumption. *)
 (* Qed. *)
+
+
+Definition sum_inc_ptr_invar (len0 idx len : bitvector 64) :=
+  isBvule 64 idx len0 /\ len = bvSub 64 len0 idx.
+
+Lemma no_errors_sum_inc_ptr : refinesFun sum_inc_ptr (fun len arr => noErrorsSpec).
+Proof.
+  unfold sum_inc_ptr, sum_inc_ptr__tuple_fun.
+  prove_refinement_match_letRecM_l.
+  - exact (fun len0 idx len sum arr _ _ _ => assumingM (sum_inc_ptr_invar len0 idx len) noErrorsSpec).
+  unfold noErrorsSpec, sum_inc_ptr_invar.
+  time "no_errors_sum_inc_ptr" prove_refinement.
+  all: try assumption.
+  - assert (isBvult 64 a2 a1).
+    + apply isBvule_to_isBvult_or_eq in e_assuming.
+      destruct e_assuming; [assumption |].
+      apply bvEq_bvSub_r in H.
+      symmetry in H; contradiction.
+    + rewrite H in e_maybe; discriminate e_maybe.
+  - apply isBvult_to_isBvule_suc; assumption.
+  - repeat rewrite bvSub_eq_bvAdd_neg.
+    rewrite bvAdd_assoc; f_equal.
+    rewrite bvNeg_bvAdd_distrib; reflexivity.
+  - apply isBvule_zero_n.
+  - symmetry; apply bvSub_n_zero.
+Qed.
+
+
+Definition sum_inc_ptr_spec len : BVVec 64 len (bitvector 8) -> bitvector 64 :=
+  foldr _ _ _ (fun a b => bvAdd 64 b (bvUExt 56 8 a)) (intToBv 64 0).
+
+Definition sum_inc_ptr_letRec_spec len0 idx len (sum : bitvector 64) arr (_ _ _ : unit) :=
+  forallM (fun (pf : isBvule 64 idx len0) =>
+  assumingM (len = bvSub 64 len0 idx)
+            (returnM (arr, bvAdd 64 sum (sum_inc_ptr_spec (bvSub 64 len0 idx)
+                                                     (dropBVVec _ _ _ idx pf arr))))).
+
+Lemma sum_inc_ptr_spec_ref :
+  refinesFun sum_inc_ptr (fun len arr => returnM (arr, sum_inc_ptr_spec len arr)).
+Proof.
+  unfold sum_inc_ptr, sum_inc_ptr__tuple_fun.
+  prove_refinement_match_letRecM_l.
+  - exact sum_inc_ptr_letRec_spec.
+  unfold noErrorsSpec, sum_inc_ptr_letRec_spec, sum_inc_ptr_spec.
+  time "sum_inc_ptr_spec_ref" prove_refinement.
+  (* Why didn't prove_refinement do this? *)
+  3: prove_refinement_eauto; [| apply refinesM_returnM ].
+  7: prove_refinement_eauto; [| apply refinesM_returnM ].
+  (* same as no_errors_sum_inc_ptr *)
+  - assert (isBvult 64 a2 a1).
+    + apply isBvule_to_isBvult_or_eq in e_forall.
+      destruct e_forall; [assumption |].
+      apply bvEq_bvSub_r in H.
+      symmetry in H; contradiction.
+    + rewrite H in e_maybe; discriminate e_maybe.
+  - apply isBvult_to_isBvule_suc; assumption.
+  - repeat rewrite bvSub_eq_bvAdd_neg.
+    rewrite bvAdd_assoc; f_equal.
+    rewrite bvNeg_bvAdd_distrib; reflexivity.
+  (* unique to this proof *)
+  - admit.
+  - repeat f_equal.
+    admit.
+  (* same as no_errors_sum_inc_ptr *)
+  - apply isBvule_zero_n.
+  - symmetry; apply bvSub_n_zero.
+  (* unique to this proof *)
+  - rewrite bvAdd_id_l.
+    repeat f_equal.
+    admit.
+Admitted.

heapster-saw/examples/loops_proofs.v

@@ -108,7 +108,7 @@ Lemma compare_sum_spec_ref : refinesFun compare_sum compare_sum_spec.
 Proof.
   unfold compare_sum, compare_sum__tuple_fun, compare_sum_spec.
   time "compare_sum_spec_ref" prove_refinement.
-  all: rewrite bvSub_zero_bvNeg in e_assert.
+  all: rewrite bvSub_zero_n in e_assert.
   (* Note that there are two versions of each case because of the if! *)
   (* The `x < y + z` case: *)
   1,4: continue_prove_refinement_left.

heapster-saw/src/Verifier/SAW/Heapster/Implication.hs

@@ -219,6 +219,12 @@ someEqProof1 x e flag =
   let eq_step = EqProofStep (MNil :>: EqPerm x e flag) (\(_ :>: e') -> e') in
   SomeEqProofCons (SomeEqProofRefl $ eqProofStepLHS eq_step) eq_step
 
+-- | A 'SomeEqProof' for the identity @x = x &+ 0@
+someEqProofZeroOffset :: (1 <= w, KnownNat w) => ExprVar (LLVMPointerType w) ->
+                         SomeEqProof (PermExpr (LLVMPointerType w))
+someEqProofZeroOffset x =
+  someEqProof1 x (PExpr_LLVMOffset x (zeroOfType (BVRepr knownNat))) True
+
 -- | Apply symmetry to a 'SomeEqProof', changing an @e1=e2@ proof to @e2=e1@
 someEqProofSym :: SomeEqProof a -> SomeEqProof a
 someEqProofSym eqp_top =
@@ -419,6 +425,12 @@ data SimplImpl ps_in ps_out where
                       SimplImpl (RNil :> LLVMPointerType w :> BVType w)
                       (RNil :> LLVMPointerType w)
 
+  -- | The implication that @x@ is the same as @x &+ 0@
+  --
+  -- > . -o x:eq(x &+ 0)
+  SImpl_LLVMOffsetZeroEq :: (1 <= w, KnownNat w) => ExprVar (LLVMPointerType w) ->
+                            SimplImpl RNil (RNil :> LLVMPointerType w)
+
   -- | Introduce an empty conjunction on @x@, i.e.:
   --
   -- > . -o x:true
@@ -1570,6 +1582,7 @@ simplImplIn (SImpl_InvTransEq x y e) =
 simplImplIn (SImpl_CopyEq x e) = distPerms1 x (ValPerm_Eq e)
 simplImplIn (SImpl_LLVMWordEq x y e) =
   distPerms2 x (ValPerm_Eq (PExpr_LLVMWord (PExpr_Var y))) y (ValPerm_Eq e)
+simplImplIn (SImpl_LLVMOffsetZeroEq _) = DistPermsNil
 simplImplIn (SImpl_IntroConj _) = DistPermsNil
 simplImplIn (SImpl_ExtractConj x ps _) = distPerms1 x (ValPerm_Conj ps)
 simplImplIn (SImpl_CopyConj x ps _) = distPerms1 x (ValPerm_Conj ps)
@@ -1868,6 +1881,8 @@ simplImplOut (SImpl_InvTransEq x y _) = distPerms1 x (ValPerm_Eq $ PExpr_Var y)
 simplImplOut (SImpl_CopyEq x e) = distPerms2 x (ValPerm_Eq e) x (ValPerm_Eq e)
 simplImplOut (SImpl_LLVMWordEq x _ e) =
   distPerms1 x (ValPerm_Eq (PExpr_LLVMWord e))
+simplImplOut (SImpl_LLVMOffsetZeroEq x) =
+  distPerms1 x (ValPerm_Eq (PExpr_LLVMOffset x (zeroOfType (BVRepr knownNat))))
 simplImplOut (SImpl_IntroConj x) = distPerms1 x ValPerm_True
 simplImplOut (SImpl_ExtractConj x ps i) =
   if i < length ps then
@@ -2356,6 +2371,8 @@ instance SubstVar PermVarSubst m =>
       SImpl_CopyEq <$> genSubst s x <*> genSubst s e
     [nuMP| SImpl_LLVMWordEq x y e |] ->
       SImpl_LLVMWordEq <$> genSubst s x <*> genSubst s y <*> genSubst s e
+    [nuMP| SImpl_LLVMOffsetZeroEq x |] ->
+      SImpl_LLVMOffsetZeroEq <$> genSubst s x
     [nuMP| SImpl_IntroConj x |] ->
       SImpl_IntroConj <$> genSubst s x
     [nuMP| SImpl_ExtractConj x ps i |] ->
@@ -3491,6 +3508,9 @@ implProveEqPerms DistPermsNil = pure ()
 implProveEqPerms (DistPermsCons ps' x (ValPerm_Eq (PExpr_Var y)))
   | x == y
   = implProveEqPerms ps' >>> introEqReflM x
+implProveEqPerms (DistPermsCons ps' x (ValPerm_Eq (PExpr_LLVMOffset y off)))
+  | x == y, bvMatchConstInt off == Just 0
+  = implProveEqPerms ps' >>> implSimplM Proxy (SImpl_LLVMOffsetZeroEq x)
 implProveEqPerms (DistPermsCons ps' x p@(ValPerm_Eq _)) =
   implProveEqPerms ps' >>> implPushCopyM x p
 implProveEqPerms _ = error "implProveEqPerms: non-equality permission"
@@ -4513,7 +4533,8 @@ substEqsWithProof a =
 
 
 -- | The main work horse for 'proveEq' on expressions
-proveEqH :: NuMatchingAny1 r => PartialSubst vars -> PermExpr a ->
+proveEqH :: forall vars a s r ps. NuMatchingAny1 r =>
+            PartialSubst vars -> PermExpr a ->
             Mb vars (PermExpr a) ->
             ImplM vars s r ps ps (SomeEqProof (PermExpr a))
 proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
@@ -4560,6 +4581,20 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
             Just _ -> proveEqH psubst e mb_e
             Nothing -> proveEqFail e mb_e
 
+  -- To prove @x &+ o = e@, we subtract @o@ from the RHS and recurse
+  (PExpr_LLVMOffset x off, _) ->
+    proveEq (PExpr_Var x) (fmap (`addLLVMOffset` bvNegate off) mb_e) >>= \some_eqp ->
+    pure $ fmap (`addLLVMOffset` off) some_eqp
+
+  -- To prove @x = x &+ o@, we prove that @0 = o@ and combine it with the fact
+  -- that @x = x &+ 0@ ('someEqProofZeroOffset') using transitivity
+  (PExpr_Var x, [nuMP| PExpr_LLVMOffset mb_y mb_off |])
+    | Right y <- mbNameBoundP mb_y
+    , x == y ->
+      proveEq (zeroOfType (BVRepr knownNat)) mb_off >>= \some_eqp ->
+      pure $ someEqProofTrans (someEqProofZeroOffset y)
+                              (fmap (PExpr_LLVMOffset y) some_eqp)
+
   -- To prove x=e, try to see if x:eq(e') and proceed by transitivity
   (PExpr_Var x, _) ->
     getVarEqPerm x >>= \case
@@ -4584,13 +4619,15 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
   (PExpr_LLVMWord e', [nuMP| PExpr_LLVMWord mb_e' |]) ->
     fmap PExpr_LLVMWord <$> proveEqH psubst e' mb_e'
 
-  -- Prove e = N*z + M where e - M is a multiple of N by setting z = (e-M)/N
-  (_, [nuMP| PExpr_BV [BVFactor (BV.BV mb_n) z] (BV.BV mb_m) |])
-    | Left memb <- mbNameBoundP z
-    , Nothing <- psubstLookup psubst memb
-    , bvIsZero (bvMod (bvSub e (bvInt $ mbLift mb_m)) (mbLift mb_n)) ->
-      setVarM memb (bvDiv (bvSub e (bvInt $ mbLift mb_m)) (mbLift mb_n)) >>>
-      pure (SomeEqProofRefl e)
+  -- Prove e = L_1*y_1 + ... + L_k*y_k + N*z + M where z is an unset variable,
+  -- each y_i is either a set variable with value e_i or an unbound variable
+  -- with e_i = y_i, and e - (L_1*e_1 + ... + L_k*e_k + M) is divisible by N,
+  -- by setting z = (e - (L_1*e_1 + ... + L_k*e_k + M))/N
+  (_, [nuMP| PExpr_BV mb_factors (BV.BV mb_m) |])
+    | Just (n, memb, e_factors) <- getUnsetBVFactor psubst mb_factors
+    , e' <- bvSub e (bvAdd e_factors (bvInt $ mbLift mb_m))
+    , bvIsZero (bvMod e' n) ->
+      setVarM memb (bvDiv e' n) >>> pure (SomeEqProofRefl e)
 
   -- FIXME: add cases to prove struct(es1)=struct(es2)
 

heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs

@@ -31,6 +31,7 @@ import Prelude hiding (pred)
 
 import Data.Char (isDigit)
 import Data.Maybe
+import Data.Either
 import Data.Foldable (asum)
 import Data.List hiding (sort)
 import Data.List.NonEmpty (NonEmpty(..))
@@ -4823,6 +4824,7 @@ isDeterminingExpr (PExpr_BV [BVFactor _ _] _) =
   -- A linear expression N*x + M lets you solve for x when it is possible
   True
 isDeterminingExpr (PExpr_ValPerm (ValPerm_Eq e)) = isDeterminingExpr e
+isDeterminingExpr (PExpr_LLVMOffset _ off) = isDeterminingExpr off
 isDeterminingExpr e =
   -- If an expression has no free variables then it vacuously determines all of
   -- its free variables
@@ -5569,6 +5571,40 @@ partialSubstForce :: Substable PartialSubst a Maybe => PartialSubst ctx ->
 partialSubstForce s mb msg = fromMaybe (error msg) $ partialSubst s mb
 
 
+----------------------------------------------------------------------
+-- * Additional functions involving partial substitutions
+----------------------------------------------------------------------
+
+-- | If there is exactly one 'BVFactor' in a list of 'BVFactor's which is
+-- an unset variable, return the value of its 'BV', the witness that it
+-- is bound, and the result of adding together the remaining factors
+getUnsetBVFactor :: (1 <= w, KnownNat w) => PartialSubst vars ->
+                    Mb vars [BVFactor w] ->
+                    Maybe (Integer, Member vars (BVType w), PermExpr (BVType w))
+getUnsetBVFactor psubst (mbList -> mb_factors) =
+  case partitionEithers $ mbFactorNameBoundP psubst <$> mb_factors of
+    ([(n, memb)], xs) -> Just (n, memb, foldl' bvAdd (bvInt 0) xs)
+    _ -> Nothing
+
+-- | If a 'BVFactor' in a binding is an unset variable, return the value
+-- of its 'BV' and the witness that it is bound. Otherwise, return the
+-- constant of the factor multiplied by the variable's value if it is
+-- a set variable, or the constant of the factor multiplied by the
+-- variable, if it is an unbound variable
+mbFactorNameBoundP :: PartialSubst vars ->
+                      Mb vars (BVFactor w) ->
+                      Either (Integer, Member vars (BVType w))
+                             (PermExpr (BVType w))
+mbFactorNameBoundP psubst (mbMatch -> [nuMP| BVFactor (BV.BV mb_n) mb_z |]) =
+  let n = mbLift mb_n in
+  case mbNameBoundP mb_z of
+    Left memb -> case psubstLookup psubst memb of 
+                   Nothing -> Left (n, memb)
+                   Just e' -> Right (bvMultBV (BV.mkBV knownNat n) e')
+    Right z -> Right (PExpr_BV [BVFactor (BV.mkBV knownNat n) z]
+                               (BV.zero knownNat))
+
+
 ----------------------------------------------------------------------
 -- * Abstracting Out Variables
 ----------------------------------------------------------------------

heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs

@@ -2302,6 +2302,11 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
     (\(pctx :>: _ :>: _) -> (pctx :>: PTrans_Eq (fmap PExpr_LLVMWord e)))
     m
 
+  [nuMP| SImpl_LLVMOffsetZeroEq x |] ->
+    let bvZero = zeroOfType (BVRepr knownNat) in
+    withPermStackM (:>: translateVar x)
+                   (:>: PTrans_Eq (fmap (flip PExpr_LLVMOffset bvZero) x)) m
+
   [nuMP| SImpl_IntroConj x |] ->
     withPermStackM (:>: translateVar x) (:>: PTrans_True) m
 

heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs

@@ -4079,6 +4079,7 @@ visitEntry names can_widen blk entry =
 
   mapM (traverseF $
         visitCallSite entry) (typedEntryCallers entry) >>= \callers ->
+  debugTrace dlevel ("can_widen: " ++ show can_widen ++ ", any_fails: "  ++ show (any (anyF typedCallSiteImplFails) callers)) $
   if can_widen && any (anyF typedCallSiteImplFails) callers then
     case widenEntry dlevel env entry of
       Some entry' ->

heapster-saw/src/Verifier/SAW/Heapster/Widening.hs

@@ -183,9 +183,10 @@ setVarNamesM :: String -> RAssign ExprVar tps -> WideningM ()
 setVarNamesM base xs = modify $ over wsPPInfo $ ppInfoAddExprNames base xs
 
 traceM :: (PPInfo -> Doc ()) -> WideningM ()
-traceM f =
-  debugTrace <$> (view wsDebugLevel <$> get)
-  <*> (renderDoc <$> f <$> view wsPPInfo <$> get) <*> (return ())
+traceM f = do
+  dlevel <- view wsDebugLevel <$> get
+  str <- renderDoc <$> f <$> view wsPPInfo <$> get
+  debugTrace dlevel str $ return ()
 
 
 ----------------------------------------------------------------------
@@ -273,17 +274,21 @@ widenExpr' tp e1@(asVarOffset -> Just (x1, off1)) e2@(asVarOffset ->
        _ | x1 == x2 && offsetsEq off1 off2 ->
            visitM x1 >> return e1
 
-       -- If we have the same variable but different offsets, then the two sides
-       -- cannot be equal, so we generalize with a new variable
-       _ | x1 == x2 ->
-           do x <- bindFreshVar tp
-              visitM x
-              ((p1',p2'), p') <-
-                doubleSplitWidenPerm tp (offsetPerm off1 p1) (offsetPerm off2 p2)
-              setOffVarPermM x1 off1 p1'
-              setOffVarPermM x2 off2 p2'
-              setVarPermM x p'
-              return $ PExpr_Var x
+       -- If we have the same variable but different offsets, e.g., if we are
+       -- widening x &+ bv1 and x &+ bv2, then bind a fresh variable bv for the
+       -- offset and return x &+ bv. Note that we cannot have the same variable
+       -- x on both sides unless they have been visited, so we can safely
+       -- ignore the isv1 and isv2 flags. The complexity of having these two
+       -- cases is to find the BVType of one of off1 or off2; because the
+       -- previous case did not match, we know at least one is LLVMPermOffset.
+       _ | x1 == x2, LLVMPermOffset (exprType -> off_tp) <- off1 ->
+           do off_var <- bindFreshVar off_tp
+              visitM off_var
+              return $ PExpr_LLVMOffset x1 (PExpr_Var off_var)
+       _ | x1 == x2, LLVMPermOffset (exprType -> off_tp) <- off2 ->
+           do off_var <- bindFreshVar off_tp
+              visitM off_var
+              return $ PExpr_LLVMOffset x1 (PExpr_Var off_var)
 
        -- If a variable has an eq(e) permission, replace it with e and recurse
        (ValPerm_Eq e1', _, _, _) ->

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v

@@ -141,6 +141,9 @@ Instance Proper_isBvslt_isBvsle w : Proper (isBvsle w --> isBvsle w ==> impl) (i
 Definition isBvult_to_isBvule w a b : isBvult w a b -> isBvule w a b. Admitted.
 Instance Proper_isBvult_isBvule w : Proper (isBvule w --> isBvule w ==> impl) (isBvult w). Admitted.
 
+Definition isBvule_to_isBvult_or_eq w a b : isBvule w a b -> isBvult w a b \/ a = b.
+Admitted.
+
 Definition isBvslt_to_isBvsle_suc w a b : isBvslt w a b ->
                                           isBvsle w (bvAdd w a (intToBv w 1)) b.
 Admitted.
@@ -169,6 +172,9 @@ Admitted.
 Definition isBvslt_antirefl w a : ~ isBvslt w a a.
 Admitted.
 
+Definition isBvule_zero_n w a : isBvule w (intToBv w 0) a.
+Admitted.
+
 Definition isBvule_n_zero w a : isBvule w a (intToBv w 0) <-> a = intToBv w 0.
 Admitted.
 
@@ -198,16 +204,22 @@ Admitted.
 
 (** Lemmas about bitvector subtraction, negation, and sign bits **)
 
-Lemma bvSub_zero_bvNeg w a : bvSub w (intToBv w 0) a = bvNeg w a.
+Lemma bvSub_n_zero w a : bvSub w a (intToBv w 0) = a.
 Admitted.
 
-Hint Rewrite bvSub_zero_bvNeg : SAWCoreBitvectors_eqs.
+Lemma bvSub_zero_n w a : bvSub w (intToBv w 0) a = bvNeg w a.
+Admitted.
+
+Hint Rewrite bvSub_zero_n : SAWCoreBitvectors_eqs.
 
 Lemma bvNeg_msb w a : msb w (bvNeg (Succ w) a) = not (msb w a).
 Admitted.
 
 Hint Rewrite bvNeg_msb : SAWCoreBitvectors_eqs.
 
+Lemma bvNeg_bvAdd_distrib w a b : bvNeg w (bvAdd w a b) = bvAdd w (bvNeg w a) (bvNeg w b).
+Admitted.
+
 Lemma bvslt_bvSub_r w a b : isBvslt w a b <-> isBvslt w (intToBv w 0) (bvSub w b a).
 Admitted.