Allow input function calls to be wrapped in coercions

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

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)

src/G2/Initialization/MkCurrExpr.hs

@@ -17,28 +17,22 @@
 
 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,8 +46,41 @@
 
  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"
+-- | 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
+ 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
+ , hasFuncType $ PresType rt = 
+ 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 =
@@ -80,13 +107,13 @@
  _ -> False
  (ats,nts) = partition anontype argts 
  -- We want to have symbolic types so we grab the type level arguments and introduce symbolic variables for them
  ns = map (\(NamedType (Id n _)) -> n) nts
  (ns', ng') = renameAll ns ng
 
  ntmap = HM.fromList $ zip ns ns' 
  -- We want to create a full list of symoblic variables with new names and put the symbolic variables into the expr env
  -- Type level arguments
  ntids = map (\(NamedType i) -> i) nts
  ntids' = renames ntmap ntids
 
  -- Value level arguments

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

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
 

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]

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

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'

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

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
  }
  }
 

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
 

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,16 +96,16 @@ 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
  . updatePGValAndTypeNames out
  $ 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

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)