Merge pull request #1940 from GaloisInc/ffi-verify

Add `llvm_ffi_setup` command

CHANGES.md

@@ -13,6 +13,10 @@
   information, see the
   [manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#cryptol-and-its-role-in-saw).
 
+* Building on the above feature, SAW now supports automatically
+  generating LLVM setup scripts for Cryptol FFI functions with the
+  `llvm_ffi_setup` command. For more information, see the [manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#verifying-cryptol-ffi-functions).
+
 # Version 1.0 -- 2023-06-26
 
 ## New Features

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

@@ -58,7 +58,10 @@ import System.Environment (lookupEnv)
 import System.Environment.Executable (splitExecutablePath)
 import System.FilePath ((</>), normalise, joinPath, splitPath, splitSearchPath)
 
-import Verifier.SAW.SharedTerm (SharedContext, Term, incVars)
+import Verifier.SAW.Cryptol.Panic
+import Verifier.SAW.Name (ecName)
+import Verifier.SAW.Recognizer (asConstant)
+import Verifier.SAW.SharedTerm (NameInfo, SharedContext, Term, incVars)
 
 import qualified Verifier.SAW.Cryptol as C
 
@@ -68,6 +71,7 @@ import qualified Cryptol.Parser.AST as P
 import qualified Cryptol.Parser.Position as P
 import qualified Cryptol.TypeCheck as T
 import qualified Cryptol.TypeCheck.AST as T
+import qualified Cryptol.TypeCheck.FFI.FFIType as T
 import qualified Cryptol.TypeCheck.Error as TE
 import qualified Cryptol.TypeCheck.Infer as TI
 import qualified Cryptol.TypeCheck.Kind as TK
@@ -131,6 +135,8 @@ data CryptolEnv = CryptolEnv
   , eTermEnv    :: Map T.Name Term      -- ^ SAWCore terms for *all* names in scope
   , ePrims      :: Map C.PrimIdent Term -- ^ SAWCore terms for primitives
   , ePrimTypes  :: Map C.PrimIdent Term -- ^ SAWCore terms for primitive type names
+  , eFFITypes   :: Map NameInfo T.FFIFunType
+    -- ^ FFI info for SAWCore names of Cryptol foreign functions
   }
 
 
@@ -230,6 +236,7 @@ initCryptolEnv sc = do
     , eTermEnv    = termEnv
     , ePrims      = Map.empty
     , ePrimTypes  = Map.empty
+    , eFFITypes   = Map.empty
     }
 
 -- Parse -----------------------------------------------------------------------
@@ -424,17 +431,33 @@ loadCryptolModule sc primOpts env path = do
                 types
                 newTermEnv
 
