Merge pull request #37 from GaloisInc/sc-vector-reduced

Add vector size and bvAt checks in scVectorReduced

src/Verifier/SAW/Recognizer.hs

@@ -11,6 +11,7 @@ Lightweight calculus for composing patterns as functions.
 
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ViewPatterns #-}
@@ -43,6 +44,8 @@ module Verifier.SAW.Recognizer
   , asRecursorApp
   , isDataType
   , asNat
+  , asBvLit
+  , asUnsignedBvLit
   , asStringLit
   , asLambda
   , asLambdaList
@@ -268,6 +271,20 @@ asNat (asCtor -> Just (c, [])) | c == "Prelude.Zero" = return 0
 asNat (asCtor -> Just (c, [asNat -> Just i])) | c == "Prelude.Succ" = return (i+1)
 asNat _ = fail "not Nat"
 
+asBvLit :: (MonadFail f) => Recognizer f Term (Natural, Natural)
+asBvLit term
+  | Just (ctor, [n_term, v_term]) <- asCtor term
+  , ctor == "Prelude.scBvNat"
+  , Just n <- asNat n_term
+  , Just v <- asNat v_term =
+    return (n, v)
+  | otherwise = fail "not a bitvector literal"
+
+asUnsignedBvLit :: (MonadFail f) => Recognizer f Term Natural
+asUnsignedBvLit term = do
+  (n, v) <- asBvLit term
+  return $ mod v (2 ^ n)
+
 asStringLit :: (MonadFail f) => Recognizer f Term String
 asStringLit t = do StringLit i <- asFTermF t; return i
 

src/Verifier/SAW/SharedTerm.hs

