{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
module ReWire.FrontEnd
      ( LoadPath
      , compileFile
      ) where

import ReWire.Annotation (Annote, noAnn, unAnn)
import ReWire.Config (Config, Language (..), Certify (..), getOutFile, target, cycles, inputsFile, defaultInputsFile, source, rtlOpt, testbench, pDebug, loadPath, locators, noLocators)
import ReWire.Error (MonadError, AstError, runSyntaxError, failAt, warnAt, printError, relocatingNoLocTo, filePath)
import ReWire.Hyle.Interp (Ins, run)
import ReWire.Hyle.Parse (parseHyle)
import ReWire.Hyle.Syntax (Program, progDevice)
import ReWire.ModCache (getDevice, LoadPath)
import ReWire.Pass (pass)
import ReWire.Pretty (Pretty, prettyPrint, fastPrint, showt)
import ReWire.Sha256 (hashHex)

import qualified ReWire.Config           as Config
import qualified ReWire.Hyle.Check     as Hyle
import qualified ReWire.Hyle.Interp    as Hyle
import qualified ReWire.Hyle.ToCryptol as HyleCry
import qualified ReWire.Hyle.ToVHDL    as HyleH
import qualified ReWire.Hyle.ToVerilog as HyleV
import qualified ReWire.Hyle.Transform as Hyle

import Control.Exception (IOException, try)
import Control.Lens ((^.))
import Control.Monad (when)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.Monad.State (MonadState)
import Data.Aeson (FromJSON (..), eitherDecodeStrict, withObject, (.:))
import Data.Char (toLower)
import Data.Maybe (fromMaybe)
import Data.Text (Text, pack, unpack)
import Data.Text.Encoding (encodeUtf8)
import GHC.Clock (getMonotonicTimeNSec)
import Numeric.Natural (Natural)
import System.Directory (doesFileExist, executable, findExecutable, getPermissions, renameFile)
import System.Environment (lookupEnv, getExecutablePath)
import System.Exit (ExitCode (..), exitFailure)
import System.FilePath (dropExtension, takeDirectory, takeExtension, (<.>), (-<.>), (</>))
import System.IO (stderr)
import System.Process (proc, readCreateProcessWithExitCode)
import System.Timeout (timeout)

import qualified Data.ByteString     as BS
import qualified Data.HashMap.Strict as Map
import qualified Data.Text           as Text
import qualified Data.Text.IO        as T
import qualified Data.Yaml           as YAML

-- | Loads and compiles a file (and, recursively, its imports) to a Hyle
--   program (the whole pass pipeline through the Eidos-to-Hyle fold).
loadProgram :: (MonadFail m, MonadError AstError m, MonadState AstError m, MonadIO m) => Config -> FilePath -> m Program
loadProgram :: forall (m :: * -> *).
(MonadFail m, MonadError AstError m, MonadState AstError m,
 MonadIO m) =>
Config -> String -> m Program
loadProgram = Config -> String -> m Program
forall (m :: * -> *).
(MonadIO m, MonadFail m, MonadError AstError m,
 MonadState AstError m) =>
Config -> String -> m Program
getDevice

compileFile :: MonadIO m => Config -> FilePath -> m ()
compileFile :: forall (m :: * -> *). MonadIO m => Config -> String -> m ()
compileFile Config
conf String
filename = do
      Name -> m ()
forall (m :: * -> *). MonadIO m => Name -> m ()
verb (Name -> m ()) -> Name -> m ()
forall a b. (a -> b) -> a -> b
$ Name
"Compiling: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
filename

      SyntaxErrorT AstError m () -> m (Either AstError ())
forall (m :: * -> *) a.
Monad m =>
SyntaxErrorT AstError m a -> m (Either AstError a)
runSyntaxError (Annote -> SyntaxErrorT AstError m () -> SyntaxErrorT AstError m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> m a -> m a
relocatingNoLocTo (String -> Annote
filePath String
filename) (SyntaxErrorT AstError m () -> SyntaxErrorT AstError m ())
-> SyntaxErrorT AstError m () -> SyntaxErrorT AstError m ()
forall a b. (a -> b) -> a -> b
$ SyntaxErrorT AstError m ()
forall (m :: * -> *). (MonadError AstError m, MonadIO m) => m ()
checkCertifyPaths SyntaxErrorT AstError m ()
-> SyntaxErrorT AstError m Program
-> SyntaxErrorT AstError m Program
forall a b.
SyntaxErrorT AstError m a
-> SyntaxErrorT AstError m b -> SyntaxErrorT AstError m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SyntaxErrorT AstError m Program
forall (m :: * -> *).
(MonadError AstError m, MonadState AstError m, MonadFail m,
 MonadIO m) =>
m Program
load SyntaxErrorT AstError m Program
-> (Program -> SyntaxErrorT AstError m Program)
-> SyntaxErrorT AstError m Program
forall a b.
SyntaxErrorT AstError m a
-> (a -> SyntaxErrorT AstError m b) -> SyntaxErrorT AstError m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Program -> SyntaxErrorT AstError m Program
forall (m :: * -> *). MonadError AstError m => Program -> m Program
Hyle.check SyntaxErrorT AstError m Program
-> (Program -> SyntaxErrorT AstError m ())
-> SyntaxErrorT AstError m ()
forall a b.
SyntaxErrorT AstError m a
-> (a -> SyntaxErrorT AstError m b) -> SyntaxErrorT AstError m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Program -> SyntaxErrorT AstError m ()
forall (m :: * -> *).
(MonadFail m, MonadError AstError m, MonadIO m) =>
Program -> m ()
compile)
            m (Either AstError ()) -> (Either AstError () -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (AstError -> m ()) -> (() -> m ()) -> Either AstError () -> m ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\ AstError
err -> [String] -> AstError -> m ()
forall (m :: * -> *). MonadIO m => [String] -> AstError -> m ()
printError (Config
conf Config -> Getting [String] Config [String] -> [String]
forall s a. s -> Getting a s a -> a
^. Getting [String] Config [String]
Lens' Config [String]
loadPath) AstError
err m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ()
forall a. IO a
exitFailure) () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

      where load :: (MonadError AstError m, MonadState AstError m, MonadFail m, MonadIO m) => m Program
            load :: forall (m :: * -> *).
(MonadError AstError m, MonadState AstError m, MonadFail m,
 MonadIO m) =>
m Program
load = case Config
confConfig -> Getting Language Config Language -> Language
forall s a. s -> Getting a s a -> a
^.Getting Language Config Language
Lens' Config Language
source of
                  Language
Haskell -> Config -> String -> m Program
forall (m :: * -> *).
(MonadFail m, MonadError AstError m, MonadState AstError m,
 MonadIO m) =>
Config -> String -> m Program
loadProgram Config
conf String
filename
                  Language
RWCore  -> String -> m Program
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
String -> m Program
parseHyle String
filename
                  Language
s       -> Annote -> Name -> m Program
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Name -> m a
failAt Annote
noAnn (Name -> m Program) -> Name -> m Program
forall a b. (a -> b) -> a -> b
$ Name
"Not a supported source language: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack (Language -> String
forall a. Show a => a -> String
show Language
s)

            -- The Hyle-level passes are numbered after ReWire.ModCache's 1-9
            -- (which -d/-v also address, but which only run for Haskell
            -- source), so the -d numbering is uniform across --from-core.
            compile :: (MonadFail m, MonadError AstError m, MonadIO m) => Program -> m ()
            compile :: forall (m :: * -> *).
