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.

Sign up for GitHub

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

Update fourmolu to set column limit #199

Draft
wants to merge 5 commits into
base: master
Choose a base branch
from
Draft

Update fourmolu to set column limit #199

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
8d38d4f
Add `column-limit: 100` to `fourmolu.yaml`
langfield Mar 31, 2023
d80f8d7
Use `haddock-style: single-line` in `fourmolu.yaml`
langfield Mar 31, 2023
3058a9f
Use `function-arrows: leading` in `fourmolu.yaml`
langfield Mar 31, 2023
3e389b5
Remove unused `fourmolu` config field
langfield Mar 31, 2023
469ba58
Don't half-indent `where` keywords
langfield Mar 31, 2023
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
126 changes: 62 additions & 64 deletions app/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,13 +62,12 @@ compatibleHorusCompileVersionLower = makeVersion [0, 0, 6, 8]
compatibleHorusCompileVersionHigher :: Version
compatibleHorusCompileVersionHigher = makeVersion [0, 0, 7]

{- | The main entrypoint of everything that happens in our monad stack.
The contract is a 1-1 representation of the data in the compiled JSON file.
The contract is then used to create a 'ContractInfo' which is a more
convenient representation of the contract.
We run `solveContract`, which is the entrypoint into the *rest* of the
program, and gather the results for pretty-printing.
-}
-- | The main entrypoint of everything that happens in our monad stack.
-- The contract is a 1-1 representation of the data in the compiled JSON file.
-- The contract is then used to create a 'ContractInfo' which is a more
-- convenient representation of the contract.
-- We run `solveContract`, which is the entrypoint into the *rest* of the
-- program, and gather the results for pretty-printing.
main' :: Arguments -> FilePath -> FilePath -> EIO ()
main' Arguments{..} filename specFileName = do
contract <- eioDecodeFileStrict filename specFileName <&> cdSpecs %~ (<> stdSpecs)
Expand All @@ -81,30 +80,30 @@ main' Arguments{..} filename specFileName = do
TextIO.putStrLn (ppSolvingInfo si)
let unknowns = [res | res@(Timeout{}) <- map si_result infos]
unless (null unknowns) $ liftIO (TextIO.putStrLn hint')
where
hint' = "\ESC[33m" <> (T.strip . T.unlines . map ("hint: " <>) . T.lines) hint <> "\ESC[0m"
guardVersion :: ContractDefinition -> EIO ()
guardVersion cd = do
compilerVersion <- case [ x
| x@(_, lst) <- readP_to_S parseVersion (cd_version cd)
, null lst
] of
[(v, [])] -> pure v
_ -> fail $ "Wrong version format: " <> cd_version cd
when
( compilerVersion < compatibleHorusCompileVersionLower
|| compilerVersion >= compatibleHorusCompileVersionHigher
)
. fail
. concat
$ [ "The *.json on input has been compiled with an incompatible version of Horus-compile.\nExpected: "
, ">="
, showVersion compatibleHorusCompileVersionLower
, ", <"
, showVersion compatibleHorusCompileVersionHigher
, " but got: "
, showVersion compilerVersion
]
where
hint' = "\ESC[33m" <> (T.strip . T.unlines . map ("hint: " <>) . T.lines) hint <> "\ESC[0m"
guardVersion :: ContractDefinition -> EIO ()
guardVersion cd = do
compilerVersion <- case [ x
| x@(_, lst) <- readP_to_S parseVersion (cd_version cd)
, null lst
] of
[(v, [])] -> pure v
_ -> fail $ "Wrong version format: " <> cd_version cd
when
( compilerVersion < compatibleHorusCompileVersionLower
|| compilerVersion >= compatibleHorusCompileVersionHigher
)
. fail
. concat
$ [ "The *.json on input has been compiled with an incompatible version of Horus-compile.\nExpected: "
, ">="
, showVersion compatibleHorusCompileVersionLower
, ", <"
, showVersion compatibleHorusCompileVersionHigher
, " but got: "
, showVersion compilerVersion
]

eioDecodeFileStrict :: FromJSON a => FilePath -> FilePath -> EIO a
eioDecodeFileStrict contractFile specFile = do
Expand All @@ -122,17 +121,16 @@ eioDecodeFileStrict contractFile specFile = do
ppSolvingInfo :: SolvingInfo -> Text
ppSolvingInfo SolvingInfo{..} =
si_moduleName <> inlinedIndicator <> "\n" <> tShow si_result <> "\n"
where
inlinedIndicator = if si_inlinable then " [inlined]" else ""
where
inlinedIndicator = if si_inlinable then " [inlined]" else ""

{- | Main entrypoint of the program.
Cases
=====
1. No arguments are passed. In this case, we print the help message.
2. The `--version` flag is passed. In this case, we print the version number.
3. No file is passed. In this case, we print an error.
4. A file is passed. In this case, we run `main'`.
-}
-- | Main entrypoint of the program.
-- Cases
-- =====
-- 1. No arguments are passed. In this case, we print the help message.
-- 2. The `--version` flag is passed. In this case, we print the version number.
-- 3. No file is passed. In this case, we print an error.
-- 4. A file is passed. In this case, we run `main'`.
main :: IO ()
main = do
TextIO.putStrLn issuesMsg'
Expand All @@ -153,26 +151,26 @@ main = do
(_, Nothing) -> putStrLn "Missing specification JSON file. Use --help for more information."
(Just filename, Just specFileName) -> do
runExceptT (main' arguments filename specFileName) >>= either (fail . T.unpack) pure
where
issuesMsg' =
"\ESC[33m" <> (T.strip . T.unlines . map ("Warning: " <>) . T.lines) issuesMsg <> "\ESC[0m\n"
opts =
info
(argParser <**> helper)
( fullDesc
<> progDescDoc
( Just $
text "Verifies "
<> text (T.unpack fileArgument)
<> text " (a JSON contract compiled with horus-compile) with the specification file "
<> text (T.unpack specFileArgument)
<> text " provided by horus-compile \n\n"
<> text "Example using solver cvc5 (default):\n"
<> text " $ horus-check a.json spec.json\n\n"
<> text "Example using solver mathsat:\n"
<> text " $ horus-check -s mathsat a.json spec.json\n\n"
<> text "Example using solvers z3, mathsat:\n"
<> text " $ horus-check -s z3 -s mathsat a.json spec.json\n"
)
<> header "horus-check: an SMT-based checker for StarkNet contracts"
)
where
issuesMsg' =
"\ESC[33m" <> (T.strip . T.unlines . map ("Warning: " <>) . T.lines) issuesMsg <> "\ESC[0m\n"
opts =
info
(argParser <**> helper)
( fullDesc
<> progDescDoc
( Just $
text "Verifies "
<> text (T.unpack fileArgument)
<> text " (a JSON contract compiled with horus-compile) with the specification file "
<> text (T.unpack specFileArgument)
<> text " provided by horus-compile \n\n"
<> text "Example using solver cvc5 (default):\n"
<> text " $ horus-check a.json spec.json\n\n"
<> text "Example using solver mathsat:\n"
<> text " $ horus-check -s mathsat a.json spec.json\n\n"
<> text "Example using solvers z3, mathsat:\n"
<> text " $ horus-check -s z3 -s mathsat a.json spec.json\n"
)
<> header "horus-check: an SMT-based checker for StarkNet contracts"
)
20 changes: 11 additions & 9 deletions fourmolu.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,12 @@
indentation: 2
comma-style: leading # for lists, tuples etc. - can also be 'trailing'
import-export-comma-style: leading # for module import export lists - can also be 'trailing'
record-brace-space: false # rec {x = 1} vs. rec{x = 1}
indent-wheres: false # 'false' means save space by only half-indenting the 'where' keyword
diff-friendly-import-export: false # 'false' uses Ormolu-style lists
respectful: true # don't be too opinionated about newlines etc.
haddock-style: multi-line # '--' vs. '{-'
newlines-between-decls: 1 # number of newlines between top-level declarations
fixities: [] # fixity information, see the section about fixities below.
comma-style: leading # for lists, tuples etc. - can also be 'trailing'
import-export-style: leading # for module import export lists - can also be 'trailing'
record-brace-space: false # rec {x = 1} vs. rec{x = 1}
indent-wheres: true # 'false' means save space by only half-indenting the 'where' keyword
respectful: true # don't be too opinionated about newlines etc.
haddock-style: single-line # '--' vs. '{-'
newlines-between-decls: 1 # number of newlines between top-level declarations
fixities: [] # fixity information, see the section about fixities below.
column-limit: 100
function-arrows: leading
single-constraint-parens: never
13 changes: 11 additions & 2 deletions src/Horus/Arguments.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,14 @@ import Data.Text (Text, unpack)
import Options.Applicative

import Horus.Global (Config (..))
import Horus.Preprocessor.Solvers (MultiSolver (..), SingleSolver, SolverSettings (..), cvc5, mathsat, z3)
import Horus.Preprocessor.Solvers
( MultiSolver (..)
, SingleSolver
, SolverSettings (..)
, cvc5
, mathsat
, z3
)

data Arguments = Arguments
{ arg_fileName :: Maybe FilePath
Expand Down Expand Up @@ -55,7 +62,9 @@ singleSolverParser =
( long "solver"
<> short 's'
<> metavar "SOLVER"
<> help ("Solver to check the resulting smt queries (options: " <> intercalate ", " singleSolverNames <> ").")
<> help
( "Solver to check the resulting smt queries (options: " <> intercalate ", " singleSolverNames <> ")."
)
<> completeWith singleSolverNames
)

Expand Down
171 changes: 84 additions & 87 deletions src/Horus/CFGBuild.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,14 +152,13 @@ getSvarSpecs = liftF' (GetSvarSpecs id)
getVerts :: Label -> CFGBuildL [Vertex]
getVerts l = liftF' (GetVerts l id)

{- | Salient vertices can be thought of as 'main' vertices of the CFG, meaning that
if one wants to reason about flow control of the program, one should query salient vertices.

Certain program transformations and optimisations can add various additional nodes into the CFG,
whose primary purpose is not to reason about control flow.

It is enforced that for any one PC, one can add at most a single salient vertex.
-}
-- | Salient vertices can be thought of as 'main' vertices of the CFG, meaning that
-- if one wants to reason about flow control of the program, one should query salient vertices.
--
-- Certain program transformations and optimisations can add various additional nodes into the CFG,
-- whose primary purpose is not to reason about control flow.
--
-- It is enforced that for any one PC, one can add at most a single salient vertex.
getSalientVertex :: Label -> CFGBuildL Vertex
getSalientVertex l = do
verts <- filter (not . isPreCheckingVertex) <$> getVerts l
Expand Down Expand Up @@ -200,31 +199,29 @@ buildFrame inlinables rows prog = do
segmentsWithVerts <- for segments $ \s -> addVertex (segmentLabel s) <&> (s,)
for_ segmentsWithVerts . uncurry $ addArcsFrom inlinables prog rows

{- | A simple procedure for splitting a stream of instructions into nonempty Segments based
on program labels, which more-or-less correspond with changes in control flow in the program.
We thus obtain linear segments of instructions without control flow.
-}
-- | A simple procedure for splitting a stream of instructions into nonempty Segments based
-- on program labels, which more-or-less correspond with changes in control flow in the program.
-- We thus obtain linear segments of instructions without control flow.
breakIntoSegments :: [Label] -> [LabeledInst] -> [Segment]
breakIntoSegments _ [] = []
breakIntoSegments ls_ (i_ : is_) = coerce (go [] (i_ :| []) ls_ is_)
where
go gAcc lAcc [] rest = reverse (NonEmpty.reverse lAcc `appendList` rest : gAcc)
go gAcc lAcc (_ : _) [] = reverse (NonEmpty.reverse lAcc : gAcc)
go gAcc lAcc (l : ls) (i@(pc, _) : is)
| l < pc = go gAcc lAcc ls (i : is)
| l == pc = go (NonEmpty.reverse lAcc : gAcc) (i :| []) ls is
| otherwise = go gAcc (i NonEmpty.<| lAcc) (l : ls) is
where
go gAcc lAcc [] rest = reverse (NonEmpty.reverse lAcc `appendList` rest : gAcc)
go gAcc lAcc (_ : _) [] = reverse (NonEmpty.reverse lAcc : gAcc)
go gAcc lAcc (l : ls) (i@(pc, _) : is)
| l < pc = go gAcc lAcc ls (i : is)
| l == pc = go (NonEmpty.reverse lAcc : gAcc) (i :| []) ls is
| otherwise = go gAcc (i NonEmpty.<| lAcc) (l : ls) is

addArc' :: Vertex -> Vertex -> [LabeledInst] -> CFGBuildL ()
addArc' lFrom lTo insts = addArc lFrom lTo insts ACNone Nothing

{- | This function adds arcs (edges) into the CFG and labels them with instructions that are
to be executed when traversing from one vertex to another.

Currently, we do not have an optimisation post-processing pass in Horus and we therefore
also include an optimisation here that generates an extra vertex in order to implement
separate checking of preconditions for abstracted functions.
-}
-- | This function adds arcs (edges) into the CFG and labels them with instructions that are
-- to be executed when traversing from one vertex to another.
--
-- Currently, we do not have an optimisation post-processing pass in Horus and we therefore
-- also include an optimisation here that generates an extra vertex in order to implement
-- separate checking of preconditions for abstracted functions.
addArcsFrom :: Set ScopedFunction -> Program -> [LabeledInst] -> Segment -> Vertex -> CFGBuildL ()
addArcsFrom inlinables prog rows seg@(Segment s) vFrom
| Call <- i_opCode endInst =
Expand Down Expand Up @@ -255,67 +252,67 @@ addArcsFrom inlinables prog rows seg@(Segment s) vFrom
| otherwise = do
lTo <- getSalientVertex $ nextSegmentLabel seg
addArc' vFrom lTo insts
where
lInst@(endPc, endInst) = NonEmpty.last s
insts = segmentInsts seg
inlinableLabels = Set.map sf_pc inlinables

callee = uncheckedScopedFOfPc (p_identifiers prog) (uncheckedCallDestination lInst)

beginInlining = do
salientCalleeV <- getSalientVertex (sf_pc callee)
addArc vFrom salientCalleeV insts ACNone . Just $ ArcCall endPc (sf_pc callee)

optimiseCheckingOfPre = do
-- Suppose F calls G where G has a precondition. We synthesize an extra module
-- Pre(F) -> Pre(G) to check whether Pre(G) holds. The standard module for F
-- is then Pre(F) -> Post(F) (conceptually, unless there's a split in the middle, etc.),
-- in which Pre(G) is assumed to hold at the PC of the G call site, as it will have
-- been checked by the module induced by the ghost vertex.
ghostV <- addOptimisingVertex (nextSegmentLabel seg) callee
pre <- maybe (mkPre Expr.True) mkPre . fs'_pre <$> getFuncSpec callee

-- Important note on the way we deal with logical variables. These are @declare-d and
-- their values can be bound in preconditions. They generate existentials which only occur
-- in our models here and require special treatment, in addition to being somewhat
-- difficult for SMT checkers to deal with.

-- First note that these preconditions now become optimising-module postconditions.
-- We existentially quantify all logical variables present in the expression, thus in the
-- following example:
-- func foo:
-- call bar // where bar refers to $my_logical_var
-- We get an optimising module along the lines of:
-- Pre(foo) -> Pre(bar) where Pre(bar) contains \exists my_logical_var, ...
-- We can then check whether this instantiation exists in the optimising module exclusively.
-- The module that then considers that pre holds as a fact now has the luxury of not having
-- to deal with existential quantifiers, as it can simply 'declare' them as free variables.
addAssertion ghostV $ quantifyEx pre
addArc' vFrom ghostV insts

abstractOver = do
salientLinearV <- getSalientVertex (nextSegmentLabel seg)
addArc' vFrom salientLinearV insts
svarSpecs <- getSvarSpecs
when (sf_scopedName callee `Set.notMember` svarSpecs) optimiseCheckingOfPre

addRetArc :: Label -> CFGBuildL ()
addRetArc pc = do
retV <- getSalientVertex endPc
pastRet <- getSalientVertex pc
addArc retV pastRet [(endPc, endInst)] ACNone $ Just ArcRet

addRetArcs :: Label -> CFGBuildL ()
addRetArcs owner
| owner `Set.notMember` inlinableLabels = pure ()
| otherwise = forM_ returnAddrs addRetArc
where
returnAddrs = map (`moveLabel` sizeOfCall) (callersOf rows owner)

quantifyEx :: (AnnotationType, Expr 'TBool) -> (AnnotationType, Expr 'TBool)
quantifyEx = second $ \expr ->
let lvars = gatherLogicalVariables expr
in foldr Expr.ExistsFelt expr lvars
where
lInst@(endPc, endInst) = NonEmpty.last s
insts = segmentInsts seg
inlinableLabels = Set.map sf_pc inlinables

callee = uncheckedScopedFOfPc (p_identifiers prog) (uncheckedCallDestination lInst)

beginInlining = do
salientCalleeV <- getSalientVertex (sf_pc callee)
addArc vFrom salientCalleeV insts ACNone . Just $ ArcCall endPc (sf_pc callee)

optimiseCheckingOfPre = do
-- Suppose F calls G where G has a precondition. We synthesize an extra module
-- Pre(F) -> Pre(G) to check whether Pre(G) holds. The standard module for F
-- is then Pre(F) -> Post(F) (conceptually, unless there's a split in the middle, etc.),
-- in which Pre(G) is assumed to hold at the PC of the G call site, as it will have
-- been checked by the module induced by the ghost vertex.
ghostV <- addOptimisingVertex (nextSegmentLabel seg) callee
pre <- maybe (mkPre Expr.True) mkPre . fs'_pre <$> getFuncSpec callee

-- Important note on the way we deal with logical variables. These are @declare-d and
-- their values can be bound in preconditions. They generate existentials which only occur
-- in our models here and require special treatment, in addition to being somewhat
-- difficult for SMT checkers to deal with.

-- First note that these preconditions now become optimising-module postconditions.
-- We existentially quantify all logical variables present in the expression, thus in the
-- following example:
-- func foo:
-- call bar // where bar refers to $my_logical_var
-- We get an optimising module along the lines of:
-- Pre(foo) -> Pre(bar) where Pre(bar) contains \exists my_logical_var, ...
-- We can then check whether this instantiation exists in the optimising module exclusively.
-- The module that then considers that pre holds as a fact now has the luxury of not having
-- to deal with existential quantifiers, as it can simply 'declare' them as free variables.
addAssertion ghostV $ quantifyEx pre
addArc' vFrom ghostV insts

abstractOver = do
salientLinearV <- getSalientVertex (nextSegmentLabel seg)
addArc' vFrom salientLinearV insts
svarSpecs <- getSvarSpecs
when (sf_scopedName callee `Set.notMember` svarSpecs) optimiseCheckingOfPre

addRetArc :: Label -> CFGBuildL ()
addRetArc pc = do
retV <- getSalientVertex endPc
pastRet <- getSalientVertex pc
addArc retV pastRet [(endPc, endInst)] ACNone $ Just ArcRet

addRetArcs :: Label -> CFGBuildL ()
addRetArcs owner
| owner `Set.notMember` inlinableLabels = pure ()
| otherwise = forM_ returnAddrs addRetArc
where
returnAddrs = map (`moveLabel` sizeOfCall) (callersOf rows owner)

quantifyEx :: (AnnotationType, Expr 'TBool) -> (AnnotationType, Expr 'TBool)
quantifyEx = second $ \expr ->
let lvars = gatherLogicalVariables expr
in foldr Expr.ExistsFelt expr lvars

-- | This function labels appropriate vertices (at 'ret'urns) with their respective postconditions.
addAssertions :: Set ScopedFunction -> Identifiers -> CFGBuildL ()
Expand Down
Loading