Skip to content

Commit

Permalink
handle "finishInstruction" during preprocessing
Browse files Browse the repository at this point in the history
  • Loading branch information
danmatichuk committed Nov 1, 2023
1 parent ab7d111 commit 0a11013
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 7 deletions.
4 changes: 0 additions & 4 deletions lib/Language/ASL/Translation.hs
Original file line number Diff line number Diff line change
Expand Up @@ -344,9 +344,6 @@ translateStatement' stmt = do

_ -> throwTrace $ UnsupportedStmt stmt

finishInstruction :: Generator h s arch ret ()
finishInstruction = void $ translateFunctionCall (AS.VarName "finishInstruction") ([] :: [Void]) ConstraintNone

-- | Translate a @return@ from the current function, combining the
-- current value of all global variables into a struct and returning
-- it with the natural return value of the function.
Expand All @@ -365,7 +362,6 @@ returnWithGlobals retVal = do
forM_ postconds $ \(nm, condE) -> do
condA <- mkAtom condE
assertAtom condA Nothing $ "Postcondition: " <> nm
finishInstruction
returnWithGlobals' retVal

returnWithGlobals' :: ret ~ FuncReturn globalWrites tps
Expand Down
9 changes: 6 additions & 3 deletions lib/Language/ASL/Translation/Preprocess.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1048,10 +1048,13 @@ validateEncoding daEnc (SomeInstructionSignature iSig) = do
WT.BaseBVRepr nr -> return $ Const $ (T.unpack nm, NR.intValue nr)
_ -> E.throwError $ InvalidInstructionOperand (nm, tr)

finishInstruction :: [AS.Stmt]
finishInstruction = [AS.StmtCall (AS.VarName "finishInstruction") []]

wrapConditionCheck :: Bool -> [AS.Stmt] -> [AS.Stmt]
wrapConditionCheck cond body = case cond of
True -> [AS.StmtIf [((AS.ExprCall (AS.VarName "ConditionPassed") []), body)] (Just [])]
False -> body
True -> [AS.StmtIf [((AS.ExprCall (AS.VarName "ConditionPassed") []), (body ++ finishInstruction))] (Just finishInstruction)]
False -> body ++ finishInstruction

initGlobals :: [AS.Stmt]
initGlobals = [AS.StmtCall (AS.VarName "initGlobals") []]
Expand Down Expand Up @@ -1081,7 +1084,7 @@ computeInstructionSignature daEnc AS.Instruction{..} enc = do
labeledArgs <- getFunctionArgSig enc daEnc

computeSignatures instStmts
globalVars <- globalsOfStmts (AS.StmtCall (AS.VarName "finishInstruction") [] : instStmts)
globalVars <- globalsOfStmts instStmts

(globalReads, globalWrites) <- return $ unpackGVarRefs globalVars
missingGlobals <- liftM catMaybes $ forM globalReads $ \(varName, Some varTp) ->
Expand Down

0 comments on commit 0a11013

Please sign in to comment.