diff --git a/g2.cabal b/g2.cabal index 10af109ac..65518cde2 100644 --- a/g2.cabal +++ b/g2.cabal @@ -47,6 +47,7 @@ library , G2.Equiv.Types , G2.Equiv.Generalize , G2.Equiv.Summary + , G2.Equiv.Uninterpreted , G2.Execution , G2.Execution.Interface diff --git a/nebula_scripts/Build_cabal_and_project.py b/nebula_scripts/Build_cabal_and_project.py index 49d6e8e25..a8da69589 100644 --- a/nebula_scripts/Build_cabal_and_project.py +++ b/nebula_scripts/Build_cabal_and_project.py @@ -4,15 +4,20 @@ # first argument is the python file # second argument is the directory that contain all the package that contain rules # third argument is the location of g2 in one's computer + + import os import sys import re import tempfile +import itertools def changing_cabal(directory): found_ghc = False found_build = False extension_to_check = ['library','test-suite','executable'] + # common stanza: binding or expression reused in different parts of the module + modularity = ['import'] for root, dirs, files in os.walk(directory): for file_name in files: # process for replace cabal file @@ -27,7 +32,7 @@ def changing_cabal(directory): with open(file_path,'r') as file, open(temp_path,'a') as temp_file: lines = file.readlines() # reading two lines together - for line,next_line in zip(lines,lines[1:]): + for line,next_line in itertools.zip_longest(lines, lines[1:], fillvalue=''): search_build_depends = re.search("Build-Depends:",line,re.IGNORECASE) if search_build_depends: print("The build-depends before update is " + line) @@ -36,22 +41,44 @@ def changing_cabal(directory): found_build = True for extension in extension_to_check: if line.startswith(extension): + for module in modularity: + next_line_strip = next_line.lstrip() + if not next_line_strip.startswith(module): # finding the correct amount of whitespace to insert in the next line + print("The next line's content " + next_line) + without_whitespace = next_line.lstrip() + whitespace_amount = len(next_line) - len(without_whitespace) + line = line + "\n" + " " * whitespace_amount + "ghc-options: -fplugin=G2.Nebula -fplugin-opt=G2.Nebula:--limit -fplugin-opt=G2.Nebula:10" + "\n" + print("Chaging line for ghc-option") + print("the line after changing is " + line) + found_ghc = True + # taking care of the common stanza case + for module in modularity: + line_without_space = line.lstrip() + if line_without_space.startswith(module): without_whitespace = next_line.lstrip() whitespace_amount = len(next_line) - len(without_whitespace) line = line + "\n" + " " * whitespace_amount + "ghc-options: -fplugin=G2.Nebula -fplugin-opt=G2.Nebula:--limit -fplugin-opt=G2.Nebula:10" + "\n" print("Chaging line for ghc-option") - print("the line after changing is " + line ) + print("the line after changing is " + line) found_ghc = True temp_file.write(line) #writing build-depends and ghc-option in case of not founding those with open(temp_path, 'a+') as temp: - if found_build == False: - print("build-depends not found \n") - temp.write( "build-depends: g2 >= 0.1.0.2 " + '\n') - if found_ghc == False: - print("ghc-option not found \n") - temp.write("ghc-options: -fplugin=G2.Nebula -fplugin-opt=G2.Nebula:--limit -fplugin-opt=G2.Nebula:10") + lines = temp.readlines() + if lines: + # format the ghc option and build-depends against previous line of the file + last_line = lines[-1] + last_line_whitespace = last_line.lstrip() + whitespace_amount = len(last_line) - len(last_line_whitespace) + if found_build == False: + print("build-depends not found \n") + write_line = whitespace_amount * " " + "build-depends: g2 >= 0.1.0.2 " + '\n' + temp.write(write_line) + if found_ghc == False: + print("ghc-option not found \n") + write_line = whitespace_amount * " " + "ghc-options: -fplugin=G2.Nebula -fplugin-opt=G2.Nebula:--limit -fplugin-opt=G2.Nebula:10" + temp.write(write_line) os.replace(temp_path, file_path) # checking for error just in case and left a error file in the directory except BaseException: diff --git a/nebula_scripts/ScriptForHackageRules2.py b/nebula_scripts/ScriptForHackageRules2.py index 77acc94cd..75321ab98 100644 --- a/nebula_scripts/ScriptForHackageRules2.py +++ b/nebula_scripts/ScriptForHackageRules2.py @@ -82,7 +82,7 @@ def starter(directory): # "main" args = sys.argv if len(args) != 2: - raise Exception("Invalid number of commands provided.") + raise Exception("Invalid number of commands provided. The first argument is the script name. The second argument is the name of the directory contain all of the download hackage") with open("./hackageRules1.txt", 'w') as file: file.truncate() directory = sys.argv[1] diff --git a/src/G2/Equiv/Config.hs b/src/G2/Equiv/Config.hs index 22aed345c..3d2891f2a 100644 --- a/src/G2/Equiv/Config.hs +++ b/src/G2/Equiv/Config.hs @@ -19,7 +19,9 @@ data NebulaConfig = NC { limit :: Int , print_summary :: SummaryMode , use_labeled_errors :: UseLabeledErrors , log_states :: LogMode -- ^ Determines whether to Log states, and if logging states, how to do so. - , sync :: Bool } + , log_rule :: Maybe String -- ^ Allow user to log the states for specific rule. + , sync :: Bool + , symbolic_unmapped :: Bool} data SummaryMode = SM { have_summary :: Bool , have_history :: Bool @@ -74,7 +76,17 @@ mkNebulaConfig = NC <*> mkSummaryMode <*> flag UseLabeledErrors NoLabeledErrors (long "no-labeled-errors" <> help "disable labeled errors, treating all errors as equivalent") <*> mkLogMode + <*> mkLogRule <*> flag False True (long "sync" <> help "sync the left and right expressions prior to symbolic execution") + <*> flag True False (long "sym-unmapped" <> help "automatically treat unmapped function as symbolic") + +mkLogRule :: Parser (Maybe String) +mkLogRule = + option (maybeReader (Just . Just)) + ( long "log-rule" + <> metavar "RULE" + <> value Nothing + <> help "Output states for this rule when logging") mkSummaryMode :: Parser SummaryMode mkSummaryMode = diff --git a/src/G2/Equiv/EquivADT.hs b/src/G2/Equiv/EquivADT.hs index 874133396..8d39af858 100644 --- a/src/G2/Equiv/EquivADT.hs +++ b/src/G2/Equiv/EquivADT.hs @@ -94,7 +94,7 @@ exprPairing ns s1@(State {expr_env = h1}) s2@(State {expr_env = h2}) e1 e2 pairs | m <- idName i , not $ m `elem` ns , Just e <- E.lookup m h2 -> exprPairing ns s1 s2 e1 e pairs n1 (m:n2) - | not $ (idName i) `elem` ns -> error "unmapped variable" + | not $ (idName i) `elem` ns -> error $ "unmapped variable" ++ show (idName i) (Prim p1 _, Prim p2 _) | p1 == Error || p1 == Undefined , p2 == Error || p2 == Undefined -> Just pairs -- extra cases for avoiding Error problems diff --git a/src/G2/Equiv/Uninterpreted.hs b/src/G2/Equiv/Uninterpreted.hs new file mode 100644 index 000000000..a16b2953f --- /dev/null +++ b/src/G2/Equiv/Uninterpreted.hs @@ -0,0 +1,139 @@ +{-# LANGUAGE FlexibleContexts, OverloadedStrings #-} + + +module G2.Equiv.Uninterpreted where + +import G2.Language +import qualified G2.Language.ExprEnv as E +import Data.Foldable +import Data.Maybe +import qualified Data.Monoid as DM +import qualified Data.HashMap.Lazy as HM +import qualified Data.HashSet as HS +import Debug.Trace +import qualified Data.Text as T + +-- | Find variables that don't have binding and adjust the epxression environment to treat them as symbolic +addFreeVarsAsSymbolic :: ExprEnv -> ExprEnv +addFreeVarsAsSymbolic eenv = let xs = freeVars eenv eenv + in foldl' (flip E.insertSymbolic) eenv xs + +-- | changing the signature of addFreeTypes so that we have +-- we want to modify the rewrite-rules passed in checkrule +-- (AstContainer c Expr, Astcontainer c Type, AstContainer t Expr, Astcontainer t Type) => c -> State t -> NameGen -> (c, State t, NameGen) +-- | apply subvars to the rule +addFreeTypes :: (ASTContainer c Expr, ASTContainer c Type, ASTContainer t Expr, ASTContainer t Type) => c -> State t -> NameGen -> (c, State t, NameGen) +addFreeTypes c s@(State {type_env = tenv }) ng = + let + (tenv', ng') = freeTypesToTypeEnv (freeTypes tenv s) ng + tenv'' = HM.union tenv tenv' + free_dc = HS.toList $ freeDC tenv'' s + m = dataConMapping free_dc + s' = subVars m s + c' = subVars m c + n_te = addDataCons tenv'' free_dc + in (c', s' { type_env = n_te }, ng' ) + -- trace ("show map " ++ show m) (s' { type_env = n_te }, ng') + + +allDC :: ASTContainer t Expr => t -> HS.HashSet DataCon +allDC = evalASTs allDC' + +allDC' :: Expr -> HS.HashSet DataCon +allDC' e = case e of + Data dc -> HS.singleton dc + Case _ _ _ as -> + HS.fromList $ mapMaybe (\(Alt am _) -> case am of + DataAlt dc _ -> Just dc + _ -> Nothing) as + _ -> HS.empty + + + +freeDC :: ASTContainer e Expr => TypeEnv -> e -> HS.HashSet DataCon +freeDC typeEnv e = + let al = allDC e + inTEnv = HS.map (\(DataCon n _) -> n) + . HS.fromList + . concatMap dataCon + . HM.elems $ typeEnv in + HS.filter (\(DataCon n _) -> not (HS.member n inTEnv)) al + + +allTypes :: ASTContainer t Type => t -> [(Name, Kind)] +allTypes = evalASTs allTypes' + +allTypes' :: Type -> [(Name, Kind)] +allTypes' t = case t of + TyCon n k -> [(n,k)] + _ -> [] + + +freeTypes :: ASTContainer t Type => TypeEnv -> t -> [(Name, Kind)] +freeTypes typeEnv t = HM.toList $ HM.difference (HM.fromList $ allTypes t) typeEnv + + +-- | we getting "free" typesnames and insert it into the TypeEnv with a "uninterprted " dataCons +-- Uninterpreted means there are potentially unlimited amount of datacons for a free type +freeTypesToTypeEnv :: [(Name,Kind)] -> NameGen -> (TypeEnv, NameGen) +freeTypesToTypeEnv nks ng = + let (adts, ng') = mapNG freeTypesToTypeEnv' nks ng + in (HM.fromList adts, ng') + +freeTypesToTypeEnv' :: (Name, Kind) -> NameGen -> ( (Name, AlgDataTy), NameGen) +freeTypesToTypeEnv' (n,k) ng = + let (bids, ng') = freshIds (argumentTypes $ PresType k) ng + (dcs,ng'') = unknownDC ng' n k bids + n_adt = (n, DataTyCon {bound_ids = bids, + data_cons = [dcs]}) + in (n_adt, ng'') + +unknownDC :: NameGen -> Name -> Kind -> [Id] -> (DataCon, NameGen) +unknownDC ng n@(Name occn _ _ _) k is = + let tc = TyCon n k + tv = map TyVar is + ta = foldl' TyApp tc tv + ti = TyLitInt `TyFun` ta + tfa = foldl' (flip TyForAll) ti is + (dc_n, ng') = freshSeededString ("Unknown" DM.<> occn) ng + in (DataCon dc_n tfa, ng') + +-- | add free Datacons into the TypeEnv at the appriorpate Type) +addDataCons :: TypeEnv -> [DataCon] -> TypeEnv +addDataCons = foldl' addDataCon + +addDataCon :: TypeEnv -> DataCon -> TypeEnv +addDataCon te dc | (TyCon n _):_ <- unTyApp $ returnType dc = + let dtc = HM.lookup n te + adt = case dtc of + Just (DataTyCon ids' dcs) -> DataTyCon {bound_ids = ids', data_cons = dc : dcs} + Nothing -> error "addDataCons: cannot find corresponding Name in TypeEnv" + Just _ -> error "addDataCons: Not DataTyCon AlgDataTy found" + in HM.insert n adt te +addDataCon _ _ = error "addDataCon: Type of DataCon had incorrect form" + +-- | addMapping will handle classification between the DataCon and Type +addMapping :: [DataCon] -> ExprEnv -> ExprEnv +addMapping dcs ee = foldl' addMapping' ee dcs + +addMapping' :: ExprEnv -> DataCon -> ExprEnv +addMapping' ee dc@(DataCon name _) = E.insert name (Data dc) ee + + +-- | The translation between GHC and g2 didn't have a matching id for the same occurence name +-- so we are using brute force by matching the same occurence name + +dataConMapping :: [DataCon] -> HM.HashMap (T.Text, Maybe T.Text) DataCon +dataConMapping dcs = HM.fromList $ map dataConMapping' dcs + +dataConMapping' :: DataCon -> ((T.Text, Maybe T.Text ), DataCon) +dataConMapping' dc@(DataCon (Name t mt _ _ ) _ ) = ((t,mt), dc) + +subVars :: ASTContainer t Expr => HM.HashMap (T.Text, Maybe T.Text) DataCon -> t -> t +subVars m = modifyASTs (subVars' m) + +subVars' :: HM.HashMap (T.Text, Maybe T.Text) DataCon -> Expr -> Expr +subVars' m expr@(Var (Id (Name t mt _ _) _ )) = case HM.lookup (t,mt) m of + Just (DataCon n' k) -> Data (DataCon n' k) + Nothing -> expr +subVars' _ expr = expr diff --git a/src/G2/Equiv/Verifier.hs b/src/G2/Equiv/Verifier.hs index ed4150f71..c87b7f641 100644 --- a/src/G2/Equiv/Verifier.hs +++ b/src/G2/Equiv/Verifier.hs @@ -1,5 +1,6 @@ {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE FlexibleContexts #-} module G2.Equiv.Verifier ( verifyLoop @@ -14,6 +15,7 @@ import G2.Interface import qualified Control.Monad.State.Lazy as CM + import qualified G2.Language.ExprEnv as E import qualified G2.Language.CallGraph as G import qualified G2.Language.Typing as T @@ -34,6 +36,7 @@ import G2.Equiv.G2Calls import G2.Equiv.Tactics import G2.Equiv.Generalize import G2.Equiv.Summary +import G2.Equiv.Uninterpreted import qualified Data.Map as M import G2.Execution.Memory @@ -754,7 +757,7 @@ reducedGuide ((Marker _ m):ms) = case m of _ -> reducedGuide ms reducedGuide (_:ms) = reducedGuide ms -checkRule :: Config +checkRule :: (ASTContainer t Type, ASTContainer t Expr) => Config -> NebulaConfig -> State t -> Bindings @@ -762,9 +765,15 @@ checkRule :: Config -> RewriteRule -> IO (S.Result () () ()) checkRule config nc init_state bindings total rule = do - let (rewrite_state_l, bindings') = initWithLHS init_state bindings $ rule - (rewrite_state_r, bindings'') = initWithRHS init_state bindings' $ rule - sym_ids = ru_bndrs rule + let (rule' ,mod_state@(State { expr_env = ee }), te_ng) = addFreeTypes rule init_state (name_gen bindings) + (mod_state', ng') = if symbolic_unmapped nc + then + ( mod_state { expr_env = addFreeVarsAsSymbolic ee } + , te_ng) + else (init_state, name_gen bindings) + (rewrite_state_l, bindings') = initWithLHS mod_state' (bindings { name_gen = ng' }) $ rule' + (rewrite_state_r, bindings'') = initWithRHS mod_state' bindings' $ rule' + sym_ids = ru_bndrs rule' total_names = filter (includedName total) (map idName sym_ids) total_hs = foldr HS.insert HS.empty total_names EquivTracker et m _ _ _ _ = emptyEquivTracker @@ -781,6 +790,8 @@ checkRule config nc init_state bindings total rule = do rewrite_state_l'' = startingState start_equiv_tracker ns rewrite_state_l' rewrite_state_r'' = startingState start_equiv_tracker ns rewrite_state_r' + + print (curr_expr rewrite_state_l) S.SomeSolver solver <- initSolver config putStrLn $ "***\n" ++ (show $ ru_name rule) ++ "\n***" diff --git a/src/G2/Execution/Rules.hs b/src/G2/Execution/Rules.hs index 2c34e7a91..6130997af 100644 --- a/src/G2/Execution/Rules.hs +++ b/src/G2/Execution/Rules.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE OverloadedStrings, FlexibleContexts #-} module G2.Execution.Rules ( module G2.Execution.RuleTypes , Sharing (..) diff --git a/src/G2/Language/Expr.hs b/src/G2/Language/Expr.hs index 8e8851ad2..0fc8c07ca 100644 --- a/src/G2/Language/Expr.hs +++ b/src/G2/Language/Expr.hs @@ -472,9 +472,14 @@ symbVars' eenv (Id n _) = E.isSymbolic n eenv freeVars :: ASTContainer m Expr => E.ExprEnv -> m -> [Id] freeVars eenv = evalASTsMonoid (freeVars' eenv) +freeAltMatch :: AltMatch -> [Id] +freeAltMatch (DataAlt _ is) = is +freeAltMatch _ = [] + freeVars' :: E.ExprEnv -> [Id] -> Expr -> ([Id], [Id]) freeVars' _ _ (Let b _) = (map fst b, []) freeVars' _ _ (Lam _ b _) = ([b], []) +freeVars' _ _ (Case _ b _ alt) = (b:concatMap (freeAltMatch . altMatch) alt, []) freeVars' eenv bound (Var i) = if E.member (idName i) eenv || i `elem` bound then ([], []) diff --git a/src/G2/Language/Support.hs b/src/G2/Language/Support.hs index 5076eed56..98eabfa9b 100644 --- a/src/G2/Language/Support.hs +++ b/src/G2/Language/Support.hs @@ -199,7 +199,8 @@ instance ASTContainer t Expr => ASTContainer (State t) Expr where (containedASTs $ path_conds s) ++ (containedASTs $ assert_ids s) ++ (containedASTs $ exec_stack s) ++ - (containedASTs $ track s) + (containedASTs $ track s) ++ + (containedASTs $ rules s) modifyContainedASTs f s = s { type_env = modifyContainedASTs f $ type_env s , expr_env = modifyContainedASTs f $ expr_env s @@ -207,7 +208,8 @@ instance ASTContainer t Expr => ASTContainer (State t) Expr where , path_conds = modifyContainedASTs f $ path_conds s , assert_ids = modifyContainedASTs f $ assert_ids s , exec_stack = modifyContainedASTs f $ exec_stack s - , track = modifyContainedASTs f $ track s } + , track = modifyContainedASTs f $ track s + , rules = modifyContainedASTs f $ rules s } instance ASTContainer t Type => ASTContainer (State t) Type where containedASTs s = ((containedASTs . expr_env) s) ++ @@ -217,7 +219,8 @@ instance ASTContainer t Type => ASTContainer (State t) Type where ((containedASTs . assert_ids) s) ++ ((containedASTs . type_classes) s) ++ ((containedASTs . exec_stack) s) ++ - (containedASTs $ track s) + (containedASTs $ track s) ++ + (containedASTs $ rules s) modifyContainedASTs f s = s { type_env = (modifyContainedASTs f . type_env) s , expr_env = (modifyContainedASTs f . expr_env) s @@ -226,7 +229,8 @@ instance ASTContainer t Type => ASTContainer (State t) Type where , assert_ids = (modifyContainedASTs f . assert_ids) s , type_classes = (modifyContainedASTs f . type_classes) s , exec_stack = (modifyContainedASTs f . exec_stack) s - , track = modifyContainedASTs f $ track s } + , track = modifyContainedASTs f $ track s + , rules = modifyContainedASTs f $ rules s } instance Named Bindings where names b = names (fixed_inputs b) diff --git a/src/G2/Nebula.hs b/src/G2/Nebula.hs index 89cbe876a..4d1f8ea43 100644 --- a/src/G2/Nebula.hs +++ b/src/G2/Nebula.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE CPP #-} +{-# LANGUAGE CPP, FlexibleContexts #-} module G2.Nebula (plugin) where @@ -73,7 +73,7 @@ nebulaPluginPass' m_entry nebula_config env modguts = do (\_ ng _ _ _ _ _ -> (Prim Undefined TyBottom, [], [], ng)) (E.higherOrderExprs . IT.expr_env) config - + let total = [] case m_entry of Just entry -> do @@ -89,7 +89,7 @@ nebulaPluginPass' m_entry nebula_config env modguts = do mapM_ (checkRulePrinting config nebula_config init_state bindings total) $ filter (\r -> L.ru_module r == mod_name) (rewrite_rules bindings) -checkRulePrinting :: Config +checkRulePrinting :: (ASTContainer t L.Type, ASTContainer t L.Expr) => Config -> NebulaConfig -> State t -> Bindings @@ -98,8 +98,13 @@ checkRulePrinting :: Config -> IO (S.Result () () ()) checkRulePrinting config nebula_config init_state bindings total rule = do let rule_name = T.unpack $ L.ru_name rule + nebula_config' = case log_rule nebula_config of + Just n -> if n == rule_name then nebula_config + else nebula_config {log_states = NoLog} + Nothing -> nebula_config + putStrLn $ "Log-rule nebula config = " ++ show (log_rule nebula_config) putStrLn $ "Checking " ++ rule_name - res <- checkRule config nebula_config init_state bindings total rule + res <- checkRule config nebula_config' init_state bindings total rule case res of S.SAT _ -> putStrLn $ rule_name ++ " - counterexample found" S.UNSAT _ -> putStrLn $ rule_name ++ " - verified" diff --git a/tests/RewriteVerify/PluginTests/Import/CHANGELOG.md b/tests/RewriteVerify/PluginTests/Import/CHANGELOG.md new file mode 100644 index 000000000..3df75e525 --- /dev/null +++ b/tests/RewriteVerify/PluginTests/Import/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for Import + +## 0.1.0.0 -- YYYY-mm-dd + +* First version. Released on an unsuspecting world. diff --git a/tests/RewriteVerify/PluginTests/Import/Import.cabal b/tests/RewriteVerify/PluginTests/Import/Import.cabal new file mode 100644 index 000000000..a498b1391 --- /dev/null +++ b/tests/RewriteVerify/PluginTests/Import/Import.cabal @@ -0,0 +1,37 @@ +cabal-version: 2.4 +name: Import +version: 0.1.0.0 + +-- A short (one-line) description of the package. +-- synopsis: + +-- A longer description of the package. +-- description: + +-- A URL where users can report bugs. +-- bug-reports: + +-- The license under which the package is released. +-- license: + +-- The package author(s). +-- author: + +-- An email address to which users can send suggestions, bug reports, and patches. +-- maintainer: + +-- A copyright notice. +-- copyright: +-- category: +extra-source-files: CHANGELOG.md + +library + exposed-modules: Import + -- Modules included in this executable, other than Main. + -- other-modules: + + -- LANGUAGE extensions used by modules in this package. + -- other-extensions: + build-depends: base >=4.8.0.0 + hs-source-dirs: app + default-language: Haskell2010 diff --git a/tests/RewriteVerify/PluginTests/Import/app/Import.hs b/tests/RewriteVerify/PluginTests/Import/app/Import.hs new file mode 100644 index 000000000..49f8a16e6 --- /dev/null +++ b/tests/RewriteVerify/PluginTests/Import/app/Import.hs @@ -0,0 +1,7 @@ +module Import where + +add1 :: Int -> Int +add1 a = a+1 + +data SomeType = MkSomeType Int + diff --git a/tests/RewriteVerify/PluginTests/Simple/PluginTests.cabal b/tests/RewriteVerify/PluginTests/Simple/PluginTests.cabal index a521fc7b4..f46a909c2 100644 --- a/tests/RewriteVerify/PluginTests/Simple/PluginTests.cabal +++ b/tests/RewriteVerify/PluginTests/Simple/PluginTests.cabal @@ -10,13 +10,14 @@ executable PluginTests main-is: Main.hs -- Modules included in this executable, other than Main. - other-modules: Nat + other-modules: Nat, ImportTest -- LANGUAGE extensions used by modules in this package. -- other-extensions: build-depends: base >= 4.8.0.0 , g2 >= 0.1.0.2 + , Import default-extensions: LambdaCase hs-source-dirs: app - ghc-options: -fplugin=G2.Nebula + ghc-options: -fplugin=G2.Nebula default-language: Haskell2010 diff --git a/tests/RewriteVerify/PluginTests/Simple/app/ImportTest.hs b/tests/RewriteVerify/PluginTests/Simple/app/ImportTest.hs new file mode 100644 index 000000000..b4c17acd7 --- /dev/null +++ b/tests/RewriteVerify/PluginTests/Simple/app/ImportTest.hs @@ -0,0 +1,23 @@ +module ImportTest where + +import Import + +{-# RULES +"simplifyAdd1" forall x . myId (add1 x) = x + 1 + +"importTypes" forall x . foo (MkSomeType x) = x * 2 + + #-} + +myId :: a -> a +myId x = x + + +{-# NOINLINE foo #-} +foo :: SomeType->Int +foo (MkSomeType x) = x + + +{-# NOINLINE callAdd1 #-} +callAdd1 :: Int -> Int +callAdd1 x = 1 + add1 x \ No newline at end of file diff --git a/tests/RewriteVerify/PluginTests/Simple/app/Main.hs b/tests/RewriteVerify/PluginTests/Simple/app/Main.hs index 6f7866066..9e7a6a5b9 100644 --- a/tests/RewriteVerify/PluginTests/Simple/app/Main.hs +++ b/tests/RewriteVerify/PluginTests/Simple/app/Main.hs @@ -1,6 +1,7 @@ module Main where import Nat +import ImportTest f :: Int -> Int f x = x diff --git a/tests/RewriteVerify/PluginTests/Simple/cabal.project b/tests/RewriteVerify/PluginTests/Simple/cabal.project index 6d8d7f686..2a6d90693 100644 --- a/tests/RewriteVerify/PluginTests/Simple/cabal.project +++ b/tests/RewriteVerify/PluginTests/Simple/cabal.project @@ -1,2 +1,3 @@ packages: . - ./../../../../g2.cabal \ No newline at end of file + ./../../../../g2.cabal + ./../Import/Import.cabal \ No newline at end of file diff --git a/tests/RewriteVerify/RewriteVerifyTest.hs b/tests/RewriteVerify/RewriteVerifyTest.hs index 398fa464a..a5bccd3be 100644 --- a/tests/RewriteVerify/RewriteVerifyTest.hs +++ b/tests/RewriteVerify/RewriteVerifyTest.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE FlexibleContexts #-} + module RewriteVerify.RewriteVerifyTest ( rewriteTests ) where import qualified Data.Map as M @@ -28,7 +30,7 @@ findRule rule_list rule_name = Just r -> r Nothing -> error $ "not found " ++ show rule_name -acceptRule :: Config -> State t -> Bindings -> RewriteRule -> IO Bool +acceptRule :: (ASTContainer t Type, ASTContainer t Expr) => Config -> State t -> Bindings -> RewriteRule -> IO Bool acceptRule config init_state bindings rule = do res <- checkRule config nebulaConfig init_state bindings [] rule return (case res of @@ -36,7 +38,7 @@ acceptRule config init_state bindings rule = do S.UNSAT _ -> True _ -> error "Failed to Produce a Result") -rejectRule :: Config -> State t -> Bindings -> RewriteRule -> IO Bool +rejectRule :: (ASTContainer t Type, ASTContainer t Expr) => Config -> State t -> Bindings -> RewriteRule -> IO Bool rejectRule config init_state bindings rule = do res <- checkRule config nebulaConfig init_state bindings [] rule return (case res of @@ -50,6 +52,7 @@ nebulaConfig = NC { limit = 20 , print_summary = SM False False False , use_labeled_errors = UseLabeledErrors , log_states = NoLog + , symbolic_unmapped = False , sync = False} good_names :: [String]