(MonadFail m, MonadError AstError m, MonadIO m) =>
Program -> m ()
compile Program
a = do
                  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config
confConfig -> Getting Bool Config Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Config Bool
Lens' Config Bool
testbench Bool -> Bool -> Bool
&& (Config
confConfig -> Getting Language Config Language -> Language
forall s a. s -> Getting a s a -> a
^.Getting Language Config Language
Lens' Config Language
target) Language -> [Language] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Language
VHDL, Language
Verilog]) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                        Config -> Annote -> Name -> m ()
forall (m :: * -> *) an.
(MonadError AstError m, MonadIO m, Annotation an) =>
Config -> an -> Name -> m ()
warnAt Config
conf Annote
noAnn Name
"--testbench: no testbench generated (only the Verilog and VHDL targets support testbench generation)."
                  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
certifyOn Bool -> Bool -> Bool
&& Config
confConfig -> Getting Language Config Language -> Language
forall s a. s -> Getting a s a -> a
^.Getting Language Config Language
Lens' Config Language
target Language -> Language -> Bool
forall a. Eq a => a -> a -> Bool
== Language
Interpret) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                        Annote -> Name -> m ()
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Annote -> Name -> m ()
notCertified Annote
noAnn Name
"nothing to certify (only device targets are certified)."
                  p10 <- Config
-> String
-> Natural
-> Name
-> String
-> (Program -> Name)
-> (Program -> m Program)
-> Program
-> m Program
forall (m :: * -> *) a b.
(MonadIO m, Data b, Show b) =>
Config
-> String
-> Natural
-> Name
-> String
-> (b -> Name)
-> (a -> m b)
-> a
-> m b
pass Config
conf String
filename Natural
10 Name
"Partially evaluating/reducing the Hyle IR (if this is slow, consider --rtl-opt=0)." String
"rwc" Program -> Name
forall a. Pretty a => a -> Name
prettyPrint
                        (Program -> m Program
forall (m :: * -> *). MonadError AstError m => Program -> m Program
Hyle.check (Program -> m Program)
-> (Program -> Program) -> Program -> m Program
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Program -> Program
Hyle.optimize (Config
confConfig -> Getting Natural Config Natural -> Natural
forall s a. s -> Getting a s a -> a
^.Getting Natural Config Natural
Lens' Config Natural
rtlOpt)) Program
a
                  -- Pass 11 runs for every device target, so every consumer
                  -- -- the HDL and Cryptol backends, the interpreter, the
                  -- .rwc emitted by --core, and the certified artifact --
                  -- reads the same fully lowered program.
                  p <- pass conf filename 11 "Inlining Hyle definitions." "rwc" prettyPrint
                        (Hyle.check . Hyle.inline (conf^.Config.flatten)) p10
                  case conf^.target of
                        Language
VHDL      -> do
                              Config -> Program -> m Device
