Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

saw-remote-api/feat/saw llvm tweaks #1026

Merged
merged 8 commits into from
Jan 21, 2021
Merged
Show file tree
Hide file tree
Changes from 7 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion saw-remote-api/saw-remote-api/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
3 changes: 2 additions & 1 deletion saw-remote-api/src/SAWServer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -80,13 +80,14 @@ instance Show SAWTask where
data CrucibleSetupVal e
= NullValue
| ArrayValue [CrucibleSetupVal e]
| StructValue [CrucibleSetupVal e]
pnwamk marked this conversation as resolved.
Show resolved Hide resolved
-- | 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)

Expand Down
15 changes: 9 additions & 6 deletions saw-remote-api/src/SAWServer/Data/SetupValue.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,11 @@ import Data.Aeson (FromJSON(..), withObject, withText, (.:))
import SAWServer

data SetupValTag
= TagServerValue
= TagNamedValue
| TagNullValue
| TagCryptol
| TagArrayValue
| TagStructValue
| TagFieldLValue
| TagElemLValue
| TagGlobalInit
Expand All @@ -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
Expand All @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
11 changes: 7 additions & 4 deletions saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 ::
Expand Down Expand Up @@ -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
Expand All @@ -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 $
Expand Down
4 changes: 2 additions & 2 deletions saw-remote-api/test-scripts/env_server.py
Original file line number Diff line number Diff line change
Expand Up @@ -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)
72 changes: 72 additions & 0 deletions saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.cry
Original file line number Diff line number Diff line change
@@ -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))









Loading