crucible-syntax: Add support for externs

crucible-concurrency/src/Cruces/CrucesMain.hs

@@ -141,9 +141,12 @@ run (cruxOpts, opts) =
  Left err -> error $ show err
  Right (ParsedProgram
  { parsedProgGlobals = gs
+ , parsedProgExterns = externs
  , parsedProgCFGs = cs
  , parsedProgForwardDecs = fds
  }) -> do
+ unless (Map.null externs) $
+ error "Externs not currently supported"
  unless (Map.null fds) $
  error "Forward declarations not currently supported"
  return ( findMain (fromString "main") cs

crucible-syntax/README.txt

@@ -87,6 +87,22 @@ of a function ahead of time, but you will know it at some point after parsing
 the program. It is the responsibility of the client to ensure that forward
 declarations are resolved to Crucible definitions before being invoked.
 
+Global variables
+
+A global variable is a form that begins with the keyword "defglobal", followed
+by an identifier prefixed with two dollar signs (e.g., $$global-name) as well
+as a type. A global variable is a mutable reference that scopes over all of the
+functions defined in the program. The value of a global variable can be set
+with the "set-global!" form.
+
+A program can reference a global variable defined externally by using an extern
+declaration. An extern declaration is exactly like a "defglobal" declaration,
+but using the "extern" keyword instead of "defglobal". The difference between
+an extern and a normal global variable is that the value of an extern may
+already have been set by the time that the .cbl file which declares the extern
+uses it. It is the responsibility of the client to ensure that externs are
+inserted into the Crucible symbolic global state before being accessed.
+
 Types
 
 si ::= 'Unicode' | 'Char16' | 'Char8'

crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs

@@ -40,7 +40,7 @@ newtype FunName = FunName Text deriving (Eq, Ord, Show)
 newtype GlobalName = GlobalName Text deriving (Eq, Ord, Show)
 
 -- | Individual language keywords (reserved identifiers)
-data Keyword = Defun | DefBlock | DefGlobal | Declare
+data Keyword = Defun | DefBlock | DefGlobal | Declare | Extern
  | Registers
  | Start
  | SetGlobal
@@ -93,6 +93,7 @@ keywords =
  , ("defblock", DefBlock)
  , ("defglobal", DefGlobal)
  , ("declare", Declare)
+ , ("extern", Extern)
  , ("registers", Registers)
 
  -- statements

crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs

@@ -191,6 +191,10 @@ defaultParserHooks = ParserHooks empty empty
 data ParsedProgram ext = ParsedProgram
  { parsedProgGlobals :: Map GlobalName (Pair TypeRepr GlobalVar)
  -- ^ The parsed @defglobal@s.
+ , parsedProgExterns :: Map GlobalName (Pair TypeRepr GlobalVar)
+ -- ^ For each parsed @extern@, map its name to its type and global variable.
+ -- It is the responsibility of the caller to insert each global variable
+ -- into the 'SymGlobalState' alongside an appropriate 'RegValue'.
  , parsedProgCFGs :: [ACFG ext]
  -- ^ The CFGs for each parsed @defun@.
  , parsedProgForwardDecs :: Map FunctionName SomeHandle
@@ -1284,6 +1288,7 @@ data ProgramState s =
  ProgramState { _progFunctions :: Map FunctionName FunctionHeader
  , _progForwardDecs :: Map FunctionName FunctionHeader
  , _progGlobals :: Map GlobalName (Pair TypeRepr GlobalVar)
+ , _progExterns :: Map GlobalName (Pair TypeRepr GlobalVar)
  , _progHandleAlloc :: HandleAllocator
  }
 
@@ -1296,6 +1301,9 @@ progForwardDecs = lens _progForwardDecs (\s v -> s { _progForwardDecs = v })
 progGlobals :: Simple Lens (ProgramState s) (Map GlobalName (Pair TypeRepr GlobalVar))
 progGlobals = lens _progGlobals (\s v -> s { _progGlobals = v })
 
+progExterns :: Simple Lens (ProgramState s) (Map GlobalName (Pair TypeRepr GlobalVar))
+progExterns = lens _progExterns (\s v -> s { _progExterns = v })
+
 progHandleAlloc :: Simple Lens (ProgramState s) HandleAllocator
 progHandleAlloc = lens _progHandleAlloc (\s v -> s { _progHandleAlloc = v })
 
@@ -1309,7 +1317,7 @@ data SyntaxState s =
  }
 
 initProgState :: [(SomeHandle,Position)] -> HandleAllocator -> ProgramState s
-initProgState builtIns ha = ProgramState fns Map.empty Map.empty ha
+initProgState builtIns ha = ProgramState fns Map.empty Map.empty Map.empty ha
  where
  f tps = Ctx.generate
  (Ctx.size tps)
@@ -1354,6 +1362,8 @@ stxForwardDecs = stxProgState . progForwardDecs
 stxGlobals :: Simple Lens (SyntaxState s) (Map GlobalName (Pair TypeRepr GlobalVar))
 stxGlobals = stxProgState . progGlobals
 
+stxExterns :: Simple Lens (SyntaxState s) (Map GlobalName (Pair TypeRepr GlobalVar))
+stxExterns = stxProgState . progExterns
 
 newtype CFGParser s ret a =
  CFGParser { runCFGParser :: (?returnType :: TypeRepr ret)
@@ -1499,7 +1509,8 @@ globRef' =
  describe "known global variable name" $
  do x <- globalName
  perhapsGlobal <- view (stxGlobals . at x)
- case perhapsGlobal of
+ perhapsExtern <- view (stxExterns . at x)
+ case perhapsGlobal <|> perhapsExtern of
  Just glob -> return glob
  Nothing -> empty
 
@@ -2038,13 +2049,25 @@ declare stx =
  stxForwardDecs %= Map.insert fnName header
  pure header
 
+-- | Parse an extern.
+extern :: (?parserHooks :: ParserHooks ext)
+ => AST s
+ -> TopParser s (Pair TypeRepr GlobalVar)
+extern stx =
+ do (var@(GlobalName varName), Some t) <- liftSyntaxParse (call (binary Extern globalName isType)) stx
+ ha <- use $ stxProgState . progHandleAlloc
+ v <- liftIO $ freshGlobalVar ha varName t
+ stxExterns %= Map.insert var (Pair t v)
+ return $ Pair t v
+
 topLevel :: (?parserHooks :: ParserHooks ext)
  => AST s
  -> TopParser s (Maybe (FunctionHeader, FunctionSource s))
 topLevel ast =
  (Just <$> functionHeader ast) `catchError` \e ->
  (global ast $> Nothing) `catchError` \_ ->
  (declare ast $> Nothing) `catchError` \_ ->
+ (extern ast $> Nothing) `catchError` \_ ->
  throwError e
 
 argTypes :: Ctx.Assignment Arg init -> Ctx.Assignment TypeRepr init
@@ -2221,10 +2244,12 @@ prog defuns =
  e' = mkBlock (blockID e) vs (blockStmts e) (blockTerm e)
  return $ ACFG types ret $ CFG handle entry (e' : rest)
  gs <- use stxGlobals
+ externs <- use stxExterns
  fds <- uses stxForwardDecs $ fmap $
  \(FunctionHeader _ _ _ handle _) -> SomeHandle handle
  return $ ParsedProgram
  { parsedProgGlobals = gs
+ , parsedProgExterns = externs
  , parsedProgCFGs = cs
  , parsedProgForwardDecs = fds
  }

crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs

@@ -26,6 +26,7 @@ import Text.Megaparsec as MP
 
 import Data.Parameterized.Nonce
 import qualified Data.Parameterized.Context as Ctx
+import Data.Parameterized.Pair (Pair(..))
 import Data.Parameterized.Some (Some(Some))
 
 import qualified Lang.Crucible.CFG.Core as C
@@ -43,6 +44,7 @@ import Lang.Crucible.Backend.Simple
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
 import Lang.Crucible.Simulator.Profiling
+import Lang.Crucible.Types (TypeRepr)
 
 import What4.Config
 import What4.Interface (getConfiguration,notPred)
@@ -77,8 +79,10 @@ doParseCheck fn theInput pprint outh =
  Left (SyntaxParseError e) -> T.hPutStrLn outh $ printSyntaxError e
  Left err -> hPutStrLn outh $ show err
  Right (ParsedProgram{ parsedProgCFGs = ok
+ , parsedProgExterns = externs
  , parsedProgForwardDecs = fds
  }) -> do
+ assertNoExterns externs
  assertNoForwardDecs fds
  forM_ ok $
  \(ACFG _ _ theCfg) ->
@@ -92,6 +96,12 @@ data SimulateProgramHooks = SimulateProgramHooks
  forall p sym ext t st fs. (IsSymInterface sym, sym ~ (ExprBuilder t st fs)) =>
  sym -> HandleAllocator -> IO [(FnBinding p sym ext,Position)]
  -- ^ Action to set up overrides before parsing a program.
+ , resolveExternsHook ::
+ forall sym t st fs. (IsSymInterface sym, sym ~ (ExprBuilder t st fs)) =>
+ sym -> Map GlobalName (Pair TypeRepr GlobalVar) -> SymGlobalState sym -> IO (SymGlobalState sym)
+ -- ^ Action to resolve externs before simulating a program. If you do not
+ -- intend to support externs, this is an appropriate place to error if a
+ -- program contains one or more externs.
  , resolveForwardDeclarationsHook ::
  forall p sym ext t st fs. (IsSymInterface sym, sym ~ (ExprBuilder t st fs)) =>
  Map FunctionName SomeHandle -> IO (FunctionBindings p sym ext)
@@ -109,11 +119,20 @@ data SimulateProgramHooks = SimulateProgramHooks
 defaultSimulateProgramHooks :: SimulateProgramHooks
 defaultSimulateProgramHooks = SimulateProgramHooks
  { setupOverridesHook = \_sym _ha -> pure []
+ , resolveExternsHook = \_sym externs gst ->
+ do assertNoExterns externs
+ pure gst
  , resolveForwardDeclarationsHook = \fds ->
  do assertNoForwardDecs fds
  pure $ FnBindings emptyHandleMap
  }
 
+assertNoExterns :: Map GlobalName (Pair TypeRepr GlobalVar) -> IO ()
+assertNoExterns externs =
+ unless (Map.null externs) $
+ do putStrLn "Externs not currently supported"
+ exitFailure
+
 assertNoForwardDecs :: Map FunctionName SomeHandle -> IO ()
 assertNoForwardDecs fds =
  unless (Map.null fds) $
@@ -148,11 +167,13 @@ simulateProgram fn theInput outh profh opts hooks =
  Left (SyntaxParseError e) -> T.hPutStrLn outh $ printSyntaxError e
  Left err -> hPutStrLn outh $ show err
  Right (ParsedProgram{ parsedProgCFGs = cs
+ , parsedProgExterns = externs
  , parsedProgForwardDecs = fds
  }) -> do
  case find isMain cs of
  Just (ACFG Ctx.Empty retType mn) ->
- do fwdDecFnBindings <- resolveForwardDeclarationsHook hooks fds
+ do gst <- resolveExternsHook hooks sym externs emptyGlobals
+ fwdDecFnBindings <- resolveForwardDeclarationsHook hooks fds
  let mainHdl = cfgHandle mn
  let fns = foldl' (\(FnBindings m) (ACFG _ _ g) ->
  case toSSA g of
@@ -164,7 +185,7 @@ simulateProgram fn theInput outh profh opts hooks =
  m)
  fwdDecFnBindings cs
  let simCtx = initSimContext bak emptyIntrinsicTypes ha outh fns emptyExtensionImpl ()
- let simSt = InitialState simCtx emptyGlobals defaultAbortHandler retType $
+ let simSt = InitialState simCtx gst defaultAbortHandler retType $
  runOverrideSim retType $
  do mapM_ (registerFnBinding . fst) ovrs
  regValue <$> callFnVal (HandleFnVal mainHdl) emptyRegMap

crucible-syntax/test-data/extern-tests/main.cbl

@@ -0,0 +1,7 @@
+(extern $$foo Integer)
+
+(defun @main () Unit
+ (start start:
+ (assert! (equal? $$foo 42) "$$foo equals 42")
+ (return ()))
+)

crucible-syntax/test-data/extern-tests/main.out.good

@@ -0,0 +1,4 @@
+==== Begin Simulation ====
+
+==== Finish Simulation ====
+==== No proof obligations ====

crucible-syntax/test/Tests.hs

@@ -15,6 +15,7 @@ import qualified Data.Map as Map
 import Data.Map (Map)
 import Data.Monoid
 import qualified Data.Parameterized.Context as Ctx
+import Data.Parameterized.Pair (Pair(..))
 import Data.Text (Text)
 import Data.Type.Equality (TestEquality(..), (:~:)(..))
 import qualified Data.Text as T
@@ -27,12 +28,15 @@ import Lang.Crucible.Syntax.Concrete hiding (SyntaxError)
 import Lang.Crucible.Backend (IsSymInterface)
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator.ExecutionTree
+import Lang.Crucible.Simulator.GlobalState (SymGlobalState, insertGlobal)
 import Lang.Crucible.Simulator.OverrideSim
+import Lang.Crucible.Syntax.Atoms (GlobalName(..))
 import Lang.Crucible.Syntax.Prog
 import Lang.Crucible.Syntax.SExpr
 import Lang.Crucible.Syntax.ExprParse
 import Lang.Crucible.Syntax.Overrides as SyntaxOvrs
 import Lang.Crucible.Types
+import Lang.Crucible.CFG.Common (GlobalVar)
 import Lang.Crucible.CFG.SSAConversion
 
 import Test.Tasty (defaultMain, TestTree, testGroup)
@@ -278,3 +282,32 @@ resolvedForwardDecTest =
  fooOv = mkOverride "foo" $ do
  sym <- use (stateContext.ctxSymInterface)
  liftIO $ intLit sym 42
+
+-- | A basic test that ensures an extern behaves as expected after assigning a
+-- value to it after parsing.
+resolvedExternTest :: TestTree
+resolvedExternTest =
+ testGroup "Externs"
+ [ goldenFileTestCase ("test-data" </> "extern-tests" </> "main.cbl") $ \mainCbl mainOut ->
+ withFile mainOut WriteMode $ \outh ->
+ do mainContents <- T.readFile mainCbl
+ simulateProgram mainCbl mainContents outh Nothing testOptions $
+ defaultSimulateProgramHooks
+ { resolveExternsHook = resolveExterns
+ }
+ ]
+ where
+ resolveExterns ::
+ IsSymInterface sym =>
+ sym ->
+ Map GlobalName (Pair TypeRepr GlobalVar) ->
+ SymGlobalState sym ->
+ IO (SymGlobalState sym)
+ resolveExterns sym externs gst
+ | Just (Pair tp gv) <- Map.lookup (GlobalName "foo") externs
+ , Just Refl <- testEquality tp IntegerRepr
+ = do fooVal <- intLit sym 42
+ pure $ insertGlobal gv fooVal gst
+
+ | otherwise
+ = assertFailure "Could not find $$foo extern of the appropriate type"