forall (m :: * -> *).
MonadError AstError m =>
Config -> Program -> m Device
HyleH.compileProgram Config
conf Program
p m Device -> (Device -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Device -> m ()
forall (m :: * -> *) a.
(MonadError AstError m, MonadIO m, Pretty a) =>
a -> m ()
writeOutput
                              ([Ins] -> Unit) -> m ()
forall (m :: * -> *) tb.
(MonadError AstError m, MonadIO m, Pretty tb) =>
([Ins] -> tb) -> m ()
writeTestbench (([Ins] -> Unit) -> m ()) -> ([Ins] -> Unit) -> m ()
forall a b. (a -> b) -> a -> b
$ Config -> Device -> [Ins] -> Unit
HyleH.testbench Config
conf (Device -> [Ins] -> Unit) -> Device -> [Ins] -> Unit
forall a b. (a -> b) -> a -> b
$ Program -> Device
progDevice Program
p
                              Program -> m ()
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Program -> m ()
certifyOutput Program
p
                        Language
Verilog   -> do
                              Config -> Program -> m Device
forall (m :: * -> *).
MonadError AstError m =>
Config -> Program -> m Device
HyleV.compileProgram Config
conf Program
p m Device -> (Device -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Device -> m ()
forall (m :: * -> *) a.
(MonadError AstError m, MonadIO m, Pretty a) =>
a -> m ()
writeOutput
                              ([Ins] -> Module) -> m ()
forall (m :: * -> *) tb.
(MonadError AstError m, MonadIO m, Pretty tb) =>
([Ins] -> tb) -> m ()
writeTestbench (([Ins] -> Module) -> m ()) -> ([Ins] -> Module) -> m ()
forall a b. (a -> b) -> a -> b
$ Config -> Device -> [Ins] -> Module
HyleV.testbench Config
conf (Device -> [Ins] -> Module) -> Device -> [Ins] -> Module
forall a b. (a -> b) -> a -> b
$ Program -> Device
progDevice Program
p
                              Program -> m ()
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Program -> m ()
certifyOutput Program
p
                        Language
Cryptol   -> do
                              Config -> Program -> m Module
forall (m :: * -> *).
MonadError AstError m =>
Config -> Program -> m Module
HyleCry.compileProgram Config
conf Program
p m Module -> (Module -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Module -> m ()
forall (m :: * -> *) a.
(MonadError AstError m, MonadIO m, Pretty a) =>
a -> m ()
writeOutput
                              Program -> m ()
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Program -> m ()
certifyOutput Program
p
                        Language
RWCore    -> do
                              Name -> m ()
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Name -> m ()
writeOutputText (Name -> m ()) -> Name -> m ()
forall a b. (a -> b) -> a -> b
$ Program -> Name
renderCore Program
p
                              Program -> m ()
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Program -> m ()
certifyOutput Program
p
                        Language
Interpret -> do
                              ips  <- m [Ins]
forall (m :: * -> *). (MonadError AstError m, MonadIO m) => m [Ins]
loadInputs
                              verb $ "Interpreting hyle: running for " <> showt (length ips) <> " cycles."
                              outs <- run conf (Hyle.interp conf p) ips
                              let fout = Config -> String -> String
getOutFile Config
conf String
filename
                              verb $ "Interpreting hyle: done running; writing YAML output to file: " <> pack fout
                              liftIO $ YAML.encodeFile fout outs
                        Language
Haskell   -> Annote -> Name -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Name -> m a
failAt Annote
noAnn Name
"Haskell is not a supported target language."

            -- | Inputs for --interpret and --testbench, padded/truncated to
            --   the cycle count. An unreadable inputs file means all wires
            --   are driven to zero -- warn, unless the file is missing and
            --   the user never named one explicitly (driving a device with
            --   no inputs file is a legitimate workflow).
            loadInputs :: (MonadError AstError m, MonadIO m) => m [Ins]
            loadInputs :: forall (m :: * -> *). (MonadError AstError m, MonadIO m) => m [Ins]
loadInputs = do
                  Name -> m ()
forall (m :: * -> *). MonadIO m => Name -> m ()
verb (Name -> m ()) -> Name -> m ()
forall a b. (a -> b) -> a -> b
$ Name
"Reading inputs: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack (Config
confConfig -> Getting String Config String -> String
forall s a. s -> Getting a s a -> a
^.Getting String Config String
Lens' Config String
inputsFile)
                  r <- IO (Either ParseException [Ins]) -> m (Either ParseException [Ins])
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either ParseException [Ins])
 -> m (Either ParseException [Ins]))
-> IO (Either ParseException [Ins])
-> m (Either ParseException [Ins])
forall a b. (a -> b) -> a -> b
$ String -> IO (Either ParseException [Ins])
forall a. FromJSON a => String -> IO (Either ParseException a)
YAML.decodeFileEither (String -> IO (Either ParseException [Ins]))
-> String -> IO (Either ParseException [Ins])
forall a b. (a -> b) -> a -> b
$ Config
confConfig -> Getting String Config String -> String
forall s a. s -> Getting a s a -> a
^.Getting String Config String
Lens' Config String
inputsFile
                  case r of
                        Right [Ins]
ips -> [Ins] -> m [Ins]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Ins] -> m [Ins]) -> [Ins] -> m [Ins]
forall a b. (a -> b) -> a -> b
$ Natural -> [Ins] -> [Ins]
boundInput (Config -> [Ins] -> Natural
effectiveCycles Config
conf [Ins]
ips) [Ins]
ips
                        Left ParseException
err  -> do
                              exists <- IO Bool -> m Bool
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> m Bool) -> IO Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesFileExist (String -> IO Bool) -> String -> IO Bool
forall a b. (a -> b) -> a -> b
$ Config
confConfig -> Getting String Config String -> String
forall s a. s -> Getting a s a -> a
^.Getting String Config String
Lens' Config String
inputsFile
                              when (exists || conf^.inputsFile /= defaultInputsFile) $ warnAt conf noAnn
                                    $ "could not read inputs from " <> pack (conf^.inputsFile)
                                    <> (if exists then " (" <> pack (YAML.prettyPrintParseException err) <> ")" else " (file does not exist)")
                                    <> "; driving all inputs with zeros."
                              pure $ boundInput (effectiveCycles conf mempty) mempty

            writeTestbench :: (MonadError AstError m, MonadIO m, Pretty tb) => ([Ins] -> tb) -> m ()
            writeTestbench :: forall (m :: * -> *) tb.