-  let env' = env { eModuleEnv = modEnv''
-                 , eTermEnv = newTermEnv
-                 }
+  let env' = updateFFITypes m
+               env { eModuleEnv = modEnv''
+                   , eTermEnv = newTermEnv
+                   }
 
   let sm' = Map.filterWithKey
               (\k _ -> Set.member k (MEx.exported C.NSType (T.mExports m)))
               (T.mTySyns m)
 
   return (CryptolModule sm' tm', env')
 
-
+updateFFITypes :: T.Module -> CryptolEnv -> CryptolEnv
+updateFFITypes m env = env { eFFITypes = eFFITypes' }
+  where
+  eFFITypes' = foldr
+    (\(nm, ty) -> Map.insert (getNameInfo nm) ty)
+    (eFFITypes env)
+    (T.findForeignDecls m)
+  getNameInfo nm =
+    case Map.lookup nm (eTermEnv env) of
+      Just tm ->
+        case asConstant tm of
+          Just (ec, _) -> ecName ec
+          Nothing -> panic "updateFFITypes"
+            ["SAWCore term of Cryptol name is not Constant", show nm, show tm]
+      Nothing -> panic "updateFFITypes"
+        ["Cannot find foreign function in term env", show nm]
 
 bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv
 bindCryptolModule (modName, CryptolModule sm tm) env =
@@ -503,12 +526,13 @@ importModule sc env src as vis imps = do
                                                             cEnv newDeclGroups
        traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv)
 
-  return
-    env { eImports   = (vis, P.Import (T.mName m) as imps Nothing)
-                     : eImports env
-        , eModuleEnv = modEnv'
-        , eTermEnv   = newTermEnv
-        }
+  return $
+    updateFFITypes m
+      env { eImports   = (vis, P.Import (T.mName m) as imps Nothing)
+                       : eImports env
+          , eModuleEnv = modEnv'
+          , eTermEnv   = newTermEnv
+          }
 
 bindIdent :: Ident -> CryptolEnv -> (T.Name, CryptolEnv)
 bindIdent ident env = (name, env')

doc/manual/manual.md

@@ -3337,6 +3337,89 @@ let main : TopLevel () = do {
 
 [^4]: https://en.wikipedia.org/wiki/Salsa20
 
+## Verifying Cryptol FFI functions
+
+SAW has special support for verifying the correctness of Cryptol's
+[`foreign`
+functions](https://galoisinc.github.io/cryptol/master/FFI.html),
+implemented in a language such as C which compiles to LLVM, provided
+that there exists a [reference Cryptol
+implementation](https://galoisinc.github.io/cryptol/master/FFI.html#cryptol-implementation-of-foreign-functions)
+of the function as well. Since the way in which `foreign` functions are
+called is precisely specified by the Cryptol FFI, SAW is able to
+generate a `LLVMSetup ()` spec directly from the type of a Cryptol
+`foreign` function. This is done with the `llvm_ffi_setup` command,
+which is experimental and requires `enable_experimental;` to be run
+beforehand.
+```
+llvm_ffi_setup : Term -> LLVMSetup ()
+```
+
+For instance, for the simple imported Cryptol foreign function `foreign
+add : [32] -> [32] -> [32]` we can obtain a `LLVMSetup` spec simply by
+writing
+```
+let add_setup = llvm_ffi_setup {{ add }};
+```
+which behind the scenes expands to something like
+```
+let add_setup = do {
+  in0 <- llvm_fresh_var "in0" (llvm_int 32);
+  in1 <- llvm_fresh_var "in1" (llvm_int 32);
+  llvm_execute_func [llvm_term in0, llvm_term in1];
+  llvm_return (llvm_term {{ add in0 in1 }});
+};
+```
+
+### Polymorphism
+
+In general, Cryptol `foreign` functions can be polymorphic, with type
+parameters of kind `#`, representing e.g. the sizes of input sequences.
+However, any individual `LLVMSetup ()` spec only specifies the behavior
+of the LLVM function on inputs of concrete sizes. We handle this by
+allowing the argument term of `llvm_ffi_setup` to contain any necessary
+type arguments in addition to the Cryptol function name, so that the
+resulting term is monomorphic. The user can then define a parameterized
+specification simply as a SAWScript function in the usual way. For
+example, for a function `foreign f : {n, m} (fin n, fin m) => [n][32] ->
+[m][32]`, we can obtain a parameterized `LLVMSetup` spec by
+```
+let f_setup (n : Int) (m : Int) = llvm_ffi_setup {{ f`{n, m} }};
+```
+Note that the `Term` parameter that `llvm_ffi_setup` takes is restricted
+syntactically to the format described above (``{{ fun`{tyArg0, tyArg1,
+..., tyArgN} }}``), and cannot be any arbitrary term.
+
+### Supported types
+
+`llvm_ffi_setup` supports all Cryptol types that are supported by the
+Cryptol FFI, with the exception of `Integer`, `Rational`, `Z`, and
+`Float`. `Integer`, `Rational`, and `Z` are not supported since they are
+translated to `gmp` arbitrary-precision types which are hard for SAW to
+handle without additional overrides. There is no fundamental obstacle to
+supporting `Float`, and in fact `llvm_ffi_setup` itself does work with
+Cryptol floating point types, but the underlying functions such as
+`llvm_fresh_var` do not, so until that is implemented `llvm_ffi_setup`
+can generate a spec involving floating point types but it cannot
+actually be run.
+
+### Performing the verification
+
+The resulting `LLVMSetup ()` spec can be used with the existing
+`llvm_verify` function to perform the actual verification. And the
+`LLVMSpec` output from that can be used as an override as usual for
+further compositional verification.
+```
+f_ov <- llvm_verify mod "f" [] true (f_setup 3 5) z3;
+```
+
+As with the Cryptol FFI itself, SAW does not manage the compilation of
+the C source implementations of `foreign` functions to LLVM bitcode. For
+the verification to be meaningful, is expected that the LLVM module
+passed to `llvm_verify` matches the compiled dynamic library actually
+used with the Cryptol interpreter. Alternatively, on x86_64 Linux, SAW
+can perform verification directly on the `.so` ELF file with the
+experimental `llvm_verify_x86` command.
 
 # Extraction to the Coq theorem prover
 

intTests/IntegrationTest.hs

@@ -185,6 +185,7 @@ check_cryptol_specs testPath disabled tests = testCase "cryptol-specs Available"
                           , "test0035_aes_consistent"
                           , "test_w4"
                           , "test_examples"
