saw-remote-api/feat/saw llvm tweaks

saw-remote-api/saw-remote-api/Main.hs

@@ -18,7 +18,7 @@ import SAWServer.SetOption
 
 main :: IO ()
 main =
-  do theApp <- mkApp "SAW RPC Server" serverDocs initialState sawMethods
+  do theApp <- mkDefaultApp "SAW RPC Server" serverDocs initialState sawMethods
      defaultMain description theApp
 
 serverDocs :: [Doc.Block]

saw-remote-api/src/SAWServer.hs

@@ -80,13 +80,14 @@ instance Show SAWTask where
 data CrucibleSetupVal e
   = NullValue
   | ArrayValue [CrucibleSetupVal e]
+  | StructValue [CrucibleSetupVal e]
   -- | TupleValue [CrucibleSetupVal e]
   -- | RecordValue [(String, CrucibleSetupVal e)]
   | FieldLValue (CrucibleSetupVal e) String
   | ElementLValue (CrucibleSetupVal e) Int
   | GlobalInitializer String
   | GlobalLValue String
-  | ServerValue ServerName
+  | NamedValue ServerName
   | CryptolExpr e
   deriving stock (Foldable, Functor, Traversable)
 

saw-remote-api/src/SAWServer/Data/SetupValue.hs

@@ -9,10 +9,11 @@ import Data.Aeson (FromJSON(..), withObject, withText, (.:))
 import SAWServer
 
 data SetupValTag
-  = TagServerValue
+  = TagNamedValue
   | TagNullValue
   | TagCryptol
   | TagArrayValue
+  | TagStructValue
   | TagFieldLValue
   | TagElemLValue
   | TagGlobalInit
@@ -22,11 +23,12 @@ instance FromJSON SetupValTag where
   parseJSON =
     withText "tag for setup value" $
     \case
-      "saved" -> pure TagServerValue
-      "null value" -> pure TagNullValue
+      "named" -> pure TagNamedValue
+      "null" -> pure TagNullValue
       "Cryptol" -> pure TagCryptol
-      "array value" -> pure TagArrayValue
-      "field lvalue" -> pure TagFieldLValue
+      "array" -> pure TagArrayValue
+      "struct" -> pure TagStructValue
+      "field" -> pure TagFieldLValue
       "element lvalue" -> pure TagElemLValue
       "global initializer" -> pure TagGlobalInit
       "global lvalue" -> pure TagGlobalLValue
@@ -38,10 +40,11 @@ instance FromJSON cryptolExpr => FromJSON (CrucibleSetupVal cryptolExpr) where
       fromObject = withObject "saved value or Cryptol expression" $ \o ->
         o .: "setup value" >>=
         \case
-          TagServerValue -> ServerValue <$> o .: "name"
+          TagNamedValue -> NamedValue <$> o .: "name"
           TagNullValue -> pure NullValue
           TagCryptol -> CryptolExpr <$> o .: "expression"
           TagArrayValue -> ArrayValue <$> o .: "elements"
+          TagStructValue -> StructValue <$> o .: "fields"
           TagFieldLValue -> FieldLValue <$> o .: "base" <*> o .: "field"
           TagElemLValue -> ElementLValue <$> o .: "base" <*> o .: "index"
           TagGlobalInit -> GlobalInitializer <$> o .: "name"

saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs

@@ -147,7 +147,7 @@ interpretJVMSetup fileReader bic cenv0 ss = runStateT (traverse_ go ss) (mempty,
     getSetupVal _ (GlobalLValue name) =
       JVMSetupM $ return $ MS.SetupGlobal () name
          -}
-    getSetupVal (env, _) (ServerValue n) = JVMSetupM $
+    getSetupVal (env, _) (NamedValue n) = JVMSetupM $
       resolve env n >>=
       \case
         Val x -> return x -- TODO add cases for the server values that

saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs

@@ -33,7 +33,7 @@ import qualified Cryptol.Parser.AST as P
 import Cryptol.Utils.Ident (mkIdent)
 import qualified Text.LLVM.AST as LLVM
 import qualified Data.LLVM.BitCode as LLVM