(MonadError AstError m, MonadIO m, Pretty tb) =>
([Ins] -> tb) -> m ()
writeTestbench [Ins] -> tb
gen = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config
confConfig -> Getting Bool Config Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Config Bool
Lens' Config Bool
testbench) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
                  ips <- m [Ins]
forall (m :: * -> *). (MonadError AstError m, MonadIO m) => m [Ins]
loadInputs
                  let fout = Config -> String -> String
getOutFile Config
conf String
filename
                      tbout = String -> String
dropExtension String
fout String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"_tb" String -> String -> String
<.> String -> String
takeExtension String
fout
                  verb $ "Writing testbench to file: " <> pack tbout
                  liftIO $ T.writeFile tbout $ (if conf^.Config.pretty then prettyPrint else fastPrint) $ gen ips

            writeOutput :: (MonadError AstError m, MonadIO m, Pretty a) => a -> m ()
            writeOutput :: forall (m :: * -> *) a.
(MonadError AstError m, MonadIO m, Pretty a) =>
a -> m ()
writeOutput = Name -> m ()
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Name -> m ()
writeOutputText (Name -> m ()) -> (a -> Name) -> a -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if Config
confConfig -> Getting Bool Config Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Config Bool
Lens' Config Bool
Config.pretty then a -> Name
forall a. Pretty a => a -> Name
prettyPrint else a -> Name
forall a. Pretty a => a -> Name
fastPrint)

            writeOutputText :: (MonadError AstError m, MonadIO m) => Text -> m ()
            writeOutputText :: forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Name -> m ()
writeOutputText Name
txt = do
                  let fout :: String
fout = Config -> String -> String
getOutFile Config
conf String
filename
                  Name -> m ()
forall (m :: * -> *). MonadIO m => Name -> m ()
verb (Name -> m ()) -> Name -> m ()
forall a b. (a -> b) -> a -> b
$ Name
"Writing to file: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
fout
                  IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> Name -> IO ()
T.writeFile String
fout Name
txt

            -- | The rendered .rwc text, shared by the RWCore target and the
            --   --certify artifact so the two outputs are byte-identical.
            --   It only carries source locators ('--@' lines) under
            --   --locators (and not under --no-locators, which wins): spans
            --   can embed absolute paths, which would destabilize golden
            --   files. Doc ('--|') and 'tag' lines are path-free and not
            --   gated.
            renderCore :: Program -> Text
            renderCore :: Program -> Name
renderCore Program
p
                  | Config
confConfig -> Getting Bool Config Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Config Bool
Lens' Config Bool
locators Bool -> Bool -> Bool
&& Bool -> Bool
not (Config
confConfig -> Getting Bool Config Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Config Bool
Lens' Config Bool
noLocators) = Program -> Name
render Program
p
                  | Bool
otherwise                                = Program -> Name
render (Program -> Name) -> Program -> Name
forall a b. (a -> b) -> a -> b
$ Program -> Program
scrubSpans Program
p
                  where render :: Program -> Text
                        render :: Program -> Name
render = if Config
confConfig -> Getting Bool Config Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Config Bool
Lens' Config Bool
Config.pretty then Program -> Name
forall a. Pretty a => a -> Name
prettyPrint else Program -> Name
forall a. Pretty a => a -> Name
fastPrint

            -- | --certify: write the certified pair beside the output --
            --   the Synolon IR (<out>.syn, the --synolon dump, written by
            --   ReWire.ModCache) and the final backend-consumed
            --   Hyle program (<out>.rwc, byte-identical to the --core
            --   output) -- run the verified validator on it over the
            --   versioned response protocol, and surface the verdict: a
            --   one-line confirmation on VALIDATED, otherwise fatal
            --   (required mode, the default) or an unsuppressible status
            --   line (--certify=warn). See doc/certify.md.
            certifyOutput :: (MonadError AstError m, MonadIO m) => Program -> m ()
            certifyOutput :: forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Program -> m ()
certifyOutput Program
p11 = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
certifyOn (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ case Config
confConfig -> Getting Language Config Language -> Language
forall s a. s -> Getting a s a -> a
^.Getting Language Config Language
Lens' Config Language
source of
                  -- The artifact shares the --core output naming, so an
                  -- HDL/Cryptol output explicitly named *.rwc (-o) would
                  -- collide with it; refuse rather than clobber the
                  -- requested output. (For the RWCore target the collision
                  -- is the point: the same bytes are written either way.)
                  Language
Haskell | Config
confConfig -> Getting Language Config Language -> Language
forall s a. s -> Getting a s a -> a
^.Getting Language Config Language
Lens' Config Language
target Language -> Language -> Bool
forall a. Eq a => a -> a -> Bool
/= Language
RWCore Bool -> Bool -> Bool
&& String -> String -> Bool
samePath String
rwcFile (Config -> String -> String
getOutFile Config
conf String
filename) ->
                        Annote -> Name -> m ()
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Annote -> Name -> m ()
notCertified (String -> Annote
filePath String
filename)
                              (Name -> m ()) -> Name -> m ()
forall a b. (a -> b) -> a -> b
$ Name
"the certify artifact (" Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
rwcFile
                              Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
") would overwrite the requested output file; pass a different -o to certify this compilation."
                  Language
Haskell -> do
                        Name -> m ()
forall (m :: * -> *). MonadIO m => Name -> m ()
verb (Name -> m ()) -> Name -> m ()
forall a b. (a -> b) -> a -> b
$ Name
"certify: writing the final (backend-consumed) Hyle IR to file: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
rwcFile
                        IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ do
                              String -> Name -> IO ()
T.writeFile (String
rwcFile String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
".tmp") (Name -> IO ()) -> Name -> IO ()
forall a b. (a -> b) -> a -> b
$ Program -> Name
renderCore Program
p11
                              String -> String -> IO ()
renameFile (String
rwcFile String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
".tmp") String
rwcFile
                        IO (Either Name String) -> m (Either Name String)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (Either Name String)
findRwv m (Either Name String) -> (Either Name String -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
                              Left Name
why  -> Annote -> Name -> m ()
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Annote -> Name -> m ()
notCertified (String -> Annote
filePath String
filename) Name
why
                              Right String
rwv -> do
                                    Name -> m ()
forall (m :: * -> *). MonadIO m => Name -> m ()
verb (Name -> m ()) -> Name -> m ()
forall a b. (a -> b) -> a -> b
$ Name
"certify: running the validator: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
rwv Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
" " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
synFile Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
" " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
rwcFile
                                    (status, detail) <- IO (Name, Name) -> m (Name, Name)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Name, Name) -> m (Name, Name))
