From 3b1a4fa03ba42150ae194c4d33879e6db7702f68 Mon Sep 17 00:00:00 2001 From: Bill Hallahan Date: Tue, 1 Oct 2024 16:02:27 -0400 Subject: [PATCH 01/10] Allow input function calls to be wrapped in coercions --- exe/Main.hs | 6 ++--- src/G2/Initialization/DeepSeqWalks.hs | 28 ++++++++++---------- src/G2/Initialization/MkCurrExpr.hs | 38 ++++++++++++++++++--------- src/G2/Interface/ExecRes.hs | 12 ++++++--- src/G2/Interface/Interface.hs | 7 ++--- src/G2/Language/Support.hs | 17 +++++++++--- src/G2/Nebula.hs | 2 +- src/G2/Translation/HaskellCheck.hs | 18 ++++++------- 8 files changed, 78 insertions(+), 50 deletions(-) diff --git a/exe/Main.hs b/exe/Main.hs index eb35ea9c3..34dc0e1bf 100644 --- a/exe/Main.hs +++ b/exe/Main.hs @@ -49,7 +49,7 @@ runWithArgs as = do case validate config of True -> do - r <- validateStates proj [src] (T.unpack $ fromJust mb_modname) entry [] [Opt_Hpc] in_out + r <- validateStates proj [src] (T.unpack $ fromJust mb_modname) entry [] [Opt_Hpc] b in_out if r then putStrLn "Validated" else putStrLn "There was an error during validation." -- runHPC src (T.unpack $ fromJust mb_modname) entry in_out @@ -61,9 +61,9 @@ runWithArgs as = do printFuncCalls :: Config -> Id -> Bindings -> [ExecRes t] -> IO () printFuncCalls config entry b = - mapM_ (\execr@(ExecRes { final_state = s}) -> do + mapM_ (\execr@(ExecRes { final_state = s }) -> do let pg = mkPrettyGuide (exprNames $ conc_args execr) - let (mvp, inp, outp) = printInputOutput pg entry execr + let (mvp, inp, outp) = printInputOutput pg entry b execr sym_gen_out = fmap (printHaskellPG pg s) $ conc_sym_gens execr case sym_gen_out of diff --git a/src/G2/Initialization/DeepSeqWalks.hs b/src/G2/Initialization/DeepSeqWalks.hs index 779f6477c..742362974 100644 --- a/src/G2/Initialization/DeepSeqWalks.hs +++ b/src/G2/Initialization/DeepSeqWalks.hs @@ -249,26 +249,26 @@ deepSeqFunc w ng ti rm e as' = map (walkerFunc w ti rm) ts in Just $ (foldl' App (Var f) (as ++ as'), ng) - | t@(TyFun _ _) <- typeOf e = - let - (a_in, ng') = freshId t ng + -- | t@(TyFun _ _) <- typeOf e = + -- let + -- (a_in, ng') = freshId t ng - tys = anonArgumentTypes e - (f_is, ng'') = freshIds tys ng' + -- tys = anonArgumentTypes e + -- (f_is, ng'') = freshIds tys ng' - cll = mkApp $ Var a_in:map Var f_is - let_cll = Let (zip f_is $ map (SymGen SNoLog) tys) cll + -- cll = mkApp $ Var a_in:map Var f_is + -- let_cll = Let (zip f_is $ map (SymGen SNoLog) tys) cll - ds_type = typeOf ds_cll + -- ds_type = typeOf ds_cll - (ds_cll, ng''') = deepSeqFuncCall w ng'' ti rm let_cll - (bnd, ng'''') = freshId ds_type ng''' + -- (ds_cll, ng''') = deepSeqFuncCall w ng'' ti rm let_cll + -- (bnd, ng'''') = freshId ds_type ng''' - (lam_ids, ng''''') = freshIds tys ng'''' + -- (lam_ids, ng''''') = freshIds tys ng'''' - cse = Case ds_cll bnd ds_type [Alt Default $ mkLams (zip (repeat TermL) lam_ids) (Var bnd)] - in - Just (Lam TermL a_in cse, ng''''') + -- cse = Case ds_cll bnd ds_type [Alt Default $ mkLams (zip (repeat TermL) lam_ids) (Var bnd)] + -- in + -- Just (Lam TermL a_in cse, ng''''') | (TyVar (Id n _)) <- typeOf e , Just f <- lookup n ti = Just (Var f, ng) diff --git a/src/G2/Initialization/MkCurrExpr.hs b/src/G2/Initialization/MkCurrExpr.hs index 8986c2d60..15dcd30ed 100644 --- a/src/G2/Initialization/MkCurrExpr.hs +++ b/src/G2/Initialization/MkCurrExpr.hs @@ -17,28 +17,22 @@ import qualified Data.HashMap.Lazy as HM mkCurrExpr :: Maybe T.Text -> Maybe T.Text -> Id -> TypeClasses -> NameGen -> ExprEnv -> TypeEnv -> Walkers - -> KnownValues -> Config -> (Expr, [Id], [Expr], NameGen) -mkCurrExpr m_assume m_assert f@(Id (Name _ m_mod _ _) _) tc ng eenv _ walkers kv config = + -> KnownValues -> Config -> (Expr, [Id], [Expr], Maybe Coercion, NameGen) +mkCurrExpr m_assume m_assert f@(Id (Name _ m_mod _ _) _) tc ng eenv tenv walkers kv config = case E.lookup (idName f) eenv of Just ex -> let var_ex = Var (Id (idName f) (typeOf ex)) - -- typs = spArgumentTypes ex + (m_coer, coer_var_ex) = coerceRetNewTypes tenv var_ex - -- (typsE, typs') = instantitateTypes tc kv typs - - -- (var_ids, is, ng') = mkInputs ng typs' - -- -- We refind the type of f, because type synonyms get replaced during the initializaton, -- -- after we first got the type of f. - -- app_ex = foldl' App var_ex $ typsE ++ var_ids (app_ex, is, typsE, ng') = if instTV config == InstBefore - then mkMainExpr tc kv ng var_ex - else mkMainExprNoInstantiateTypes var_ex ng + then mkMainExpr tc kv ng coer_var_ex + else mkMainExprNoInstantiateTypes coer_var_ex ng var_ids = map Var is - -- strict_app_ex = app_ex strict_app_ex = if strict config then mkStrict walkers app_ex else app_ex (name, ng'') = freshName ng' @@ -52,9 +46,29 @@ mkCurrExpr m_assume m_assert f@(Id (Name _ m_mod _ _) _) tc ng eenv _ walkers kv let_ex = Let [(id_name, strict_app_ex)] retsTrue_ex in - (let_ex, is, typsE, ng'') + (let_ex, is, typsE, m_coer, ng'') Nothing -> error "mkCurrExpr: Bad Name" +coerceRetNewTypes :: TypeEnv -> Expr -> (Maybe Coercion, Expr) +coerceRetNewTypes tenv e = + let + t = typeOf e + rt = returnType e + c = coerce_to rt + c_rt = replace_ret_ty c t + coer = t :~ c_rt + in + if rt == c then (Nothing, e) else (Just coer, Cast e coer) + where + coerce_to t | TyCon n _:ts <- unTyApp t + , Just (NewTyCon { bound_ids = bis, rep_type = rt }) <- HM.lookup n tenv = + coerce_to $ foldl' (\rt_ (b, bt) -> retype b bt rt_) rt (zip bis ts) + | otherwise = t + + replace_ret_ty c (TyForAll i t) = TyForAll i $ replace_ret_ty c t + replace_ret_ty c (TyFun t t') = TyFun t $ replace_ret_ty c t' + replace_ret_ty c _ = c + mkMainExpr :: TypeClasses -> KnownValues -> NameGen -> Expr -> (Expr, [Id], [Expr], NameGen) mkMainExpr tc kv ng ex = let diff --git a/src/G2/Interface/ExecRes.hs b/src/G2/Interface/ExecRes.hs index 3d320ee51..ee32b4ecf 100644 --- a/src/G2/Interface/ExecRes.hs +++ b/src/G2/Interface/ExecRes.hs @@ -22,16 +22,17 @@ data ExecRes t = ExecRes { final_state :: State t -- ^ The final state. printInputOutput :: PrettyGuide -> Id -- ^ Input function + -> Bindings -> ExecRes t -> (T.Text, T.Text, T.Text) -printInputOutput pg i er = +printInputOutput pg i (Bindings { input_coercion = c }) er = let er' = er { conc_args = modifyASTs remMutVarPrim (conc_args er) , conc_out = modifyASTs remMutVarPrim (conc_out er) , conc_sym_gens = modifyASTs remMutVarPrim (conc_sym_gens er) , conc_mutvars = modifyASTs remMutVarPrim (conc_mutvars er) } in - (printMutVars pg er', printInputFunc pg i er', printOutput pg er') + (printMutVars pg er', printInputFunc pg c i er', printOutput pg er') printMutVars :: PrettyGuide -> ExecRes t -> T.Text printMutVars pg (ExecRes { final_state = s, conc_mutvars = mv@(_:_) }) = @@ -43,8 +44,11 @@ printMutVars pg (ExecRes { final_state = s, conc_mutvars = mv@(_:_) }) = "let " <> bound <> " in " printMutVars _ _ = "" -printInputFunc :: PrettyGuide -> Id -> ExecRes t -> T.Text -printInputFunc pg i (ExecRes { final_state = s, conc_args = ars }) = printHaskellPG pg s $ mkApp (Var i:ars) +printInputFunc :: PrettyGuide -> Maybe Coercion -> Id -> ExecRes t -> T.Text +printInputFunc pg m_c i (ExecRes { final_state = s, conc_args = ars }) = printHaskellPG pg s $ mkApp (app_maybe_coer m_c (Var i):ars) + where + app_maybe_coer Nothing e = e + app_maybe_coer (Just c) e = Cast e c printOutput :: PrettyGuide -> ExecRes t -> T.Text printOutput pg (ExecRes { final_state = s, conc_out = e }) = printHaskellPG pg s e diff --git a/src/G2/Interface/Interface.hs b/src/G2/Interface/Interface.hs index d186101b1..801eb648c 100644 --- a/src/G2/Interface/Interface.hs +++ b/src/G2/Interface/Interface.hs @@ -85,7 +85,7 @@ type AssertFunc = T.Text type ReachFunc = T.Text type MkCurrExpr = TypeClasses -> NameGen -> ExprEnv -> TypeEnv -> Walkers - -> KnownValues -> Config -> (Expr, [Id], [Expr], NameGen) + -> KnownValues -> Config -> (Expr, [Id], [Expr], Maybe Coercion, NameGen) doTimeout :: Int -> IO a -> IO (Maybe a) doTimeout secs action = do @@ -165,7 +165,7 @@ initStateFromSimpleState s m_mod useAssert mkCurr argTys config = ng' = IT.name_gen s' kv' = IT.known_values s' tc' = IT.type_classes s' - (ce, is, f_i, ng'') = mkCurr tc' ng' eenv' tenv' ds_walkers kv' config + (ce, is, f_i, m_coercion, ng'') = mkCurr tc' ng' eenv' tenv' ds_walkers kv' config in (State { expr_env = foldr E.insertSymbolic eenv' is @@ -192,6 +192,7 @@ initStateFromSimpleState s m_mod useAssert mkCurr argTys config = , arb_value_gen = arbValueInit , cleaned_names = HM.empty , input_names = map idName is + , input_coercion = m_coercion , higher_order_inst = S.filter (\n -> nameModule n == m_mod) . S.fromList $ IT.exports s , rewrite_rules = IT.rewrite_rules s , name_gen = ng'' @@ -356,7 +357,7 @@ initialStateNoStartFunc proj src transConfig config = do let simp_state = initSimpleState exg2 (init_s, bindings) = initStateFromSimpleState simp_state Nothing False - (\_ ng _ _ _ _ _ -> (Prim Undefined TyBottom, [], [], ng)) + (\_ ng _ _ _ _ _ -> (Prim Undefined TyBottom, [], [], Nothing, ng)) (E.higherOrderExprs . IT.expr_env) config diff --git a/src/G2/Language/Support.hs b/src/G2/Language/Support.hs index 9d5841fa6..0636e7b8c 100644 --- a/src/G2/Language/Support.hs +++ b/src/G2/Language/Support.hs @@ -71,7 +71,10 @@ data Bindings = Bindings { deepseq_walkers :: Walkers , arb_value_gen :: ArbValueGen , cleaned_names :: CleanedNames , higher_order_inst :: S.HashSet Name -- ^ Functions to try instantiating higher order functions with - , input_names :: [Name] + + , input_names :: [Name] -- ^ Names of input symbolic arguments + , input_coercion :: Maybe Coercion -- ^ Coercion wrapping the initial function call + , rewrite_rules :: ![RewriteRule] , name_gen :: NameGen , exported_funcs :: [Name] @@ -262,6 +265,7 @@ instance Named Bindings where <> names (cleaned_names b) <> names (higher_order_inst b) <> names (input_names b) + <> names (input_coercion b) <> names (exported_funcs b) <> names (rewrite_rules b) @@ -272,6 +276,7 @@ instance Named Bindings where , cleaned_names = HM.insert new old (cleaned_names b) , higher_order_inst = rename old new (higher_order_inst b) , input_names = rename old new (input_names b) + , input_coercion = rename old new (input_coercion b) , rewrite_rules = rename old new (rewrite_rules b) , name_gen = name_gen b , exported_funcs = rename old new (exported_funcs b) @@ -284,6 +289,7 @@ instance Named Bindings where , cleaned_names = foldr (\(old, new) -> HM.insert new old) (cleaned_names b) (HM.toList hm) , higher_order_inst = renames hm (higher_order_inst b) , input_names = renames hm (input_names b) + , input_coercion = renames hm (input_coercion b) , rewrite_rules = renames hm (rewrite_rules b) , name_gen = name_gen b , exported_funcs = renames hm (exported_funcs b) @@ -296,10 +302,13 @@ instance ASTContainer Bindings Expr where , input_names = modifyContainedASTs f $ input_names b } instance ASTContainer Bindings Type where - containedASTs b = ((containedASTs . fixed_inputs) b) ++ ((containedASTs . input_names) b) + containedASTs b = (containedASTs . fixed_inputs $ b) + ++ (containedASTs . input_names $ b) + ++ (containedASTs . input_coercion $ b) - modifyContainedASTs f b = b { fixed_inputs = (modifyContainedASTs f . fixed_inputs) b - , input_names = (modifyContainedASTs f . input_names) b } + modifyContainedASTs f b = b { fixed_inputs = modifyContainedASTs f . fixed_inputs $ b + , input_names = modifyContainedASTs f . input_names $ b + , input_coercion = modifyContainedASTs f . input_coercion $ b } instance ASTContainer CurrExpr Expr where containedASTs (CurrExpr _ e) = [e] diff --git a/src/G2/Nebula.hs b/src/G2/Nebula.hs index e42ec1a69..dfcb25eb7 100644 --- a/src/G2/Nebula.hs +++ b/src/G2/Nebula.hs @@ -70,7 +70,7 @@ nebulaPluginPass' m_entry nebula_config env modguts = do let simp_state = initSimpleState injected_exg2 (init_state, bindings) = initStateFromSimpleState simp_state Nothing False - (\_ ng _ _ _ _ _ -> (Prim Undefined TyBottom, [], [], ng)) + (\_ ng _ _ _ _ _ -> (Prim Undefined TyBottom, [], [], Nothing, ng)) (E.higherOrderExprs . IT.expr_env) config diff --git a/src/G2/Translation/HaskellCheck.hs b/src/G2/Translation/HaskellCheck.hs index dcb32fa2a..191077b3a 100644 --- a/src/G2/Translation/HaskellCheck.hs +++ b/src/G2/Translation/HaskellCheck.hs @@ -38,8 +38,8 @@ import System.Process import Control.Monad.IO.Class -- | Load the passed module(s) into GHC, and check that the `ExecRes` results are correct. -validateStates :: [FilePath] -> [FilePath] -> String -> String -> [String] -> [GeneralFlag] -> [ExecRes t] -> IO Bool -validateStates proj src modN entry chAll gflags in_out = do +validateStates :: [FilePath] -> [FilePath] -> String -> String -> [String] -> [GeneralFlag] -> Bindings -> [ExecRes t] -> IO Bool +validateStates proj src modN entry chAll gflags b in_out = do and <$> runGhc (Just libdir) (do adjustDynFlags loadToCheck proj src modN gflags @@ -48,7 +48,7 @@ validateStates proj src modN entry chAll gflags in_out = do let pg = updatePGValNames (concatMap (map Data . dataCon) $ type_env s) $ updatePGTypeNames (type_env s) $ mkPrettyGuide () _ <- createDecls pg s (H.filter (\x -> adt_source x == ADTG2Generated) (type_env s)) - validateStatesGHC pg (Just $ T.pack modN) entry chAll er) in_out) + validateStatesGHC pg (Just $ T.pack modN) entry chAll b er) in_out) -- | Convert g2 generated types into readable string that aim to notify the environment about the types generated by g2 -- The type is formatted as the following: @@ -67,9 +67,9 @@ creatDeclStr pg s (x, DataTyCon{data_cons = dcs, bound_ids = is}) = creatDeclStr _ _ _ = error "creatDeclStr: unsupported AlgDataTy" -- | Compile with GHC, and check that the output we got is correct for the input -validateStatesGHC :: PrettyGuide -> I.ModuleName -> String -> [String] -> ExecRes t -> Ghc Bool -validateStatesGHC pg modN entry chAll er@(ExecRes {final_state = s, conc_out = out}) = do - (v, chAllR) <- runCheck pg modN entry chAll er +validateStatesGHC :: PrettyGuide -> I.ModuleName -> String -> [String] -> Bindings -> ExecRes t -> Ghc Bool +validateStatesGHC pg modN entry chAll b er@(ExecRes {final_state = s, conc_out = out}) = do + (v, chAllR) <- runCheck pg modN entry chAll b er v' <- liftIO $ (unsafeCoerce v :: IO (Either SomeException Bool)) let outStr = T.unpack $ printHaskell s out @@ -96,8 +96,8 @@ adjustDynFlags = do _ <- setSessionDynFlags dyn'' return () -runCheck :: PrettyGuide -> I.ModuleName -> String -> [String] -> ExecRes t -> Ghc (HValue, [HValue]) -runCheck init_pg modN entry chAll er@(ExecRes {final_state = s, conc_args = ars, conc_out = out}) = do +runCheck :: PrettyGuide -> I.ModuleName -> String -> [String] -> Bindings -> ExecRes t -> Ghc (HValue, [HValue]) +runCheck init_pg modN entry chAll b er@(ExecRes {final_state = s, conc_args = ars, conc_out = out}) = do let Left (v, _) = findFunc (T.pack entry) [modN] (expr_env s) let e = mkApp $ Var v:ars let pg = updatePGValAndTypeNames e @@ -105,7 +105,7 @@ runCheck init_pg modN entry chAll er@(ExecRes {final_state = s, conc_args = ars, $ updatePGValAndTypeNames (varIds v) init_pg -- let arsStr = T.unpack $ printHaskellPG pg s e -- let outStr = T.unpack $ printHaskellPG pg s out - let (mvTxt, arsTxt, outTxt) = printInputOutput pg v er + let (mvTxt, arsTxt, outTxt) = printInputOutput pg v b er mvStr = T.unpack mvTxt arsStr = T.unpack arsTxt outStr = T.unpack outTxt From f236dfa14e0e654eb38e4cd31468426069aa7a53 Mon Sep 17 00:00:00 2001 From: Bill Hallahan Date: Tue, 1 Oct 2024 16:26:17 -0400 Subject: [PATCH 02/10] Correct LH build errors --- src/G2/Liquid/Inference/Initalization.hs | 2 +- src/G2/Liquid/Interface.hs | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/G2/Liquid/Inference/Initalization.hs b/src/G2/Liquid/Inference/Initalization.hs index 61c7a92c2..b1af23553 100644 --- a/src/G2/Liquid/Inference/Initalization.hs +++ b/src/G2/Liquid/Inference/Initalization.hs @@ -42,7 +42,7 @@ createStateForInference simp_s main_mod config lhconfig ghci = then fmap Just $ addTyVarsEEnvTEnv simp_s else (simp_s, Nothing) (s, b) = initStateFromSimpleState simp_s' main_mod True - (\_ ng _ _ _ _ _ -> (Prim Undefined TyBottom, [], [], ng)) + (\_ ng _ _ _ _ _ -> (Prim Undefined TyBottom, [], [], Nothing, ng)) (E.higherOrderExprs . IT.expr_env) config in diff --git a/src/G2/Liquid/Interface.hs b/src/G2/Liquid/Interface.hs index c4aa55a9f..56da82d84 100644 --- a/src/G2/Liquid/Interface.hs +++ b/src/G2/Liquid/Interface.hs @@ -86,6 +86,7 @@ import qualified Data.Text as T import qualified Data.Text.IO as TI import G2.Language.Monad +import G2.Language.Support (Bindings(input_coercion)) data LHReturn = LHReturn { calledFunc :: FuncInfo , violating :: Maybe FuncInfo @@ -350,7 +351,7 @@ processLiquidReadyStateWithCall lrs@(LiquidReadyState { lr_state = lhs@(LHState Left ie' -> ie' Right errs -> error errs - (ce, is, f_i, ng') = mkCurrExpr Nothing Nothing ie (type_classes s) (name_gen bindings) + (ce, is, f_i, m_c, ng') = mkCurrExpr Nothing Nothing ie (type_classes s) (name_gen bindings) (expr_env s) (type_env s) (deepseq_walkers bindings) (known_values s) config lhs' = lhs { state = s { expr_env = foldr E.insertSymbolic (expr_env s) is @@ -363,6 +364,7 @@ processLiquidReadyStateWithCall lrs@(LiquidReadyState { lr_state = lhs@(LHState lrs' = lrs { lr_state = lhs''' , lr_binding = bindings' { fixed_inputs = f_i , input_names = map idName is + , input_coercion = m_c } } From bf87c6e7a34d45be186de867a435fd14b2fc3b9e Mon Sep 17 00:00:00 2001 From: Bill Hallahan Date: Tue, 1 Oct 2024 16:42:06 -0400 Subject: [PATCH 03/10] Fixing build error in test --- tests/InputOutputTest.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/InputOutputTest.hs b/tests/InputOutputTest.hs index 71901abbb..180677d50 100644 --- a/tests/InputOutputTest.hs +++ b/tests/InputOutputTest.hs @@ -98,18 +98,18 @@ checkInputOutput' io_config src tests = do checkInputOutput'' :: [FilePath] -> ExtractedG2 -> Maybe T.Text - -> Config + -> Config -> (String, Int, [Reqs String]) -> IO (Bool, [ExecRes ()]) checkInputOutput'' src exg2 mb_modname config (entry, stps, req) = do let config' = config { steps = stps } (init_state, bindings) = initStateWithCall exg2 False (T.pack entry) mb_modname (mkCurrExpr Nothing Nothing) mkArgTys config' - (r, _) <- runG2WithConfig mb_modname init_state config' bindings + (r, b) <- runG2WithConfig mb_modname init_state config' bindings let chAll = checkExprAll req let proj = map takeDirectory src - mr <- validateStates proj src (T.unpack $ fromJust mb_modname) entry chAll [] r + mr <- validateStates proj src (T.unpack $ fromJust mb_modname) entry chAll [] b r let io = map (\(ExecRes { conc_args = i, conc_out = o}) -> i ++ [o]) r let chEx = checkExprInOutCount io req From b3199fc1c525445c31d9798f4b4b4fd2aabbe9e2 Mon Sep 17 00:00:00 2001 From: Bill Hallahan Date: Tue, 1 Oct 2024 20:08:36 -0400 Subject: [PATCH 04/10] Fixed build error --- tests/FuzzExecution.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/FuzzExecution.hs b/tests/FuzzExecution.hs index ffe126a88..dd13bd444 100644 --- a/tests/FuzzExecution.hs +++ b/tests/FuzzExecution.hs @@ -31,7 +31,7 @@ fuzzExecution (SB init_state bindings) = do ioProperty (do config <- mkConfigTestIO - (ers, _) <- runG2WithConfig Nothing init_state config bindings + (ers, b) <- runG2WithConfig Nothing init_state config bindings mr <- runGhc (Just libdir) (do and <$> mapM (\er -> do @@ -46,7 +46,7 @@ fuzzExecution (SB init_state bindings) = do _ <- execStmt stmt execOptions return () Nothing -> return () - validateStatesGHC pg Nothing "call" [] er) ers + validateStatesGHC pg Nothing "call" [] b er) ers ) return $ not (null ers) ==> property mr) \ No newline at end of file From 8a7edbb72060d83a4213c05659a167b78830cc68 Mon Sep 17 00:00:00 2001 From: Bill Hallahan Date: Tue, 1 Oct 2024 21:07:00 -0400 Subject: [PATCH 05/10] Only coerce entry function if a newtype is wrapping a function --- src/G2/Initialization/MkCurrExpr.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/G2/Initialization/MkCurrExpr.hs b/src/G2/Initialization/MkCurrExpr.hs index 15dcd30ed..bc0267943 100644 --- a/src/G2/Initialization/MkCurrExpr.hs +++ b/src/G2/Initialization/MkCurrExpr.hs @@ -61,7 +61,8 @@ coerceRetNewTypes tenv e = if rt == c then (Nothing, e) else (Just coer, Cast e coer) where coerce_to t | TyCon n _:ts <- unTyApp t - , Just (NewTyCon { bound_ids = bis, rep_type = rt }) <- HM.lookup n tenv = + , Just (NewTyCon { bound_ids = bis, rep_type = rt }) <- HM.lookup n tenv + , hasFuncType $ PresType rt = coerce_to $ foldl' (\rt_ (b, bt) -> retype b bt rt_) rt (zip bis ts) | otherwise = t From 61dd8fd754f8e7c68bd50c19510b8ffec842823e Mon Sep 17 00:00:00 2001 From: Bill Hallahan Date: Tue, 1 Oct 2024 22:24:42 -0400 Subject: [PATCH 06/10] Added config option --- src/G2/Config/Config.hs | 6 ++++++ src/G2/Initialization/MkCurrExpr.hs | 4 +++- src/G2/Liquid/Interface.hs | 3 ++- 3 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/G2/Config/Config.hs b/src/G2/Config/Config.hs index f57043b68..8a0823717 100644 --- a/src/G2/Config/Config.hs +++ b/src/G2/Config/Config.hs @@ -12,6 +12,7 @@ module G2.Config.Config ( Mode (..) , BoolDef (..) , InstTV (..) , ShowType (..) + , ExpandRetNewTypes (..) , mkConfig , mkConfigDirect @@ -60,6 +61,8 @@ data FpHandling = RealFP | RationalFP deriving (Eq, Show, Read) data NonRedPathCons = Nrpc | NoNrpc deriving (Eq, Show, Read) +data ExpandRetNewTypes = ExpandNT | NoExpandNT deriving (Eq, Show, Read) + type IncludePath = FilePath data Config = Config { @@ -86,6 +89,7 @@ data Config = Config { , timeLimit :: Int -- ^ Seconds , validate :: Bool -- ^ If True, run on G2's input, and check against expected output. , nrpc :: NonRedPathCons -- ^ Whether to execute using non reduced path constraints or not + , expand_ret_new_types :: ExpandRetNewTypes -- ^ Whether to expand returned new types wrapping a functions } mkConfig :: String -> Parser Config @@ -123,6 +127,7 @@ mkConfig homedir = Config Regular <> help "time limit, in seconds") <*> switch (long "validate" <> help "use GHC to automatically compile and run on generated inputs, and check that generated outputs are correct") <*> flag NoNrpc Nrpc (long "nrpc" <> help "execute with non reduced path constraints") + <*> pure ExpandNT mkBaseInclude :: String -> Parser [IncludePath] mkBaseInclude homedir = @@ -239,6 +244,7 @@ mkConfigDirect homedir as m = Config { , timeLimit = strArg "time" as m read 300 , validate = boolArg "validate" as m Off , nrpc = NoNrpc + , expand_ret_new_types = ExpandNT } baseIncludeDef :: FilePath -> [FilePath] diff --git a/src/G2/Initialization/MkCurrExpr.hs b/src/G2/Initialization/MkCurrExpr.hs index bc0267943..fea14e8d2 100644 --- a/src/G2/Initialization/MkCurrExpr.hs +++ b/src/G2/Initialization/MkCurrExpr.hs @@ -23,7 +23,9 @@ mkCurrExpr m_assume m_assert f@(Id (Name _ m_mod _ _) _) tc ng eenv tenv walkers Just ex -> let var_ex = Var (Id (idName f) (typeOf ex)) - (m_coer, coer_var_ex) = coerceRetNewTypes tenv var_ex + (m_coer, coer_var_ex) = if expand_ret_new_types config == ExpandNT + then coerceRetNewTypes tenv var_ex + else (Nothing, var_ex) -- -- We refind the type of f, because type synonyms get replaced during the initializaton, -- -- after we first got the type of f. diff --git a/src/G2/Liquid/Interface.hs b/src/G2/Liquid/Interface.hs index 56da82d84..732ec2eb5 100644 --- a/src/G2/Liquid/Interface.hs +++ b/src/G2/Liquid/Interface.hs @@ -87,6 +87,7 @@ import qualified Data.Text.IO as TI import G2.Language.Monad import G2.Language.Support (Bindings(input_coercion)) +import G2.Config.Config (Config(expand_ret_new_types), ExpandRetNewTypes (NoExpandNT)) data LHReturn = LHReturn { calledFunc :: FuncInfo , violating :: Maybe FuncInfo @@ -101,7 +102,7 @@ data FuncInfo = FuncInfo { func :: T.Text -- attempt to find counterexamples to the functions liquid type findCounterExamples :: [FilePath] -> [FilePath] -> T.Text -> Config -> LHConfig -> IO (([ExecRes AbstractedInfo], Bindings), Lang.Id) findCounterExamples proj fp entry config lhconfig = do - let config' = config { mode = Liquid, fp_handling = RationalFP } + let config' = config { mode = Liquid, fp_handling = RationalFP, expand_ret_new_types = NoExpandNT } lh_config <- getOpts [] From 1beadde15ef79cf9f387228eb3d03d6266988526 Mon Sep 17 00:00:00 2001 From: Bill Hallahan Date: Tue, 1 Oct 2024 22:43:01 -0400 Subject: [PATCH 07/10] Revert "Added config option" This reverts commit 61dd8fd754f8e7c68bd50c19510b8ffec842823e. --- src/G2/Config/Config.hs | 6 ------ src/G2/Initialization/MkCurrExpr.hs | 4 +--- src/G2/Liquid/Interface.hs | 3 +-- 3 files changed, 2 insertions(+), 11 deletions(-) diff --git a/src/G2/Config/Config.hs b/src/G2/Config/Config.hs index 8a0823717..f57043b68 100644 --- a/src/G2/Config/Config.hs +++ b/src/G2/Config/Config.hs @@ -12,7 +12,6 @@ module G2.Config.Config ( Mode (..) , BoolDef (..) , InstTV (..) , ShowType (..) - , ExpandRetNewTypes (..) , mkConfig , mkConfigDirect @@ -61,8 +60,6 @@ data FpHandling = RealFP | RationalFP deriving (Eq, Show, Read) data NonRedPathCons = Nrpc | NoNrpc deriving (Eq, Show, Read) -data ExpandRetNewTypes = ExpandNT | NoExpandNT deriving (Eq, Show, Read) - type IncludePath = FilePath data Config = Config { @@ -89,7 +86,6 @@ data Config = Config { , timeLimit :: Int -- ^ Seconds , validate :: Bool -- ^ If True, run on G2's input, and check against expected output. , nrpc :: NonRedPathCons -- ^ Whether to execute using non reduced path constraints or not - , expand_ret_new_types :: ExpandRetNewTypes -- ^ Whether to expand returned new types wrapping a functions } mkConfig :: String -> Parser Config @@ -127,7 +123,6 @@ mkConfig homedir = Config Regular <> help "time limit, in seconds") <*> switch (long "validate" <> help "use GHC to automatically compile and run on generated inputs, and check that generated outputs are correct") <*> flag NoNrpc Nrpc (long "nrpc" <> help "execute with non reduced path constraints") - <*> pure ExpandNT mkBaseInclude :: String -> Parser [IncludePath] mkBaseInclude homedir = @@ -244,7 +239,6 @@ mkConfigDirect homedir as m = Config { , timeLimit = strArg "time" as m read 300 , validate = boolArg "validate" as m Off , nrpc = NoNrpc - , expand_ret_new_types = ExpandNT } baseIncludeDef :: FilePath -> [FilePath] diff --git a/src/G2/Initialization/MkCurrExpr.hs b/src/G2/Initialization/MkCurrExpr.hs index fea14e8d2..bc0267943 100644 --- a/src/G2/Initialization/MkCurrExpr.hs +++ b/src/G2/Initialization/MkCurrExpr.hs @@ -23,9 +23,7 @@ mkCurrExpr m_assume m_assert f@(Id (Name _ m_mod _ _) _) tc ng eenv tenv walkers Just ex -> let var_ex = Var (Id (idName f) (typeOf ex)) - (m_coer, coer_var_ex) = if expand_ret_new_types config == ExpandNT - then coerceRetNewTypes tenv var_ex - else (Nothing, var_ex) + (m_coer, coer_var_ex) = coerceRetNewTypes tenv var_ex -- -- We refind the type of f, because type synonyms get replaced during the initializaton, -- -- after we first got the type of f. diff --git a/src/G2/Liquid/Interface.hs b/src/G2/Liquid/Interface.hs index 732ec2eb5..56da82d84 100644 --- a/src/G2/Liquid/Interface.hs +++ b/src/G2/Liquid/Interface.hs @@ -87,7 +87,6 @@ import qualified Data.Text.IO as TI import G2.Language.Monad import G2.Language.Support (Bindings(input_coercion)) -import G2.Config.Config (Config(expand_ret_new_types), ExpandRetNewTypes (NoExpandNT)) data LHReturn = LHReturn { calledFunc :: FuncInfo , violating :: Maybe FuncInfo @@ -102,7 +101,7 @@ data FuncInfo = FuncInfo { func :: T.Text -- attempt to find counterexamples to the functions liquid type findCounterExamples :: [FilePath] -> [FilePath] -> T.Text -> Config -> LHConfig -> IO (([ExecRes AbstractedInfo], Bindings), Lang.Id) findCounterExamples proj fp entry config lhconfig = do - let config' = config { mode = Liquid, fp_handling = RationalFP, expand_ret_new_types = NoExpandNT } + let config' = config { mode = Liquid, fp_handling = RationalFP } lh_config <- getOpts [] From eca8a69f484c3e6b42fee2915180197a3ffbc3a4 Mon Sep 17 00:00:00 2001 From: Bill Hallahan Date: Tue, 1 Oct 2024 23:11:08 -0400 Subject: [PATCH 08/10] Fixing handling of LH assumption arguments --- src/G2/Liquid/Conversion.hs | 2 ++ src/G2/Liquid/ConvertCurrExpr.hs | 3 ++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/G2/Liquid/Conversion.hs b/src/G2/Liquid/Conversion.hs index 5e3f3ae9f..1623999a8 100644 --- a/src/G2/Liquid/Conversion.hs +++ b/src/G2/Liquid/Conversion.hs @@ -44,6 +44,8 @@ import qualified Data.Map as M import Data.Maybe import qualified Data.Text as T +import Debug.Trace + -- | A mapping of TyVar Name's, to Id's for the LH dict's type LHDictMap = HM.HashMap Name Id diff --git a/src/G2/Liquid/ConvertCurrExpr.hs b/src/G2/Liquid/ConvertCurrExpr.hs index 88bba8405..a868d9c6f 100644 --- a/src/G2/Liquid/ConvertCurrExpr.hs +++ b/src/G2/Liquid/ConvertCurrExpr.hs @@ -204,10 +204,11 @@ addCurrExprAssumption ifi (Bindings {fixed_inputs = fi}) = do -- fi <- fixedInputs eenv <- exprEnv inames <- inputNames + let inames' = take (length $ argumentTypes ifi) inames lh <- mapM (lhTCDict' HM.empty) $ mapMaybe typeType fi' - let is = catMaybes (map (E.getIdFromName eenv) inames) + let is = catMaybes (map (E.getIdFromName eenv) inames') let (typs, ars) = span isType $ fi' ++ map Var is case assumpt of From 5899cbfbcbd1f3925a01840842495d39f65bd604 Mon Sep 17 00:00:00 2001 From: Bill Hallahan Date: Tue, 1 Oct 2024 23:38:52 -0400 Subject: [PATCH 09/10] Comment --- src/G2/Initialization/MkCurrExpr.hs | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/G2/Initialization/MkCurrExpr.hs b/src/G2/Initialization/MkCurrExpr.hs index bc0267943..f3a6e60f7 100644 --- a/src/G2/Initialization/MkCurrExpr.hs +++ b/src/G2/Initialization/MkCurrExpr.hs @@ -48,7 +48,19 @@ mkCurrExpr m_assume m_assert f@(Id (Name _ m_mod _ _) _) tc ng eenv tenv walkers in (let_ex, is, typsE, m_coer, ng'') Nothing -> error "mkCurrExpr: Bad Name" - +-- | If a function we are symbolically executing returns a newtype wrapping a function type, applies a coercion to the function. +-- For instance, given: +-- @ +-- newtype F = F (Int -> Int) + +-- f :: Int -> F +-- f y = F (\x -> x + y) +-- @ +-- +-- This allows symbolic execution to find an input/output example: +-- @ +-- ((coerce (f :: Int -> F)) :: Int -> Int -> Int) (0) (1) = 1 +-- @ coerceRetNewTypes :: TypeEnv -> Expr -> (Maybe Coercion, Expr) coerceRetNewTypes tenv e = let From b3ce5a4a687c8d7711c53d5d25d4c6e8cb7d5e39 Mon Sep 17 00:00:00 2001 From: Bill Hallahan Date: Wed, 2 Oct 2024 01:01:28 -0400 Subject: [PATCH 10/10] Fixing handling of newtypes with LH --- src/G2/Liquid/Conversion.hs | 2 -- src/G2/Liquid/G2Calls.hs | 4 +++- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/G2/Liquid/Conversion.hs b/src/G2/Liquid/Conversion.hs index 1623999a8..5e3f3ae9f 100644 --- a/src/G2/Liquid/Conversion.hs +++ b/src/G2/Liquid/Conversion.hs @@ -44,8 +44,6 @@ import qualified Data.Map as M import Data.Maybe import qualified Data.Text as T -import Debug.Trace - -- | A mapping of TyVar Name's, to Id's for the LH dict's type LHDictMap = HM.HashMap Name Id diff --git a/src/G2/Liquid/G2Calls.hs b/src/G2/Liquid/G2Calls.hs index 6406a8de5..1ed859931 100644 --- a/src/G2/Liquid/G2Calls.hs +++ b/src/G2/Liquid/G2Calls.hs @@ -167,7 +167,9 @@ getAbstracted :: (Solver solver, Simplifier simplifier) getAbstracted g2call solver simplifier share s bindings abs_fc@(FuncCall { funcName = n, arguments = ars }) | Just e <- E.lookup n $ expr_env s = do let - e' = mkApp $ Var (Id n (typeOf e)):ars + v = Var (Id n (typeOf e)) + v' = maybe v (Cast v) (input_coercion bindings) + e' = mkApp $ v':ars ds = deepseq_walkers bindings strict_call = maybe e' (fillLHDictArgs ds) $ mkStrict_maybe ds e'