-import SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..))
+import qualified SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..))
 import SAWScript.Crucible.LLVM.Builtins
     ( llvm_alloc
     , llvm_alloc_aligned
@@ -75,7 +75,7 @@ instance FromJSON StartLLVMCrucibleSetupParams where
     withObject "params for \"SAW/Crucible setup\"" $ \o ->
     StartLLVMCrucibleSetupParams <$> o .: "name"
 
-data ServerSetupVal = Val (CMS.AllLLVM SetupValue)
+data ServerSetupVal = Val (CMS.AllLLVM MS.SetupValue)
 
 -- TODO: this is an extra layer of indirection that could be collapsed, but is easy to implement for now.
 compileLLVMContract ::
@@ -147,6 +147,9 @@ interpretLLVMSetup fileReader bic cenv0 ss =
     getSetupVal env (ArrayValue elts) =
       do elts' <- mapM (getSetupVal env) elts
          LLVMCrucibleSetupM $ return $ CMS.anySetupArray elts'
+    getSetupVal env (StructValue elts) =
+      do elts' <- mapM (getSetupVal env) elts
+         LLVMCrucibleSetupM $ return $ CMS.anySetupStruct False elts'
     getSetupVal env (FieldLValue base fld) =
       do base' <- getSetupVal env base
          LLVMCrucibleSetupM $ return $ CMS.anySetupField base' fld
@@ -157,10 +160,10 @@ interpretLLVMSetup fileReader bic cenv0 ss =
       LLVMCrucibleSetupM $ return $ CMS.anySetupGlobalInitializer name
     getSetupVal _ (GlobalLValue name) =
       LLVMCrucibleSetupM $ return $ CMS.anySetupGlobal name
-    getSetupVal (env, _) (ServerValue n) = LLVMCrucibleSetupM $
+    getSetupVal (env, _) (NamedValue n) = LLVMCrucibleSetupM $
       resolve env n >>=
       \case
-        Val x -> return x -- TODO add cases for the server values that
+        Val x -> return x -- TODO add cases for the named server values that
                           -- are not coming from the setup monad
                           -- (e.g. surrounding context)
     getSetupVal (_, cenv) (CryptolExpr expr) = LLVMCrucibleSetupM $

saw-remote-api/test-scripts/env_server.py

@@ -5,13 +5,13 @@
 def env_connect():
     server = os.environ.get('SAW_SERVER')
     if not server:
-        server = "cabal new-exec --verbose=0 saw-remote-api"
+        server = "cabal new-exec --verbose=0 saw-remote-api socket"
     print("Running: " + server)
     return conn.connect(server)
 
 def env_connect_global():
     server = os.environ.get('SAW_SERVER')
     if not server:
-        server = "cabal new-exec --verbose=0 saw-remote-api"
+        server = "cabal new-exec --verbose=0 saw-remote-api socket"
     print("Running: " + server)
     saw.connect(server)

saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.cry

@@ -0,0 +1,72 @@
+////////////////////////////////////////////////////////////////
+// Copyright 2016 Galois, Inc. All Rights Reserved
+//
+// Authors:
+//      Aaron Tomb : atomb@galois.com
+//	Nathan Collins : conathan@galois.com
+//      Joey Dodds : jdodds@galois.com
+//
+// Licensed under the Apache License, Version 2.0 (the "License").
+// You may not use this file except in compliance with the License.
+// A copy of the License is located at
+//
+//  http://aws.amazon.com/apache2.0
+//
+// or in the "license" file accompanying this file. This file is distributed
+// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
+// express or implied. See the License for the specific language governing
+// permissions and limitations under the License.
+//
+////////////////////////////////////////////////////////////////
+
+module HMAC where
+
+import SHA256
+
+//////// Functional version ////////
+
+hmacSHA256 : {pwBytes, msgBytes}
+             (fin pwBytes, fin msgBytes
+             , 32 >= width msgBytes
+             , 64 >= width (8*pwBytes)
+             , 64 >= width (8 * (64 + msgBytes))
+             ) => [pwBytes][8] -> [msgBytes][8] -> [256]
+hmacSHA256 = hmac `{blockLength=64} SHA256 SHA256 SHA256
+
+kinit : { pwBytes, blockLength, digest }
+        ( fin pwBytes, fin blockLength, fin digest )
+     => ([pwBytes][8] -> [8*digest])
+     -> [pwBytes][8]
+     -> [blockLength][8]
+kinit hash key =
+  if `pwBytes > (`blockLength : [max (width pwBytes) (width blockLength)])
+  then take `{blockLength} (split (hash key) # (zero : [blockLength][8]))
+  else take `{blockLength} (key # (zero : [blockLength][8]))
+
+// Due to limitations of the type system we must accept two
+// separate arguments (both aledgedly the same) for two
+// separate length inputs.
+hmac : { msgBytes, pwBytes, digest, blockLength }
+       ( fin pwBytes, fin digest, fin blockLength )
+    => ([blockLength + msgBytes][8] -> [8*digest])
+    -> ([blockLength + digest][8] -> [8*digest])
+    -> ([pwBytes][8] -> [8*digest])
+    -> [pwBytes][8]
+    -> [msgBytes][8]
+    -> [digest*8]
+hmac hash hash2 hash3 key message = hash2 (okey # internal)
+ where
+   ks : [blockLength][8]
+   ks = kinit hash3 key
+   okey = [k ^ 0x5C | k <- ks]
+   ikey = [k ^ 0x36 | k <- ks]
+   internal = split (hash (ikey # message))
+
+
+
+
+
+
+
+
+