-> IO (Name, Name) -> m (Name, Name)
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> IO (Name, Name)
runValidator String
rwv String
synFile String
rwcFile
                                    case status of
                                          Name
"validated" -> IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Name -> IO ()
T.putStrLn
                                                (Name -> IO ()) -> Name -> IO ()
forall a b. (a -> b) -> a -> b
$ Name
"certify: VALIDATED: the compiled device (" Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
rwcFile
                                                Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
") implements the Synolon machine (" Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
synFile Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
")."
                                          Name
_ -> Annote -> Name -> m ()
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Annote -> Name -> m ()
notCertified (String -> Annote
filePath String
filename)
                                                (Name -> m ()) -> Name -> m ()
forall a b. (a -> b) -> a -> b
$ Name -> Name
Text.toUpper Name
status Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
": " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
detail
                                                Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
" (artifacts: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
synFile Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
", " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
rwcFile Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
")."
                  -- Under --from-core the front-end passes never run, so
                  -- there is no Synolon IR to validate against.
                  Language
_       -> Annote -> Name -> m ()
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Annote -> Name -> m ()
notCertified Annote
noAnn Name
"nothing to certify (certification requires compiling from Haskell source; no Synolon IR exists under --from-core)."

            -- | Refuse up front (in required mode) an output naming under
            --   which certification would corrupt its own artifacts: the
            --   pass-8 .syn dump and the final .rwc are written beside the
            --   output, so the requested output must not claim either name
            --   (modulo case, for case-insensitive filesystems). Under
            --   --certify=warn the compilation proceeds and the collision
            --   surfaces as a not-validated status.
            checkCertifyPaths :: (MonadError AstError m, MonadIO m) => m ()
            checkCertifyPaths :: forall (m :: * -> *). (MonadError AstError m, MonadIO m) => m ()
checkCertifyPaths = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
certifyOn Bool -> Bool -> Bool
&& Config
confConfig -> Getting Certify Config Certify -> Certify
forall s a. s -> Getting a s a -> a
^.Getting Certify Config Certify
Lens' Config Certify
Config.certify Certify -> Certify -> Bool
forall a. Eq a => a -> a -> Bool
== Certify
CertifyRequired Bool -> Bool -> Bool
&& Config
confConfig -> Getting Language Config Language -> Language
forall s a. s -> Getting a s a -> a
^.Getting Language Config Language
Lens' Config Language
source Language -> Language -> Bool
forall a. Eq a => a -> a -> Bool
== Language
Haskell) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
                  let fout :: String
fout = Config -> String -> String
getOutFile Config
conf String
filename
                  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String -> String -> Bool
samePath String
fout String
synFile) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> Name -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Name -> m a
failAt (String -> Annote
filePath String
filename)
                        (Name -> m ()) -> Name -> m ()
forall a b. (a -> b) -> a -> b
$ Name
"certify: the requested output file (" Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
fout
                        Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
") collides with the certify artifact (" Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
synFile Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
"); pass a different -o."
                  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config
confConfig -> Getting Language Config Language -> Language
forall s a. s -> Getting a s a -> a
^.Getting Language Config Language
Lens' Config Language
target Language -> Language -> Bool
forall a. Eq a => a -> a -> Bool
/= Language
RWCore Bool -> Bool -> Bool
&& String -> String -> Bool
samePath String
fout String
rwcFile) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> Name -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Name -> m a
failAt (String -> Annote
filePath String
filename)
                        (Name -> m ()) -> Name -> m ()
forall a b. (a -> b) -> a -> b
$ Name
"certify: the requested output file (" Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
fout
                        Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
") collides with the certify artifact (" Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
rwcFile Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
"); pass a different -o."

            -- | A non-validated certification outcome: fatal when
            --   certification is required (the default); an unsuppressible
            --   status line under --certify=warn, printed directly to
            --   stderr -- an explicitly requested best-effort report must
            --   not vanish under -w, and -Werror does not govern it.
            notCertified :: (MonadError AstError m, MonadIO m) => Annote -> Text -> m ()
            notCertified :: forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Annote -> Name -> m ()
notCertified Annote
an Name
msg
                  | Config
confConfig -> Getting Certify Config Certify -> Certify
forall s a. s -> Getting a s a -> a
^.Getting Certify Config Certify
Lens' Config Certify
Config.certify Certify -> Certify -> Bool
forall a. Eq a => a -> a -> Bool
== Certify
CertifyRequired = Annote -> Name -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Name -> m a
failAt Annote
an (Name -> m ()) -> Name -> m ()
forall a b. (a -> b) -> a -> b
$ Name
"certify: not validated: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
msg
                  | Bool
