Merge branch 'master' into fix-newtype-translation

.github/workflows/ci.yml

@@ -197,6 +197,40 @@ jobs:
           name: "saw-${{ runner.os }}-${{ matrix.ghc }}"
           path: "dist/bin/saw"
 
+  mr-solver-tests:
+    needs: [build]
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, macos-10.15]
+    runs-on: ${{ matrix.os }}
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: true
+
+      - shell: bash
+        run: .github/ci.sh install_system_deps
+        env:
+          BUILD_TARGET_OS: ${{ matrix.os }}
+
+      - uses: actions/download-artifact@v2
+        with:
+          name: "${{ runner.os }}-bins"
+          path: dist/bin
+
+      - name: Update PATH to include SAW
+        shell: bash
+        run: |
+          chmod +x dist/bin/*
+          echo $GITHUB_WORKSPACE/dist/bin >> $GITHUB_PATH
+
+      - working-directory: examples/mr_solver
+        shell: bash
+        run: |
+          saw monadify.saw
+          saw mr_solver_unit_tests.saw
+
   heapster-tests:
     needs: [build]
     strategy:
@@ -464,7 +498,7 @@ jobs:
 
   s2n-tests:
     name: "Test s2n proofs"
-    timeout-minutes: 60
+    timeout-minutes: 120
     needs: build
     runs-on: ubuntu-18.04
     strategy:

CHANGES.md

@@ -33,6 +33,20 @@
   dealing with C `union` types, as the type information provided by
   LLVM is imprecise in these cases.
 
+* A new `llvm_union` function has been added that uses debug
+  information to allow users to select fields from `union` types by
+  name. This automates the process of manually applying
+  `llvm_cast_pointer` with the type of the selected union field. Just
+  as with `llvm_field`, debug symbols are required for `llvm_union` to
+  work correctly.
+
+* A new highly experimental `llvm_verify_fixpoint_x86` function that
+  allows partial correctness verification of loops using loop
+  invariants instead of full symbolic unrolling. Only certain very simple
+  styles of loops can currently be accommodated, and the user is
+  required to provide a term that describes how the live variables in
+  the loop evolve over an iteration.
+
 # Version 0.9
 
 ## New Features

README.md

@@ -148,7 +148,7 @@ unix-time
 
 Much of the work on SAW has been funded by, and lots of design input was
 provided by the team at the [NSA's Laboratory for Advanced Cybersecurity
-Research](https://www.nsa.gov/what-we-do/research/cybersecurity-research/),
+Research](https://www.nsa.gov/Research/NSA-Mission-Oriented-Research/LAC/),
 including Brad Martin, Frank Taylor, and Sean Weaver.
 
 Portions of SAW are also based upon work supported by the Office

crux-mir-comp/src/Mir/Compositional/Builder.hs

@@ -613,6 +613,7 @@ substMethodSpec sc sm ms = do
         MS.SetupElem b sv idx -> MS.SetupElem b <$> goSetupValue sv <*> pure idx
         MS.SetupField b sv name -> MS.SetupField b <$> goSetupValue sv <*> pure name
         MS.SetupCast v _ _ -> case v of {}
+        MS.SetupUnion v _ _ -> case v of {}
         MS.SetupGlobal _ _ -> return sv
         MS.SetupGlobalInitializer _ _ -> return sv
 

crux-mir-comp/src/Mir/Compositional/MethodSpec.hs

@@ -30,6 +30,7 @@ type instance MS.HasSetupArray MIR = 'True
 type instance MS.HasSetupElem MIR = 'True
 type instance MS.HasSetupField MIR = 'True
 type instance MS.HasSetupCast MIR = 'False
+type instance MS.HasSetupUnion MIR = 'False
 type instance MS.HasSetupGlobalInitializer MIR = 'False
 
 type instance MS.HasGhostState MIR = 'False

cryptol-saw-core/saw/Cryptol.sawcore

@@ -232,6 +232,9 @@ ecRatio x y = ();
 eqRational : Rational -> Rational -> Bool;
 eqRational x y = error Bool "Unimplemented: (==) Rational";
 
+leRational : Rational -> Rational -> Bool;
+leRational x y = error Bool "Unimplemented: (<=) Rational";
+
 ltRational : Rational -> Rational -> Bool;
 ltRational x y = error Bool "Unimplemented: (<) Rational";
 
@@ -455,6 +458,9 @@ errorBinary s a _ _ = error a s;
 boolCmp : Bool -> Bool -> Bool -> Bool;
 boolCmp x y k = ite Bool x (and y k) (or y k);
 
+boolLt : Bool -> Bool -> Bool;
+boolLt x y = and (not x) y;
+
 integerCmp : Integer -> Integer -> Bool -> Bool;
 integerCmp x y k = or (intLt x y) (and (intEq x y) k);
 
@@ -473,14 +479,35 @@ vecCmp n a f xs ys k =
   foldr (Bool -> Bool) Bool n (\ (f : Bool -> Bool) -> f) k
     (zipWith a a (Bool -> Bool) f n xs ys);
 
+vecLt :
+  (n : Nat) -> (a : isort 0) ->
+  (a -> a -> Bool -> Bool) ->
+  (a -> a -> Bool) ->
+  (Vec n a -> Vec n a -> Bool);
+vecLt n a f g xs ys =
+  foldr (Bool -> Bool) Bool n (\ (f : Bool -> Bool) -> f) False
+    (zipWith a a (Bool -> Bool) f n xs ys);
+
 unitCmp : #() -> #() -> Bool -> Bool;
-unitCmp _ _ _ = False;
+unitCmp _ _ k = k;
+
+unitLe : #() -> #() -> Bool;
+unitLe _ _ = True;
+
+unitLt : #() -> #() -> Bool;
+unitLt _ _ = False;
 
 pairCmp : (a b : sort 0) -> (a -> a -> Bool -> Bool) -> (b -> b -> Bool -> Bool)
         -> a * b -> a * b -> Bool -> Bool;
 pairCmp a b f g x12 y12 k =
   f (fst a b x12) (fst a b y12) (g (snd a b x12) (snd a b y12) k);
 
+pairLt :
+  (a b : sort 0) -> (a -> a -> Bool -> Bool) -> (b -> b -> Bool) ->
+  a * b -> a * b -> Bool;
+pairLt a b f g x y =
+  f (fst a b x) (fst a b y) (g (snd a b x) (snd a b y));
+
 --------------------------------------------------------------------------------
 -- Dictionaries and overloading
 
@@ -534,23 +561,31 @@ PEqPair a b pa pb = { eq = pairEq a b pa.eq pb.eq };
 
 -- Cmp class
 
+-- `cmp x y k` computes `if k then x <= y else x < y`
 PCmp : sort 0 -> sort 1;
 PCmp a =
   #{ cmpEq : PEq a
    , cmp : a -> a -> Bool -> Bool
+   , le : a -> a -> Bool
+   , lt : a -> a -> Bool
    };
 
 PCmpBit : PCmp Bool;
-PCmpBit = { cmpEq = PEqBit, cmp = boolCmp };
+PCmpBit = { cmpEq = PEqBit, cmp = boolCmp, le = implies, lt = boolLt };
 
 PCmpInteger : PCmp Integer;
-PCmpInteger = { cmpEq = PEqInteger, cmp = integerCmp };
+PCmpInteger = { cmpEq = PEqInteger, cmp = integerCmp, le = intLe, lt = intLt };
 
 PCmpRational : PCmp Rational;
-PCmpRational = { cmpEq = PEqRational, cmp = rationalCmp };
+PCmpRational = { cmpEq = PEqRational, cmp = rationalCmp, le = leRational, lt = ltRational };
 
 PCmpVec : (n : Nat) -> (a : isort 0) -> PCmp a -> PCmp (Vec n a);
-PCmpVec n a pa = { cmpEq = PEqVec n a pa.cmpEq, cmp = vecCmp n a pa.cmp };
+PCmpVec n a pa =
+  { cmpEq = PEqVec n a pa.cmpEq
+  , cmp = vecCmp n a pa.cmp
+  , le = \ (x : Vec n a) -> \ (y : Vec n a) -> vecCmp n a pa.cmp x y True
+  , lt = \ (x : Vec n a) -> \ (y : Vec n a) -> vecCmp n a pa.cmp x y False
+  };
 
 PCmpSeq : (n : Num) -> (a : isort 0) -> PCmp a -> PCmp (seq n a);
 PCmpSeq n =
@@ -560,7 +595,7 @@ PCmpSeq n =
           n;
 
 PCmpWord : (n : Nat) -> PCmp (Vec n Bool);
-PCmpWord n = { cmpEq = PEqWord n, cmp = bvCmp n };
+PCmpWord n = { cmpEq = PEqWord n, cmp = bvCmp n, le = bvule n, lt = bvult n };
 
 PCmpSeqBool : (n : Num) -> PCmp (seq n Bool);
 PCmpSeqBool n =
@@ -570,26 +605,33 @@ PCmpSeqBool n =
           n;
 
 PCmpUnit : PCmp #();
-PCmpUnit = { cmpEq = PEqUnit, cmp = unitCmp };
+PCmpUnit = { cmpEq = PEqUnit, cmp = unitCmp, le = unitLe, lt = unitLt };
 
 PCmpPair : (a b : sort 0) -> PCmp a -> PCmp b -> PCmp (a * b);
 PCmpPair a b pa pb =
   { cmpEq  = PEqPair a b pa.cmpEq pb.cmpEq
   , cmp = pairCmp a b pa.cmp pb.cmp
+  , le = pairLt a b pa.cmp pb.le
+  , lt = pairLt a b pa.cmp pb.lt
   };
 
 -- SignedCmp class
 
+-- `scmp x y k` computes `if k then sle x y else slt x y`
 PSignedCmp : sort 0 -> sort 1;
 PSignedCmp a =
    #{ signedCmpEq : PEq a
     , scmp : a -> a -> Bool -> Bool
+    , sle : a -> a -> Bool
+    , slt : a -> a -> Bool
     };
 
 PSignedCmpVec : (n : Nat) -> (a : isort 0) -> PSignedCmp a -> PSignedCmp (Vec n a);
 PSignedCmpVec n a pa =
    { signedCmpEq = PEqVec n a pa.signedCmpEq
    , scmp = vecCmp n a pa.scmp
+   , sle = \ (x : Vec n a) -> \ (y : Vec n a) -> vecCmp n a pa.scmp x y True
+   , slt = \ (x : Vec n a) -> \ (y : Vec n a) -> vecCmp n a pa.scmp x y False
    };
 
 PSignedCmpSeq : (n : Num) -> (a : isort 0) -> PSignedCmp a -> PSignedCmp (seq n a);
@@ -600,7 +642,7 @@ PSignedCmpSeq n =
           n;
 
 PSignedCmpWord : (n : Nat) -> PSignedCmp (Vec n Bool);
-PSignedCmpWord n = { signedCmpEq = PEqWord n, scmp = bvSCmp n };
+PSignedCmpWord n = { signedCmpEq = PEqWord n, scmp = bvSCmp n, sle = bvsle n, slt = bvslt n };
 
 PSignedCmpSeqBool : (n : Num) -> PSignedCmp (seq n Bool);
 PSignedCmpSeqBool n =
@@ -610,12 +652,14 @@ PSignedCmpSeqBool n =
           n;
 
 PSignedCmpUnit : PSignedCmp #();
-PSignedCmpUnit = { signedCmpEq = PEqUnit, scmp = unitCmp };
+PSignedCmpUnit = { signedCmpEq = PEqUnit, scmp = unitCmp, sle = unitLe, slt = unitLt };
 
 PSignedCmpPair : (a b : sort 0) -> PSignedCmp a -> PSignedCmp b -> PSignedCmp (a * b);
 PSignedCmpPair a b pa pb =
   { signedCmpEq = PEqPair a b pa.signedCmpEq pb.signedCmpEq
   , scmp = pairCmp a b pa.scmp pb.scmp
+  , sle = pairLt a b pa.scmp pb.sle
+  , slt = pairLt a b pa.scmp pb.slt
   };
 
 
@@ -1110,20 +1154,20 @@ ecNotEq a pa x y = not (ecEq a pa x y);
 
 -- Cmp
 ecLt : (a : sort 0) -> PCmp a -> a -> a -> Bool;
-ecLt a pa x y = pa.cmp x y False;
+ecLt a pa = pa.lt;
 
 ecGt : (a : sort 0) -> PCmp a -> a -> a -> Bool;
 ecGt a pa x y = ecLt a pa y x;
 
 ecLtEq  : (a : sort 0) -> PCmp a -> a -> a -> Bool;
-ecLtEq a pa x y = not (ecLt a pa y x);
+ecLtEq a pa = pa.le;
 
 ecGtEq  : (a : sort 0) -> PCmp a -> a -> a -> Bool;
-ecGtEq a pa x y = not (ecLt a pa x y);
+ecGtEq a pa x y = ecLtEq a pa y x;
 
 -- SignedCmp
 ecSLt : (a : sort 0) -> PSignedCmp a -> a -> a -> Bool;
-ecSLt a pa x y = pa.scmp x y False;
+ecSLt a pa = pa.slt;
 
 -- Logic
 ecAnd : (a : sort 0) -> PLogic a -> a -> a -> a;
@@ -1592,6 +1636,8 @@ PCmpFloat : (e p : Num) -> PCmp (TCFloat e p);
 PCmpFloat e p =
   { cmpEq = PEqFloat e p
   , cmp = \(x y : TCFloat e p) (k : Bool) -> error Bool "Unimplemented: Cmp Float"
+  , le = \(x y : TCFloat e p) -> error Bool "Unimplemented: Cmp Float"
+  , lt = \(x y : TCFloat e p) -> error Bool "Unimplemented: Cmp Float"
   };
 
 PZeroFloat : (e p : Num) -> PZero (TCFloat e p);

cryptol-saw-core/saw/CryptolM.sawcore

@@ -24,12 +24,20 @@ numAssertEqM n m =
 isFinite : Num -> Prop;
 isFinite = Num_rec (\ (_:Num) -> Prop) (\ (_:Nat) -> TrueProp) FalseProp;
 
+-- Check whether a Num is finite
+checkFinite : (n:Num) -> Maybe (isFinite n);
+checkFinite =
+  Num_rec (\ (n:Num) -> Maybe (isFinite n))
+          (\ (n:Nat) -> Just (isFinite (TCNum n)) (Refl Bool True))
+          (Nothing (isFinite TCInf));
+
 -- Assert that a Num is finite, or fail
 assertFiniteM : (n:Num) -> CompM (isFinite n);
-assertFiniteM =
-  Num_rec (\ (n:Num) -> CompM (isFinite n))
-          (\ (_:Nat) -> returnM TrueProp TrueI)
-          (errorM FalseProp "assertFiniteM: Num not finite");
+assertFiniteM n =
+  maybe (isFinite n) (CompM (isFinite n))
+        (errorM (isFinite n) "assertFiniteM: Num not finite")
+        (returnM (isFinite n))
+        (checkFinite n);
 
 -- Recurse over a Num known to be finite
 Num_rec_fin : (p: Num -> sort 1) -> ((n:Nat) -> p (TCNum n)) ->

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -83,10 +83,13 @@ data Env = Env
   , envC :: Map C.Name C.Schema    -- ^ Cryptol type environment
   , envS :: [Term]                 -- ^ SAW-Core bound variable environment (for type checking)
   , envRefPrims :: Map C.PrimIdent C.Expr
+  , envPrims :: Map C.PrimIdent Term -- ^ Translations for other primitives
+  , envPrimTypes :: Map C.PrimIdent Term -- ^ Translations for primitive types
   }
 
 emptyEnv :: Env
-emptyEnv = Env Map.empty Map.empty Map.empty Map.empty [] Map.empty
+emptyEnv =
+  Env Map.empty Map.empty Map.empty Map.empty [] Map.empty Map.empty Map.empty
 
 liftTerm :: (Term, Int) -> (Term, Int)
 liftTerm (t, j) = (t, j + 1)
@@ -103,6 +106,8 @@ liftEnv env =
       , envC = envC env
       , envS = envS env
       , envRefPrims = envRefPrims env
+      , envPrims = envPrims env
+      , envPrimTypes = envPrimTypes env
       }
 
 bindTParam :: SharedContext -> C.TParam -> Env -> IO Env
@@ -263,7 +268,11 @@ importType sc env ty =
                                b <- go (tyargs !! 1)
                                scFun sc a b
             C.TCTuple _n -> scTupleType sc =<< traverse go tyargs
-            C.TCAbstract{} -> panic "importType TODO: abstract type" []
+            C.TCAbstract (C.UserTC n _)
+              | Just prim <- C.asPrim n
+              , Just t <- Map.lookup prim (envPrimTypes env) ->
+                scApplyAllBeta sc t =<< traverse go tyargs
+              | True -> panic ("importType: unknown primitive type: " ++ show n) []
         C.PC pc ->
           case pc of
             C.PLiteral -> -- we omit first argument to class Literal
@@ -669,6 +678,9 @@ importPrimitive sc primOpts env n sch
          nmi <- importName n
          scConstant' sc nmi e t
 
+  -- lookup primitive in the extra primitive lookup table
+  | Just nm <- C.asPrim n, Just t <- Map.lookup nm (envPrims env) = return t
+
   -- Optionally, create an opaque constant representing the primitive
   -- if it doesn't match one of the ones we know about.
   | Just _ <- C.asPrim n, allowUnknownPrimitives primOpts =