From 73c56f460915bade0a3fcc1a0841f3dd4021e964 Mon Sep 17 00:00:00 2001 From: zoep Date: Fri, 23 Aug 2024 18:58:23 +0300 Subject: [PATCH] WIP fresh addresses --- src/Act/HEVM.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/Act/HEVM.hs b/src/Act/HEVM.hs index 400cb845..62f2749a 100644 --- a/src/Act/HEVM.hs +++ b/src/Act/HEVM.hs @@ -51,6 +51,8 @@ import EVM.Effects import EVM.Format as Format import EVM.Traversals +import Debug.Trace + type family ExprType a where ExprType 'AInteger = EVM.EWord ExprType 'ABoolean = EVM.EWord @@ -669,7 +671,12 @@ checkInputSpaces :: App m => SolverGroup -> [EVM.Expr EVM.End] -> [EVM.Expr EVM. checkInputSpaces solvers l1 l2 = do let p1 = inputSpace l1 let p2 = inputSpace l2 + -- traceM "Sol props" + -- traceM $ showProps p1 + traceM "Act props" + traceM $ showProps p2 conf <- readConfig + let queries = fmap (assertProps conf) [ [ EVM.PNeg (EVM.por p1), EVM.por p2 ] , [ EVM.por p1, EVM.PNeg (EVM.por p2) ] ] @@ -778,3 +785,6 @@ checkResult calldata sig res = -- | Pretty prints a list of hevm behaviours for debugging purposes showBehvs :: [EVM.Expr a] -> String showBehvs behvs = T.unpack $ T.unlines $ fmap Format.formatExpr behvs + +showProps :: [EVM.Prop] -> String +showProps props = T.unpack $ T.unlines $ fmap Format.formatProp props