{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TupleSections #-} module G2.Liquid.Interface ( LiquidData (..) , LiquidReadyState , lr_state , lr_binding , lrsMeasures , Abstracted (..) , AbstractedInfo (..) , findCounterExamples , runLHG2 , onlyMinimalStates , cleanupResults , runLHCore , liquidStateWithCall , liquidStateWithCall' , liquidStateFromSimpleStateWithCall , liquidStateFromSimpleStateWithCall' , cleanReadyState , fromLiquidNoCleaning , createLiquidReadyState , processLiquidReadyState , processLiquidReadyStateWithCall , extractWithoutSpecs , processLiquidReadyStateCleaning , reqNames , lhStateToCE , printLHOut , printCE) where import G2.Config.Config import G2.Translation import G2.Interface import G2.Language as Lang import G2.Language.KnownValues as KV import qualified G2.Language.ExprEnv as E import G2.Execution import G2.Initialization.MkCurrExpr import G2.Liquid.AddCFBranch import G2.Liquid.AddLHTC import G2.Liquid.AddOrdToNum import G2.Liquid.AddTyVars import G2.Liquid.Config import G2.Liquid.Conversion import G2.Liquid.ConvertCurrExpr import G2.Liquid.Helpers import G2.Liquid.LHReducers import G2.Liquid.Measures import G2.Liquid.MkLHVals import G2.Liquid.G2Calls import G2.Liquid.Simplify import G2.Liquid.SpecialAsserts import G2.Liquid.TCGen import G2.Liquid.TCValues import G2.Liquid.Types import G2.Liquid.TyVarBags import G2.Solver hiding (solve) import G2.Lib.Printers import Language.Haskell.Liquid.Types hiding (Config, cls, names, measures) import Language.Haskell.Liquid.UX.CmdLine hiding (config) import Control.Exception import Control.Monad.Extra import Control.Monad.IO.Class import qualified Control.Monad.State as SM import Data.List import qualified Data.HashSet as S import qualified Data.HashMap.Lazy as HM import qualified Data.Map as M import qualified Data.Text as T import qualified Data.Text.IO as TI import G2.Language.Monad data LHReturn = LHReturn { calledFunc :: FuncInfo , violating :: Maybe FuncInfo , abstracted :: [FuncInfo] } deriving (Eq, Show) data FuncInfo = FuncInfo { func :: T.Text , funcArgs :: T.Text , funcReturn :: T.Text } deriving (Eq, Show) -- | findCounterExamples -- Given (several) LH sources, and a string specifying a function name, -- 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 } lh_config <- getOpts [] ghci <- try $ getGHCInfos lh_config proj fp :: IO (Either SomeException [GhcInfo]) let ghci' = case ghci of Right g_c -> g_c Left e -> error $ "ERROR OCCURRED IN LIQUIDHASKELL\n" ++ show e tgt_trans <- translateLoaded proj fp (simplTranslationConfig { simpl = False }) config' runLHCore entry tgt_trans ghci' config' lhconfig runLHCore :: T.Text -> (Maybe T.Text, ExtractedG2) -> [GhcInfo] -> Config -> LHConfig -> IO (([ExecRes AbstractedInfo], Bindings), Lang.Id) runLHCore entry (mb_modname, exg2) ghci config lhconfig = do LiquidData { ls_state = final_st , ls_bindings = bindings , ls_id = ifi , ls_counterfactual_name = cfn , ls_memconfig = pres_names } <- liquidStateWithCall entry (mb_modname, exg2) ghci config lhconfig mempty SomeSolver solver <- initSolver config let simplifier = IdSimplifier let (red, hal, ord) = lhReducerHalterOrderer config lhconfig solver simplifier entry mb_modname cfn final_st (exec_res, final_bindings) <- SM.evalStateT (runLHG2 config red hal ord solver simplifier pres_names ifi final_st bindings) (mkPrettyGuide ()) close solver return ((exec_res, final_bindings), ifi) {-# INLINE liquidStateWithCall #-} liquidStateWithCall :: T.Text -> (Maybe T.Text, ExtractedG2) -> [GhcInfo] -> Config -> LHConfig -> MemConfig -> IO LiquidData liquidStateWithCall entry (mb_modname, exg2) ghci config lhconfig memconfig = liquidStateWithCall' entry (mb_modname, exg2) ghci config lhconfig memconfig (mkCurrExpr Nothing Nothing) mkArgTys {-# INLINE liquidStateWithCall' #-} liquidStateWithCall' :: T.Text -> (Maybe T.Text, ExtractedG2) -> [GhcInfo] -> Config -> LHConfig -> MemConfig -> (Lang.Id -> MkCurrExpr) -> (Lang.Expr -> MkArgTypes) -> IO LiquidData liquidStateWithCall' entry (mb_m, exg2) ghci config lhconfig memconfig mkCurr argTys = do let simp_s = initSimpleState exg2 liquidStateFromSimpleStateWithCall' simp_s ghci entry mb_m config lhconfig memconfig mkCurr argTys {-# INLINE liquidStateFromSimpleStateWithCall #-} liquidStateFromSimpleStateWithCall :: SimpleState -> [GhcInfo] -> T.Text -> Maybe T.Text -> Config -> LHConfig -> MemConfig -> IO LiquidData liquidStateFromSimpleStateWithCall simp_s ghci entry mb_m config lhconfig memconfig = liquidStateFromSimpleStateWithCall' simp_s ghci entry mb_m config lhconfig memconfig (mkCurrExpr Nothing Nothing) mkArgTys {-# INLINE liquidStateFromSimpleStateWithCall' #-} liquidStateFromSimpleStateWithCall' :: SimpleState -> [GhcInfo] -> T.Text -> Maybe T.Text -> Config -> LHConfig -> MemConfig -> (Lang.Id -> MkCurrExpr) -> (Lang.Expr -> MkArgTypes) -> IO LiquidData liquidStateFromSimpleStateWithCall' simp_s ghci entry mb_m config lhconfig memconfig mkCurr argTys = do let (simp_s', ph_tyvars) = if add_tyvars lhconfig then fmap Just $ addTyVarsEEnvTEnv simp_s else (simp_s, Nothing) (s, i, bindings') = initStateFromSimpleStateWithCall simp_s' True entry mb_m mkCurr argTys config fromLiquidReadyState s i bindings' ghci ph_tyvars lhconfig memconfig {-# INLINE fromLiquidReadyState #-} fromLiquidReadyState :: State () -> Lang.Id -> Bindings -> [GhcInfo] -> Maybe PhantomTyVars -> LHConfig -> MemConfig -> IO LiquidData fromLiquidReadyState init_state ifi bindings ghci ph_tyvars lhconfig memconfig = do let (init_state', bindings') = (markAndSweepPreserving (reqNames init_state `mappend` memconfig) init_state bindings) cleaned_state = init_state' { type_env = type_env init_state } fromLiquidNoCleaning cleaned_state ifi bindings' ghci ph_tyvars lhconfig memconfig data LiquidReadyState = LiquidReadyState { lr_state :: LHState , lr_binding :: Bindings , lr_known_values :: KnownValues , lr_type_classes :: TypeClasses , lr_higher_ord_insts :: S.HashSet Name } data LiquidData = LiquidData { ls_state :: State LHTracker , ls_bindings :: Bindings , ls_id :: Lang.Id , ls_counterfactual_name :: CounterfactualName , ls_counterfactual_funcs :: S.HashSet Name , ls_measures :: Measures , ls_assumptions :: Assumptions , ls_posts :: Posts , ls_tcv :: TCValues , ls_memconfig :: MemConfig } cleanReadyState :: LiquidReadyState -> MemConfig -> LiquidReadyState cleanReadyState lrs@(LiquidReadyState { lr_state = lhs@(LHState { state = s }), lr_binding = b }) memconfig = let (s', b') = (markAndSweepPreserving (reqNames s `mappend` memconfig) s b) s'' = s' { type_env = type_env s } in lrs { lr_state = lhs { state = s'' }, lr_binding = b' } fromLiquidNoCleaning :: State () -> Lang.Id -> Bindings -> [GhcInfo] -> Maybe PhantomTyVars -> LHConfig -> MemConfig -> IO LiquidData fromLiquidNoCleaning init_state ifi bindings ghci ph_tyvars lhconfig memconfig = do let lrs = createLiquidReadyState init_state bindings ghci ph_tyvars lhconfig processLiquidReadyState lrs ifi ghci lhconfig memconfig createLiquidReadyState :: State () -> Bindings -> [GhcInfo] -> Maybe PhantomTyVars -> LHConfig -> LiquidReadyState createLiquidReadyState s bindings ghci ph_tyvars lhconfig = let np_ng = name_gen bindings (meenv, mkv, mtc, minst, mexported, ng') = mkLHVals s (higher_order_inst bindings) (exported_funcs bindings) np_ng s' = s { track = [] } bindings' = bindings { exported_funcs = mexported ++ exported_funcs bindings, name_gen = ng' } (lh_state, lh_bindings) = createLHState meenv mkv mtc s' bindings' (data_state, data_bindings) = execLHStateM (initializeLHData ghci ph_tyvars lhconfig) lh_state lh_bindings in LiquidReadyState { lr_state = data_state , lr_binding = data_bindings , lr_known_values = mkv , lr_type_classes = mtc , lr_higher_ord_insts = minst } -- (mkv, mtc, minst, data_state, data_bindings) processLiquidReadyStateCleaning :: LiquidReadyState -> Lang.Id -> [GhcInfo] -> LHConfig -> MemConfig -> IO LiquidData processLiquidReadyStateCleaning lrs ifi ghci lhconfig memconfig = let lrs' = cleanReadyState lrs memconfig in processLiquidReadyState lrs' ifi ghci lhconfig memconfig processLiquidReadyState :: LiquidReadyState -> Lang.Id -> [GhcInfo] -> LHConfig -> MemConfig -> IO LiquidData processLiquidReadyState lrs@(LiquidReadyState { lr_state = lh_state , lr_binding = lh_bindings }) ifi ghci lhconfig memconfig = do let ((cfn, mc, cff), (merged_state, bindings')) = runLHStateM (initializeLHSpecs (counterfactual lhconfig) ghci ifi lh_bindings) lh_state lh_bindings lrs' = lrs { lr_state = merged_state, lr_binding = bindings'} lhs <- extractWithoutSpecs lrs' ifi ghci memconfig let lh_s = if only_top lhconfig then elimNonTop (S.insert (idName mc) cff) (ls_state lhs) else ls_state lhs return $ lhs { ls_state = lh_s , ls_id = mc , ls_counterfactual_name = cfn , ls_counterfactual_funcs = cff } extractWithoutSpecs :: LiquidReadyState -> Lang.Id -> [GhcInfo] -> MemConfig -> IO LiquidData extractWithoutSpecs lrs@(LiquidReadyState { lr_state = s , lr_binding = bindings , lr_known_values = mkv , lr_type_classes = mtc , lr_higher_ord_insts = minst}) ifi ghci memconfig = do let (lh_s, bindings') = execLHStateM (return ()) s bindings let bindings'' = bindings' { higher_order_inst = minst } let tcv = tcvalues lh_s let lh_s' = deconsLHState lh_s let annm = annots lh_s pres_names = addSearchNames (namesList tcv ++ namesList mkv) $ reqNames lh_s' pres_names' = addSearchNames (namesList annm) pres_names let track_state = lh_s' {track = LHTracker { abstract_calls = [] , last_var = Nothing , annotations = annm , all_calls = [] , higher_order_calls = [] } } -- We replace certain function name lists in the final State with names -- mapping into the measures from the LHState. These functions do not -- need to be passed the LH typeclass, so this ensures use of Names from -- these lists will work, without us having to modify all of G2 to account -- for the LH typeclass. let final_st = track_state { known_values = mkv , type_classes = unionTypeClasses mtc (type_classes track_state)} let real_meas = lrsMeasures ghci lrs return $ LiquidData { ls_state = final_st , ls_bindings = bindings'' , ls_id = ifi , ls_counterfactual_name = error "No counterfactual name" , ls_counterfactual_funcs = error "No counterfactual funcs" , ls_measures = real_meas , ls_assumptions = assumptions lh_s , ls_posts = posts lh_s , ls_tcv = tcv , ls_memconfig = pres_names' `mappend` memconfig } lrsMeasures :: [GhcInfo] -> LiquidReadyState -> Measures lrsMeasures ghci lrs = let meas_names = measureNames ghci meas_nameOcc = map (\(Name n md _ _) -> (n, md)) $ map symbolName meas_names real_meas = E.filterWithKey (\(Name n md i _) _ -> (n, md) `elem` meas_nameOcc && i == 0) . measures $ lr_state lrs in real_meas processLiquidReadyStateWithCall :: LiquidReadyState -> [GhcInfo] -> T.Text -> Maybe T.Text -> Config -> LHConfig -> MemConfig -> IO LiquidData processLiquidReadyStateWithCall lrs@(LiquidReadyState { lr_state = lhs@(LHState { state = s }) , lr_binding = bindings}) ghci f m_mod config lhconfig memconfig = do let (ie, _) = case findFunc f m_mod (expr_env s) of Left ie' -> ie' Right errs -> error errs (ce, is, f_i, 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 , curr_expr = CurrExpr Evaluate ce } } (lhs'', bindings') = execLHStateM (addLHTCCurrExpr) lhs' (bindings { name_gen = ng' }) lrs' = lrs { lr_state = lhs'' , lr_binding = bindings' { fixed_inputs = f_i , input_names = map idName is } } processLiquidReadyStateCleaning lrs' ie ghci lhconfig memconfig runLHG2 :: (MonadIO m, Solver solver, Simplifier simplifier) => Config -> SomeReducer m LHTracker -> SomeHalter m LHTracker -> SomeOrderer m LHTracker -> solver -> simplifier -> MemConfig -> Lang.Id -> State LHTracker -> Bindings -> m ([ExecRes AbstractedInfo], Bindings) runLHG2 config red hal ord solver simplifier pres_names init_id final_st bindings = do let only_abs_st = addTicksToDeepSeqCases (deepseq_walkers bindings) final_st (ret, final_bindings) <- runG2WithSomes red hal ord solver simplifier pres_names only_abs_st bindings let ret' = onlyMinimalStates ret cleanupResults solver simplifier config init_id final_st final_bindings ret' onlyMinimalStates :: [ExecRes LHTracker] -> [ExecRes LHTracker] onlyMinimalStates ers = let mi = case length ers of 0 -> 0 _ -> minimum $ map (\(ExecRes {final_state = s}) -> abstractCallsNum s) ers in filter (\(ExecRes {final_state = s}) -> mi == (abstractCallsNum s)) ers cleanupResults :: (MonadIO m, Solver solver, Simplifier simplifier) => solver -> simplifier -> Config -> Lang.Id -> State LHTracker -> Bindings -> [ExecRes LHTracker] -> m ([ExecRes AbstractedInfo], Bindings) cleanupResults solver simplifier config init_id init_state bindings ers = do let ers2 = map (\er -> er { final_state = putSymbolicExistentialInstInExprEnv (final_state er) }) ers ers3 = map (\er -> if fmap funcName (violated er) == Just initiallyCalledFuncName then er { violated = Nothing } else er) ers2 (bindings', ers4) <- liftIO $ mapAccumM (reduceCalls runG2WithSomes solver simplifier config) bindings ers3 ers5 <- liftIO $ mapM (checkAbstracted runG2WithSomes solver simplifier config init_id bindings') ers4 let ers6 = map (\er@(ExecRes { final_state = s }) -> (er { final_state = s {track = mapAbstractedInfoFCs (subVarFuncCall True (model s) (expr_env init_state) (type_classes s)) $ track s } })) ers5 return (ers6, bindings') lhReducerHalterOrderer :: (MonadIO m, Solver solver, Simplifier simplifier) => Config -> LHConfig -> solver -> simplifier -> T.Text -> Maybe T.Text -> CounterfactualName -> State t -> ( SomeReducer (SM.StateT PrettyGuide m) LHTracker , SomeHalter (SM.StateT PrettyGuide m) LHTracker , SomeOrderer (SM.StateT PrettyGuide m) LHTracker) lhReducerHalterOrderer config lhconfig solver simplifier entry mb_modname cfn st = let share = sharing config state_name = Name "state" Nothing 0 Nothing abs_ret_name = Name "abs_ret" Nothing 0 Nothing non_red = nonRedPCRed .|. nonRedPCRedConst m_logger = fmap SomeReducer $ getLogger config lh_std_red = existentialInstRed :== NoProgress .--> lhRed cfn :== Finished --> stdRed share retReplaceSymbFuncVar solver simplifier opt_logger_red = case m_logger of Just logger -> logger .~> lh_std_red Nothing -> lh_std_red in if higherOrderSolver config == AllFuncs then (opt_logger_red .== Finished .--> (taggerRed abs_ret_name :== Finished --> nonRedAbstractReturnsRed) .== Finished .--> SomeReducer non_red , SomeHalter (maxOutputsHalter (maxOutputs config) <~> zeroHalter (steps config) <~> lhAbsHalter entry mb_modname (expr_env st) <~> lhLimitByAcceptedHalter (cut_off lhconfig) <~> switchEveryNHalter (switch_after lhconfig) <~> lhAcceptIfViolatedHalter) , SomeOrderer lhLimitByAcceptedOrderer) else (opt_logger_red .== Finished .--> ((taggerRed state_name :== Finished --> non_red)) .== Finished .--> (taggerRed abs_ret_name :== Finished --> nonRedAbstractReturnsRed) , SomeHalter (discardIfAcceptedTagHalter state_name <~> discardIfAcceptedTagHalter abs_ret_name <~> maxOutputsHalter (maxOutputs config) <~> zeroHalter (steps config) <~> lhAbsHalter entry mb_modname (expr_env st) <~> lhLimitByAcceptedHalter (cut_off lhconfig) <~> switchEveryNHalter (switch_after lhconfig) <~> lhAcceptIfViolatedHalter) , SomeOrderer lhLimitByAcceptedOrderer) initializeLHData :: [GhcInfo] -> Maybe PhantomTyVars -> LHConfig -> LHStateM () initializeLHData ghcInfos m_ph_tyvars config = do addLHTC addOrdToNum addErrorAssumes config let lh_measures = measureSpecs ghcInfos meenv <- measuresM nt <- return . M.fromList =<< mapMaybeM measureTypeMappings lh_measures fil_meenv <- filterMeasures' meenv (M.keys nt) createMeasures lh_measures case m_ph_tyvars of Just ph_tyvars -> addTyVarsMeasures ph_tyvars Nothing -> return () meenv' <- measuresM putMeasuresM (fil_meenv `E.union` meenv') -- | Returns the name of the Tick on the counterfactual branches, and the names -- of all functions with counterfactual branches initializeLHSpecs :: Counterfactual -> [GhcInfo] -> Lang.Id -> Bindings -> LHStateM (Lang.Name, Lang.Id, S.HashSet Lang.Name) initializeLHSpecs counter ghcInfos ifi bindings = do let specs = funcSpecs ghcInfos mergeLHSpecState specs addSpecialAsserts addTrueAsserts (idName ifi) -- Most of the simplification works less well on some of the Core generated by convertCurrExpr, -- so we apply the simplification first. However, we do want to stamp out as much redundancy -- from convertCurrExpr as we can, so we do further simplificiation after simplify (main_call, ns) <- convertCurrExpr ifi bindings furtherSimplifyCurrExpr (cfn, ns') <- case counter of Counterfactual cf_mods -> return . (,ns) =<< addCounterfactualBranch cf_mods ns NotCounterfactual -> return (Name "" Nothing 0 Nothing, []) mapME (return . flattenLets) return (cfn, main_call, S.fromList ns') reqNames :: State t -> MemConfig reqNames (State { expr_env = eenv , type_env = tenv , type_classes = tc , known_values = kv}) = let ns = Lang.namesList [ mkGe kv eenv , mkGt kv eenv , mkEq kv eenv , mkNeq kv eenv , mkLt kv eenv , mkLe kv eenv , mkAnd kv eenv , mkOr kv eenv , mkNot kv eenv , mkPlus kv eenv , mkMinus kv eenv , mkMult kv eenv -- , mkDiv kv eenv , mkMod kv eenv , mkNegate kv eenv , mkImplies kv eenv , mkIff kv eenv , mkFromInteger kv eenv -- , mkToInteger kv eenv , mkJust kv tenv , mkNothing kv tenv , mkUnit kv tenv , mkIntegralExtactReal kv , mkRealExtractNum kv ] ++ Lang.namesList (HM.filterWithKey (\k _ -> k == eqTC kv || k == numTC kv || k == ordTC kv || k == integralTC kv || k == fractionalTC kv) (toMap tc) ) ++ Lang.namesList (filter (\(Name _ m _ _) -> m == Just "Data.Set.Internal") (E.keys eenv)) in MemConfig { search_names = ns , pres_func = pf } where pf _ (Bindings { deepseq_walkers = dsw }) a = S.fromList . map idName . M.elems $ M.filterWithKey (\n _ -> n `S.member` a) dsw printLHOut :: Lang.Id -> [ExecRes AbstractedInfo] -> IO () printLHOut entry = mapM_ (\lhr -> do printParsedLHOut lhr; putStrLn "") . map (parseLHOut entry) printCE :: State t -> [CounterExample] -> IO () printCE s = mapM_ (\lhr -> do printParsedLHOut lhr; putStrLn "") . map (counterExampleToLHReturn s) printParsedLHOut :: LHReturn -> IO () printParsedLHOut (LHReturn { calledFunc = FuncInfo {func = f, funcArgs = call, funcReturn = output} , violating = Nothing , abstracted = abstr}) = do putStrLn "The call" TI.putStrLn $ call `T.append` " = " `T.append` output TI.putStrLn $ "violates " `T.append` f `T.append` "'s refinement type" printAbs abstr printParsedLHOut (LHReturn { calledFunc = FuncInfo {funcArgs = call, funcReturn = output} , violating = Just (FuncInfo {func = f, funcArgs = call', funcReturn = output'}) , abstracted = abstr }) = do TI.putStrLn $ call `T.append` " = " `T.append` output putStrLn "makes a call to" TI.putStrLn $ call' `T.append` " = " `T.append` output' TI.putStrLn $ "violating " `T.append` f `T.append` "'s refinement type" printAbs abstr printAbs :: [FuncInfo] -> IO () printAbs fi = do let fn = T.intercalate ", " $ map func fi if length fi > 0 then do putStrLn "if" mapM_ printFuncInfo fi if length fi > 1 then do TI.putStrLn $ "Strengthen the refinement types of " `T.append` fn `T.append` " to eliminate these possibilities" putStrLn "Abstract" else do TI.putStrLn $ "Strengthen the refinement type of " `T.append` fn `T.append` " to eliminate this possibility" putStrLn "Abstract" else putStrLn "Concrete" printFuncInfo :: FuncInfo -> IO () printFuncInfo (FuncInfo {funcArgs = call, funcReturn = output}) = TI.putStrLn $ call `T.append` " = " `T.append` output parseLHOut :: Lang.Id -> ExecRes AbstractedInfo -> LHReturn parseLHOut entry (ExecRes { final_state = s , conc_args = inArg , conc_out = ex , violated = ais}) = let called = funcCallToFuncInfo (printHaskell s) $ FuncCall { funcName = idName entry, arguments = inArg, returns = ex} viFunc = fmap (parseLHFuncTuple s) ais abstr = map (parseLHFuncTuple s) . map abstract . abs_calls $ track s in LHReturn { calledFunc = called , violating = viFunc , abstracted = abstr} counterExampleToLHReturn :: State t -> CounterExample -> LHReturn counterExampleToLHReturn s (DirectCounter fc abstr _) = let called = funcCallToFuncInfo (printHaskell s) . abstract $ fc abstr' = map (funcCallToFuncInfo (printHaskell s) . abstract) abstr in LHReturn { calledFunc = called , violating = Nothing , abstracted = abstr'} counterExampleToLHReturn s (CallsCounter fc viol_fc abstr _) = let called = funcCallToFuncInfo (printHaskell s) . abstract $ fc viol_called = funcCallToFuncInfo (printHaskell s) . abstract $ viol_fc abstr' = map (funcCallToFuncInfo (printHaskell s) . abstract) abstr in LHReturn { calledFunc = called , violating = Just viol_called , abstracted = abstr'} funcCallToFuncInfo :: (Expr -> T.Text) -> FuncCall -> FuncInfo funcCallToFuncInfo t (FuncCall { funcName = f, arguments = inArg, returns = ret }) = let funcCall = t . foldl (\a a' -> App a a') (Var (Id f TyUnknown)) $ inArg funcOut = t ret in FuncInfo {func = nameOcc f, funcArgs = funcCall, funcReturn = funcOut} lhStateToCE :: ExecRes AbstractedInfo -> CounterExample lhStateToCE (ExecRes { final_state = State { track = t } }) | Just c <- abs_violated t = CallsCounter (init_call t) c (abs_calls t) (ai_higher_order_calls t) | otherwise = DirectCounter (init_call t) (abs_calls t) (ai_higher_order_calls t) parseLHFuncTuple :: State t -> FuncCall -> FuncInfo parseLHFuncTuple s (FuncCall {funcName = n, arguments = ars, returns = out}) = let t = case fmap typeOf $ E.lookup n (expr_env s) of Just t' -> t' Nothing -> error $ "Unknown type for abstracted function " ++ show n in FuncInfo { func = nameOcc n , funcArgs = printHaskell s (foldl' App (Var (Id n t)) ars) , funcReturn = printHaskell s out }