+                          , "test_ffi_verify_salsa"
                           ]
       cspec_dir = takeDirectory testPath </> "deps" </> "cryptol-specs"
   in if need_cryptol_spec

intTests/test_ffi_verify/Makefile

@@ -0,0 +1,6 @@
+test.bc: test.c
+	clang -Wall -Werror -g -c -emit-llvm $< -o $@
+
+.PHONY: clean
+clean:
+	rm test.bc

intTests/test_ffi_verify/README.md

@@ -0,0 +1,9 @@
+Test the `llvm_ffi_setup` command for verifying Cryptol `foreign`
+functions.
+
+These test cases are mostly from the test suite for the Cryptol FFI, but
+with Cryptol implementations of each function provided as well so that
+we can verify them with SAW. Some functions are changed or removed since
+SAW doesn't support Cryptol's Float types right now. There are also some
+additional tests for the more tricky parts of the llvm_ffi_setup
+implementation.

intTests/test_ffi_verify/test.c

@@ -0,0 +1,118 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stddef.h>
+
+uint8_t add8(uint8_t x, uint8_t y) {
+  return x + y;
+}
+
+uint16_t sub16(uint16_t x, uint16_t y) {
+  return x - y;
+}
+
+uint32_t mul32(uint32_t x, uint32_t y) {
+  return x * y;
+}
+
+uint64_t div64(uint64_t x, uint64_t y) {
+  if (y == 0) {
+    return 0;
+  }
+  return x / y;
+}
+
+uint8_t extendInput(uint8_t x) {
+  return x;
+}
+
+uint8_t maskOutput(uint8_t x) {
+  return x;
+}
+
+uint8_t noBits(uint8_t zero) {
+  assert(zero == 0);
+  return 1;
+}
+
+uint8_t not(uint8_t x) {
+  return !x;
+}
+
+uint8_t usesTypeSynonym(uint32_t x, uint64_t y) {
+  return x == y;
+}
+
+uint32_t sum10(uint32_t *xs) {
+  uint32_t sum = 0;
+  for (unsigned i = 0; i < 10; ++i) {
+    sum += xs[i];
+  }
+  return sum;
+}
+
+void reverse5(uint64_t *in, uint64_t *out) {
+  for (unsigned i = 0; i < 5; ++i) {
+    out[i] = in[4 - i];
+  }
+}
+
+void compoundTypes(uint32_t n, uint16_t x, uint32_t *y, uint32_t *z,
+    uint16_t *a_0, uint16_t *a_1, uint32_t *c, uint8_t *d, uint8_t *e) {
+  *a_0 = n >> 16;
+  *a_1 = n;
+  for (unsigned i = 0; i < 3; ++i) {
+    c[i] = y[i];
+  }
+  for (unsigned i = 0; i < 5; ++i) {
+    c[i + 3] = z[i];
+  }
+  *d = x >> 5;
+  *e = x;
+}
+
+uint64_t typeToValue(size_t n) {
+  return n;
+}
+
+uint32_t sumPoly(size_t n, uint32_t *xs) {
+  uint32_t sum = 0;
+  for (size_t i = 0; i < n; ++i) {
+    sum += xs[i];
+  }
+  return sum;
+}
+
+void inits(size_t n, uint8_t *in, uint8_t *out) {
+  for (unsigned i = 1; i <= n; ++i) {
+    for (unsigned j = 0; j < i; ++j) {
+      *out++ = in[j];
+    }
+  }
+}
+
+void zipMul3(size_t n, size_t m, size_t p,
+    uint32_t *xs, uint32_t *ys, uint32_t *zs, uint32_t *out) {
+  for (size_t i = 0; i < n && i < m && i < p; ++i) {
+    out[i] = xs[i] * ys[i] * zs[i];
+  }
+}
+
+void reshape(size_t a, size_t b, size_t c, size_t d,
+    uint32_t *abcd, uint32_t *dcba, uint32_t *acbd) {
+  for (size_t i = 0; i < a * b * c * d; ++i) {
+    dcba[i] = acbd[i] = abcd[i];
+  }
+}
+
+void same(uint32_t n, uint16_t x, uint32_t *yz,\
+    uint32_t *n1, uint16_t *x1, uint32_t *yz1) {
+  uint16_t a_0, a_1;
+  uint8_t d, e;
+  compoundTypes(n, x, yz, yz + 3, &a_0, &a_1, yz1, &d, &e);
+  *n1 = a_0 << 16 | a_1;
+  *x1 = d << 5 | (e & 0x1f);
+}
+
+uint8_t notnot(uint8_t x) {
+    return x;
+}