GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-28 08:34:23 +03:00
Code Issues Projects Releases Wiki Activity

Unsupported functions (nonceAppEval) should error immediately.

Browse Source 
Original version was pushing error into generated TH, which was
generating the error statement into the SSA formula; this breaks
formula interpretation at compile time but hides the error.  Instead,
this changes it so that the error is thrown during TH evaluation.
This commit is contained in:
Kevin Quick 2018-03-10 10:04:03 -08:00
parent 1bceb8dc32
commit 0c67eddda8
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
macaw-semmc/src/Data/Macaw/SemMC/TH.hs
View File

@ -618,7 +618,7 @@ defaultNonceAppEvaluator bvi nonceApp =
_ -> fail ("Unexpected arguments to read_mem: " ++ showF args) _ -> fail ("Unexpected arguments to read_mem: " ++ showF args)
| otherwise -> | otherwise ->
case lookup fnName (A.locationFuncInterpretation (Proxy @arch)) of case lookup fnName (A.locationFuncInterpretation (Proxy @arch)) of
Nothing -> liftQ [| error ("Unsupported UF: " ++ show $(litE (StringL fnName))) |] Nothing -> error ("Unsupported UF: " ++ show fnName)
Just fi -> do Just fi -> do
-- args is an assignment that contains elts; we could just generate -- args is an assignment that contains elts; we could just generate
-- expressions that evaluate each one and then splat them into new names -- expressions that evaluate each one and then splat them into new names
@ -628,7 +628,7 @@ defaultNonceAppEvaluator bvi nonceApp =
argNames -> do argNames -> do
let call = appE (varE (A.exprInterpName fi)) $ foldr1 appE (map varE argNames) let call = appE (varE (A.exprInterpName fi)) $ foldr1 appE (map varE argNames)
liftQ [| O.extractValue ($(call)) |] liftQ [| O.extractValue ($(call)) |]
_ -> liftQ [| error "Unsupported NonceApp case" |] _ -> error "Unsupported NonceApp case"
-- | Parse the name of a memory read intrinsic and return the number of bytes -- | Parse the name of a memory read intrinsic and return the number of bytes
-- that it reads. For example -- that it reads. For example