otherwise = IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Handle -> Name -> IO ()
T.hPutStrLn Handle
stderr (Name -> IO ()) -> Name -> IO ()
forall a b. (a -> b) -> a -> b
$ Name
"certify: not validated: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
msg

            certifyOn :: Bool
            certifyOn :: Bool
certifyOn = Config
confConfig -> Getting Certify Config Certify -> Certify
forall s a. s -> Getting a s a -> a
^.Getting Certify Config Certify
Lens' Config Certify
Config.certify Certify -> Certify -> Bool
forall a. Eq a => a -> a -> Bool
/= Certify
CertifyOff

            samePath :: FilePath -> FilePath -> Bool
            samePath :: String -> String -> Bool
samePath String
a String
b = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
b

            fout' :: String
fout'   = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
filename (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ Config
confConfig
-> Getting (Maybe String) Config (Maybe String) -> Maybe String
forall s a. s -> Getting a s a -> a
^.Getting (Maybe String) Config (Maybe String)
Lens' Config (Maybe String)
Config.outFile
            synFile :: String
synFile = Config -> String -> String
Config.synolonFile Config
conf String
filename
            rwcFile :: String
rwcFile = String
fout' String -> String -> String
-<.> String
"rwc"

            verb :: MonadIO m => Text -> m ()
            verb :: forall (m :: * -> *). MonadIO m => Name -> m ()
verb = Config -> Name -> m ()
forall (m :: * -> *). MonadIO m => Config -> Name -> m ()
pDebug Config
conf

-- | Strip all provenance from the program's annotations (a generic sweep;
--   Hyle types derive Data) so the printed .rwc carries no '--@' locator
--   lines.
scrubSpans :: Program -> Program
scrubSpans :: Program -> Program
scrubSpans = Program -> Program
forall d. Data d => d -> d
unAnn

-- | The verified Synolon-to-Hyle validator executable (built from verify/
--   with Lake; see doc/certify.md).
rwvExe :: String
rwvExe :: String
rwvExe = String
"rwv-cstep-validate"

-- | Locate the validator: RWC_RWV (which must name an executable file --
--   a broken override fails closed rather than falling through), then
--   next to the rwc executable, then the PATH. There is deliberately no
--   cwd-relative fallback: the selected executable is part of the trust
--   base, and rwc must never execute a binary planted in whatever
--   directory it happens to be invoked from.
findRwv :: IO (Either Text FilePath)
findRwv :: IO (Either Name String)
findRwv = String -> IO (Maybe String)
lookupEnv String
"RWC_RWV" IO (Maybe String)
-> (Maybe String -> IO (Either Name String))
-> IO (Either Name String)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
      Just String
r  -> String -> IO Bool
executableAt String
r IO Bool
-> (Bool -> IO (Either Name String)) -> IO (Either Name String)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
            Bool
True  -> Either Name String -> IO (Either Name String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Name String -> IO (Either Name String))
-> Either Name String -> IO (Either Name String)
forall a b. (a -> b) -> a -> b
$ String -> Either Name String
forall a b. b -> Either a b
Right String
r
            Bool
False -> Either Name String -> IO (Either Name String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Name String -> IO (Either Name String))
-> Either Name String -> IO (Either Name String)
forall a b. (a -> b) -> a -> b
$ Name -> Either Name String
forall a b. a -> Either a b
Left (Name -> Either Name String) -> Name -> Either Name String
forall a b. (a -> b) -> a -> b
$ Name
"RWC_RWV is set to " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
r Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
", which does not exist or is not executable."
      Maybe String
