Skip to content

Commit

Permalink
Fix for decompiler QC tests
Browse files Browse the repository at this point in the history
  • Loading branch information
zoep committed Oct 31, 2024
1 parent fd60c94 commit f464723
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 6 deletions.
4 changes: 2 additions & 2 deletions src/Act/Syntax/TimeAgnostic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,7 @@ deriving instance Show (VarRef t)
-- TODO better way to do Vars and Storage entires without duplication

instance Eq (VarRef t) where
VVar _ at x == VVar _ at' x' = at == at' && x == x'
VVar _ _ x == VVar _ _ x' = x == x' -- NOTE: adding equality of types fails decompilation QC tests. We must fix this.
VMapping _ r ixs == VMapping _ r' ixs' = r == r' && ixs == ixs'
VField _ r c x == VField _ r' c' x' = r == r' && c == c' && x == x'
_ == _ = False
Expand Down Expand Up @@ -283,7 +283,7 @@ instance Eq (Exp a t) where

ITE _ a b c == ITE _ d e f = a == d && b == e && c == f
TEntry _ a t == TEntry _ b u = a == b && t == u
Var _ _ _ vt1 a == Var _ _ _ vt2 b = vt1 == vt2 && a == b
Var _ _ _ _ a == Var _ _ _ _ b = a == b -- NOTE: add equality for ValueTypes that currently fails QC tests for decompiler

Create _ a b == Create _ c d = a == c && b == d

Expand Down
10 changes: 6 additions & 4 deletions src/Test/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ module Main where

import Prelude hiding (GT, LT)
import Test.Tasty
import Test.Tasty.QuickCheck (Gen, arbitrary, testProperty, Property, (===), counterexample)
import Test.Tasty.QuickCheck (Gen, arbitrary, testProperty, Property, (===), counterexample, whenFail)
import Test.QuickCheck.Instances.ByteString()
import Test.QuickCheck.GenT
import Test.QuickCheck.Monadic
Expand All @@ -21,7 +21,7 @@ import Data.Map (fromList)

import Act.CLI (compile)
import Act.Error
import Act.Print (prettyBehaviour)
import Act.Print (prettyBehaviour, prettyAct)
import Act.SMT
import Act.Syntax.Annotated

Expand Down Expand Up @@ -60,8 +60,10 @@ main = defaultMain $ testGroup "act"
let actual = compile $ prettyBehaviour behv
expected = Act (defaultStore contract) [Contract (defaultCtor contract) [behv]]
return $ case actual of
Success a -> a === expected
Failure err -> counterexample ("Internal error: compilation of Act failed\n" <> show err) False
Success a ->
let err_str = "Actual:\n" <> prettyAct a <> "Expected:\n" <> prettyAct expected in
whenFail (putStrLn err_str) $ a === expected
Failure err -> counterexample ("Internal error: compilation of Act failed\n" <> show err <> "\n") False
]

, testGroup "smt"
Expand Down

0 comments on commit f464723

Please sign in to comment.