@@ -4,6 +4,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE ParallelListComp #-}
+{-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE RecordWildCards #-}
@@ -145,7 +146,10 @@ module Verifier.SAW.SharedTerm
   , scTypeOfGlobal
     -- ** Prelude operations
   , scAppend
+  , scJoin
+  , scSplit
   , scGet
+  , scAtWithDefault
   , scAt
   , scNot
   , scAnd
@@ -1187,25 +1191,27 @@ scTupleReduced sc (t : ts) = scPairValueReduced sc t =<< scTupleReduced sc ts
 -- | An optimized variant of 'scVector' that will reduce vectors of
 -- the form @[at x 0, at x 1, at x 2, at x 3]@ to just @x@.
 scVectorReduced :: SharedContext -> Term {- ^ element type -} -> [Term] {- ^ elements -} -> IO Term
-scVectorReduced sc ety xs =
-  case traverse asAt xs >>= asRedex of
-    Just x -> return x
-    Nothing -> scVector sc ety xs
+scVectorReduced sc ety xs
+  | (hd : _) <- xs
+  , Just ((arr_sz :*: arr_tm) :*: 0) <- asAtOrBvAt hd
+  , fromIntegral (length xs) == arr_sz
+  , iall (\i x -> asAtOrBvAt x == Just ((arr_sz :*: arr_tm) :*: fromIntegral i)) xs =
+    return arr_tm
+  | otherwise = scVector sc ety xs
   where
     asAny :: Term -> Maybe ()
     asAny _ = Just ()
 
-    asAt :: Term -> Maybe (Term :*: Natural)
-    asAt = isGlobalDef "Prelude.at" @> asAny @> asAny @> return <@> asNat
+    asAt :: Term -> Maybe ((Natural :*: Term) :*: Natural)
+    asAt = ((isGlobalDef "Prelude.at" @> asNat) <@> (asAny @> return)) <@> asNat
 
-    asRedex :: [Term :*: Natural] -> Maybe Term
-    asRedex [] = Nothing
-    asRedex ((t :*: n) : ts) = if n == 0 then check t 0 ts else Nothing
+    asBvAt :: Term -> Maybe ((Natural :*: Term) :*: Natural)
+    asBvAt = ((isGlobalDef "Prelude.bvAt" @> asNat) <@> (asAny @> asAny @> return)) <@> asUnsignedBvLit
 
-    check :: Term -> Natural -> [Term :*: Natural] -> Maybe Term
-    check t _ [] = Just t
-    check t n ((t' :*: n') : ts)
-      | t' == t && n' == n + 1 = check t n' ts
+    asAtOrBvAt :: Term -> Maybe ((Natural :*: Term) :*: Natural)
+    asAtOrBvAt term
+      | res@Just{} <- asAt term = res
+      | res@Just{} <- asBvAt term = res
       | otherwise = Nothing
 
 ------------------------------------------------------------
@@ -1258,6 +1264,14 @@ scAppend :: SharedContext -> Term -> Term -> Term ->
             Term -> Term -> IO Term
 scAppend sc t m n x y = scGlobalApply sc "Prelude.append" [m, n, t, x, y]
 
+-- | join  : (m n : Nat) -> (a : sort 0) -> Vec m (Vec n a) -> Vec (mulNat m n) a;
+scJoin :: SharedContext -> Term -> Term -> Term -> Term -> IO Term
+scJoin sc m n a v = scGlobalApply sc "Prelude.join" [m, n, a, v]
+
+-- | split : (m n : Nat) -> (a : sort 0) -> Vec (mulNat m n) a -> Vec m (Vec n a);
+scSplit :: SharedContext -> Term -> Term -> Term -> Term -> IO Term
+scSplit sc m n a v = scGlobalApply sc "Prelude.split" [m, n, a, v]
+
 -- | slice :: (e :: sort 1) -> (i n o :: Nat) -> Vec (addNat (addNat i n) o) e -> Vec n e;
 scSlice :: SharedContext -> Term -> Term ->
            Term -> Term -> Term -> IO Term
@@ -1273,6 +1287,10 @@ scBvAt :: SharedContext -> Term -> Term ->
          Term -> Term -> Term -> IO Term
 scBvAt sc n a i xs idx = scGlobalApply sc (mkIdent preludeName "bvAt") [n, a, i, xs, idx]
 
+-- | atWithDefault :: (n :: Nat) -> (a :: sort 0) -> a -> Vec n a -> Nat -> a;
+scAtWithDefault :: SharedContext -> Term -> Term -> Term -> Term -> Term -> IO Term
+scAtWithDefault sc n a v xs idx = scGlobalApply sc (mkIdent preludeName "atWithDefault") [n, a, v, xs, idx]
+
 -- | at :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Nat -> a;
 scAt :: SharedContext -> Term -> Term ->
         Term -> Term -> IO Term

src/Verifier/SAW/Simulator/Prims.hs

@@ -526,7 +526,7 @@ ltNatOp bp =
          VBool <$> bpBvult bp x1 x2
 
 -- natCase :: (p :: Nat -> sort 0) -> p Zero -> ((n :: Nat) -> p (Succ n)) -> (n :: Nat) -> p n;
-natCaseOp :: VMonad l => Value l
+natCaseOp :: (VMonad l, Show (Extra l)) => Value l
 natCaseOp =
   constFun $
   VFun $ \z -> return $
@@ -544,7 +544,7 @@ vecTypeOp :: VMonad l => Value l
 vecTypeOp = pureFun $ \n -> pureFun $ \a -> VVecType n a
 
 -- gen :: (n :: Nat) -> (a :: sort 0) -> (Nat -> a) -> Vec n a;
-genOp :: VMonadLazy l => Value l
+genOp :: (VMonadLazy l, Show (Extra l)) => Value l
 genOp =
   natFun' "gen1" $ \n -> return $
   constFun $
@@ -667,7 +667,7 @@ dropOp bp =
     _ -> error $ "dropOp: " ++ show v
 
 -- append :: (m n :: Nat) -> (a :: sort 0) -> Vec m a -> Vec n a -> Vec (addNat m n) a;
-appendOp :: VMonad l => BasePrims l -> Value l
+appendOp :: (VMonad l, Show (Extra l)) => BasePrims l -> Value l
 appendOp bp =
   constFun $
   constFun $
@@ -676,7 +676,7 @@ appendOp bp =
   strictFun $ \ys ->
   appV bp xs ys
 
-appV :: VMonad l => BasePrims l -> Value l -> Value l -> MValue l
+appV :: (VMonad l, Show (Extra l)) => BasePrims l -> Value l -> Value l -> MValue l
 appV bp xs ys =
   case (xs, ys) of
     (VVector xv, _) | V.null xv -> return ys
@@ -685,10 +685,10 @@ appV bp xs ys =
     (VVector xv, VVector yv) -> return $ VVector ((V.++) xv yv)
     (VVector xv, VWord yw) -> liftM (\yv -> VVector ((V.++) xv (fmap (ready . VBool) yv))) (bpUnpack bp yw)
     (VWord xw, VVector yv) -> liftM (\xv -> VVector ((V.++) (fmap (ready . VBool) xv) yv)) (bpUnpack bp xw)
-    _ -> fail "Verifier.SAW.Simulator.Prims.appendOp"
+    _ -> fail $ "Verifier.SAW.Simulator.Prims.appendOp: " ++ show xs ++ ", " ++ show ys
 
 -- join  :: (m n :: Nat) -> (a :: sort 0) -> Vec m (Vec n a) -> Vec (mulNat m n) a;
-joinOp :: VMonad l => BasePrims l -> Value l
+joinOp :: (VMonad l, Show (Extra l)) => BasePrims l -> Value l
 joinOp bp =
   constFun $
   constFun $
@@ -701,7 +701,7 @@ joinOp bp =
     _ -> error "Verifier.SAW.Simulator.Prims.joinOp"
 
 -- split :: (m n :: Nat) -> (a :: sort 0) -> Vec (mulNat m n) a -> Vec m (Vec n a);
-splitOp :: (VMonad l) => BasePrims l -> Value l
+splitOp :: (VMonad l, Show (Extra l)) => BasePrims l -> Value l
 splitOp bp =
   natFun $ \(fromIntegral -> m) -> return $
   natFun $ \(fromIntegral -> n) -> return $
@@ -1179,7 +1179,7 @@ muxValue bp b = value
     thunk x y = delay $ do x' <- force x; y' <- force y; value x' y'
 
 -- fix :: (a :: sort 0) -> (a -> a) -> a;
-fixOp :: (VMonadLazy l, MonadFix (EvalM l)) => Value l
+fixOp :: (VMonadLazy l, MonadFix (EvalM l), Show (Extra l)) => Value l
 fixOp =
   constFun $
   strictFun $ \f ->

src/Verifier/SAW/Simulator/Value.hs

@@ -199,12 +199,12 @@ valRecordProj v@(VRecordValue _) fld =
   "valRecordProj: record field not found: " ++ fld ++ " in value: " ++ show v
 valRecordProj v _ = fail $ "valRecordProj: not a record value: " ++ show v
 
-apply :: VMonad l => Value l -> Thunk l -> MValue l
+apply :: (VMonad l, Show (Extra l)) => Value l -> Thunk l -> MValue l
 apply (VFun f) x = f x
 apply (VPiType _ f) x = f x
-apply _ _ = fail "Not a function value"
+apply v _x = fail $ "Not a function value: " ++ show v
 
-applyAll :: VMonad l => Value l -> [Thunk l] -> MValue l
+applyAll :: (VMonad l, Show (Extra l)) => Value l -> [Thunk l] -> MValue l
 applyAll = foldM apply
 
 asFiniteTypeValue :: Value l -> Maybe FiniteType