Nothing -> do
            cand <- (String -> String -> String
</> String
rwvExe) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
takeDirectory (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String
getExecutablePath
            executableAt cand >>= \ case
                  Bool
True  -> Either Name String -> IO (Either Name String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Name String -> IO (Either Name String))
-> Either Name String -> IO (Either Name String)
forall a b. (a -> b) -> a -> b
$ String -> Either Name String
forall a b. b -> Either a b
Right String
cand
                  Bool
False -> String -> IO (Maybe String)
findExecutable String
rwvExe IO (Maybe String)
-> (Maybe String -> IO (Either Name String))
-> IO (Either Name String)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
                        Just String
r  -> Either Name String -> IO (Either Name String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Name String -> IO (Either Name String))
-> Either Name String -> IO (Either Name String)
forall a b. (a -> b) -> a -> b
$ String -> Either Name String
forall a b. b -> Either a b
Right String
r
                        Maybe String
Nothing -> Either Name String -> IO (Either Name String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Name String -> IO (Either Name String))
-> Either Name String -> IO (Either Name String)
forall a b. (a -> b) -> a -> b
$ Name -> Either Name String
forall a b. a -> Either a b
Left (Name -> Either Name String) -> Name -> Either Name String
forall a b. (a -> b) -> a -> b
$ Name
"the validator (" Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
rwvExe
                              Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
") was not found next to rwc or on the PATH; build it with"
                              Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
" 'cd verify && lake build " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
rwvExe Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
"' in a ReWire checkout"
                              Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
" and install it next to rwc or on the PATH (or set RWC_RWV to its location)."
      where executableAt :: FilePath -> IO Bool
            executableAt :: String -> IO Bool
executableAt String
f = String -> IO Bool
doesFileExist String
f IO Bool -> (Bool -> IO Bool) -> IO Bool
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
                  Bool
False -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
                  Bool
True  -> Permissions -> Bool
executable (Permissions -> Bool) -> IO Permissions -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO Permissions
getPermissions String
f

-- | The validator's protocol-2 response: exactly one JSON object on
--   stdout identifying the tool, verdict, echoed nonce, and the SHA-256
--   of the artifact bytes the validator actually read.
data RwvResponse = RwvResponse
      { RwvResponse -> Name
rwvTool     :: !Text
      , RwvResponse -> Int
rwvProtocol :: !Int
      , RwvResponse -> Name
rwvStatus   :: !Text
      , RwvResponse -> Name
rwvDetail   :: !Text
      , RwvResponse -> Name
rwvNonce    :: !Text
      , RwvResponse -> Name
rwvSource   :: !Text
      , RwvResponse -> Name
rwvTarget   :: !Text
      }

instance FromJSON RwvResponse where
      parseJSON :: Value -> Parser RwvResponse
parseJSON = String
-> (Object -> Parser RwvResponse) -> Value -> Parser RwvResponse
forall a. String -> (Object -> Parser a) -> Value -> Parser a
withObject String
"rwv response" ((Object -> Parser RwvResponse) -> Value -> Parser RwvResponse)
-> (Object -> Parser RwvResponse) -> Value -> Parser RwvResponse
forall a b. (a -> b) -> a -> b
$ \ Object
o -> Name -> Int -> Name -> Name -> Name -> Name -> Name -> RwvResponse
RwvResponse
            (Name
 -> Int -> Name -> Name -> Name -> Name -> Name -> RwvResponse)
-> Parser Name
-> Parser
     (Int -> Name -> Name -> Name -> Name -> Name -> RwvResponse)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
o Object -> Key -> Parser Name
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"tool"
            Parser (Int -> Name -> Name -> Name -> Name -> Name -> RwvResponse)
-> Parser Int
-> Parser (Name -> Name -> Name -> Name -> Name -> RwvResponse)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
o Object -> Key -> Parser Int
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"protocol"
            Parser (Name -> Name -> Name -> Name -> Name -> RwvResponse)
-> Parser Name
-> Parser (Name -> Name -> Name -> Name -> RwvResponse)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
o Object -> Key -> Parser Name
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"status"
            Parser (Name -> Name -> Name -> Name -> RwvResponse)
-> Parser Name -> Parser (Name -> Name -> Name -> RwvResponse)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
o Object -> Key -> Parser Name
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"detail"
            Parser (Name -> Name -> Name -> RwvResponse)
-> Parser Name -> Parser (Name -> Name -> RwvResponse)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
o Object -> Key -> Parser Name
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"nonce"
            Parser (Name -> Name -> RwvResponse)
-> Parser Name -> Parser (Name -> RwvResponse)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Object
o Object -> Key -> Parser Value
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"source" Parser Value -> (Value -> Parser Name) -> Parser Name
forall a b. Parser a -> (a -> Parser b) -> Parser b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> (Object -> Parser Name) -> Value -> Parser Name
forall a. String -> (Object -> Parser a) -> Value -> Parser a
withObject String
"artifact" (Object -> Key -> Parser Name
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"sha256"))
            Parser (Name -> RwvResponse) -> Parser Name -> Parser RwvResponse
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Object
o Object -> Key -> Parser Value
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"target" Parser Value -> (Value -> Parser Name) -> Parser Name
forall a b. Parser a -> (a -> Parser b) -> Parser b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> (Object -> Parser Name) -> Value -> Parser Name
forall a. String -> (Object -> Parser a) -> Value -> Parser a
withObject String
"artifact" (Object -> Key -> Parser Name
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"sha256"))

-- | One validator invocation, fail-closed: the result is
--   (status, detail), where status is "validated" only if the process
--   exited successfully AND printed exactly one well-formed protocol-2
--   response whose nonce echoes this invocation and whose artifact
--   hashes match the bytes we hashed independently. Spawn failures,
--   timeouts, nonzero exits, malformed or ambiguous output, and
--   mismatched identities all classify as "error".
runValidator :: FilePath -> FilePath -> FilePath -> IO (Text, Text)
runValidator :: String -> String -> String -> IO (Name, Name)
runValidator String
rwv String
synFile String
rwcFile = do
      synHash <- ByteString -> Name
hashHex (ByteString -> Name) -> IO ByteString -> IO Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO ByteString
BS.readFile String
synFile
      rwcHash <- hashHex <$> BS.readFile rwcFile
      nonce   <- (\ Word64
t -> ByteString -> Name
hashHex (ByteString -> Name) -> ByteString -> Name
forall a b. (a -> b) -> a -> b
$ Name -> ByteString
encodeUtf8 (Name -> ByteString) -> Name -> ByteString
forall a b. (a -> b) -> a -> b
$ Name
synHash Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
rwcHash Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack (Word64 -> String
forall a. Show a => a -> String
show Word64
t)) <$> getMonotonicTimeNSec
      r       <- try $ timeout (validatorTimeoutSecs * 1000000)
            $ readCreateProcessWithExitCode (proc rwv [synFile, rwcFile, "--protocol=2", "--nonce=" <> unpack nonce]) ""
      pure $ case r of
            Left (IOException
ex :: IOException)     -> (Name
"error", Name
"could not run the validator: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack (IOException -> String
forall a. Show a => a -> String
show IOException
ex))
            Right Maybe (ExitCode, String, String)
Nothing                -> (Name
"error", Name
"the validator timed out after " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Int -> Name
forall a. TextShow a => a -> Name
showt Int
validatorTimeoutSecs Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
" seconds")
            Right (Just (ExitCode
code, String
out, String
_))  -> case (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
out of
                  [String
l] -> case ByteString -> Either String RwvResponse
forall a. FromJSON a => ByteString -> Either String a
eitherDecodeStrict (ByteString -> Either String RwvResponse)
-> ByteString -> Either String RwvResponse
forall a b. (a -> b) -> a -> b
$ Name -> ByteString
encodeUtf8 (Name -> ByteString) -> Name -> ByteString
forall a b. (a -> b) -> a -> b
$ String -> Name
pack String
l of
                        Left String
perr -> (Name
"error", Name
"malformed validator response: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack String
perr)
                        Right RwvResponse
resp
                              | RwvResponse -> Name
rwvTool RwvResponse
resp Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
"rwv-cstep-validate" -> (Name
"error", Name
"the response names an unexpected tool: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> RwvResponse -> Name
rwvTool RwvResponse
resp)
                              | RwvResponse -> Int
rwvProtocol RwvResponse
resp Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
2                -> (Name
"error", Name
"the response speaks an unexpected protocol version: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Int -> Name
forall a. TextShow a => a -> Name
showt (RwvResponse -> Int
rwvProtocol RwvResponse
resp))
                              | RwvResponse -> Name
rwvNonce RwvResponse
resp Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
nonce               -> (Name
"error", Name
"the response does not echo this invocation's nonce")
                              | RwvResponse -> Name
rwvSource RwvResponse
resp Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
synHash            -> (Name
"error", Name
"the response's source hash does not match the artifact bytes")
                              | RwvResponse -> Name
rwvTarget RwvResponse
resp Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
rwcHash            -> (Name
"error", Name
"the response's target hash does not match the artifact bytes")
                              | RwvResponse -> Name
rwvStatus RwvResponse
resp Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
"validated", ExitCode
code ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
/= ExitCode
ExitSuccess -> (Name
"error", Name
"the validator reported validated but exited nonzero")
                              | RwvResponse -> Name
rwvStatus RwvResponse
resp Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
"validated", ExitCode
code ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
== ExitCode
ExitSuccess -> (Name
"error", Name
"the validator exited successfully without reporting validated")
                              | RwvResponse -> Name
rwvStatus RwvResponse
resp Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name
"validated", Name
"rejected", Name
"unsupported", Name
"error"] -> (RwvResponse -> Name
rwvStatus RwvResponse
resp, RwvResponse -> Name
rwvDetail RwvResponse
resp)
                              | Bool
otherwise -> (Name
"error", Name
"unknown validator status: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> RwvResponse -> Name
rwvStatus RwvResponse
resp)
                  []  -> (Name
"error", Name
"the validator produced no response (exit: " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
pack (ExitCode -> String
forall a. Show a => a -> String
show ExitCode
code) Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
")")
                  [String]
_   -> (Name
"error", Name
"the validator produced multiple responses")

-- | How long one validator run may take. The corpus giants complete in
--   well under a minute; ten minutes is a generous ceiling.
validatorTimeoutSecs :: Int
validatorTimeoutSecs :: Int
validatorTimeoutSecs = Int
600

-- | The number of cycles to interpret/simulate: the explicit --cycles value if
--   the user gave one, otherwise the larger of 10 or the number of inputs
--   supplied in the inputs file.
effectiveCycles :: Config -> [Ins] -> Natural
effectiveCycles :: Config -> [Ins] -> Natural
effectiveCycles Config
conf [Ins]
ips = Natural -> Maybe Natural -> Natural
forall a. a -> Maybe a -> a
fromMaybe (Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
max Natural
10 (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Ins] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ins]
ips))) (Config
confConfig
-> Getting (Maybe Natural) Config (Maybe Natural) -> Maybe Natural
forall s a. s -> Getting a s a -> a
^.Getting (Maybe Natural) Config (Maybe Natural)
Lens' Config (Maybe Natural)
cycles)

-- | Replicates/truncates inputs to fill up exactly ncycles cycles.
boundInput :: Natural -> [Ins] -> [Ins]
boundInput :: Natural -> [Ins] -> [Ins]
boundInput Natural
ncycles [Ins]
ips = ([Ins] -> Ins -> [Ins]) -> [Ins] -> [Ins] -> [Ins]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ [Ins]
ms Ins
m -> [Ins]
ms [Ins] -> [Ins] -> [Ins]
forall a. Semigroup a => a -> a -> a
<> [Ins -> Ins -> Ins
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
Map.union Ins
m ([Ins] -> Ins
forall a. Monoid a => [a] -> a
last' [Ins]
ms)]) [] [Ins]
ips'
      where ips' :: [Ins]
            ips' :: [Ins]
ips' = Int -> [Ins] -> [Ins]
forall a. Int -> [a] -> [a]
take (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
ncycles) ([Ins] -> [Ins]) -> [Ins] -> [Ins]
forall a b. (a -> b) -> a -> b
$ [Ins]
ips [Ins] -> [Ins] -> [Ins]
forall a. Semigroup a => a -> a -> a
<> Ins -> [Ins]
forall a. a -> [a]
repeat ([Ins] -> Ins
forall a. Monoid a => [a] -> a
last' [Ins]
ips)

lastMaybe :: [a] -> Maybe a
lastMaybe :: forall a. [a] -> Maybe a
lastMaybe = \ case
      []       -> Maybe a
forall a. Maybe a
Nothing
      [a
a]      -> a -> Maybe a
forall a. a -> Maybe a
Just a
a
      (a
_ : [a]
as) -> [a] -> Maybe a
forall a. [a] -> Maybe a
lastMaybe [a]
as

last' :: Monoid a => [a] -> a
last' :: forall a. Monoid a => [a] -> a
last' = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
forall a. Monoid a => a
mempty (Maybe a -> a) -> ([a] -> Maybe a) -> [a] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Maybe a
forall a. [a] -> Maybe a
lastMaybe