------------------------------------------------------------------------------
--- The definition of call types and an operation to infer them.
---
--- @author Michael Hanus
--- @version January 2024
------------------------------------------------------------------------------
module Verify.CallTypes where
import Data.List
import Analysis.TermDomain ( TermDomain(..), litAsCons )
import FlatCurry.Goodies
import FlatCurry.Types
import FlatCurry.Build ( pre )
import Verify.Helpers
import Verify.Options
import Verify.ProgInfo
------------------------------------------------------------------------------
--- A call type is intended to specify the conditions on arguments
--- so that a function call satisfying the call type is reducible
--- (i.e., some rule matches).
---
--- A call type is either `AnyT` (any term matches) or a list of
--- possible constructors with their argument call types.
--- Note that literals `l` are represented as `MCons [(("",l),[])]`.
--- This also implies that their siblings are unknown.
data CallType = AnyT | MCons [(QName,[CallType])]
deriving (Eq,Read,Show)
--- The call type of an operation which has no non-failing arguments.
failCallType :: [[CallType]]
failCallType = []
--- Is the call type a failure call type?
isFailCallType :: [[CallType]] -> Bool
isFailCallType = null
-- Shows a call type in a prettier way.
prettyCT :: CallType -> String
prettyCT AnyT = "_"
prettyCT (MCons cs) = "{" ++ intercalate " | " (map prettyC cs) ++ "}"
where
prettyC (qc,args) = snd qc ++ prettyArgs args
prettyArgs [] = ""
prettyArgs args@(_:_) = "(" ++ intercalate "," (map prettyCT args) ++ ")"
prettyFunCallTypes :: [[CallType]] -> String
prettyFunCallTypes cts =
if isFailCallType cts
then ""
else intercalate " | " $ map prettyCallTypeArgs cts
prettyCallTypeArgs :: [CallType] -> String
prettyCallTypeArgs cts = case cts of
[] -> "()"
[ct] -> prettyCT ct
_ -> "(" ++ intercalate ", " (map prettyCT cts) ++ ")"
--- Simplify call types by recursively transforming each complete
--- list of constructors with `AnyT` arguments to `AnyT`.
simpFuncCallType :: [(QName,ConsInfo)] -> [[CallType]] -> [[CallType]]
simpFuncCallType consinfos ctss =
let ctss' = foldr addCTArgs [] (map (map simpCallType) ctss)
in if ctss' == ctss then ctss
else simpFuncCallType consinfos ctss'
where
simpCallType AnyT = AnyT
simpCallType (MCons qcts) =
complete2Any (map (\ (qc,cts) -> (qc, map simpCallType cts)) qcts)
where
complete2Any [] = MCons []
complete2Any cs@(_:_)
| all (== AnyT) (concatMap snd cs) && -- all arguments AnyT?
isCompleteConstructorList consinfos (map fst cs)
= AnyT
| otherwise = MCons cs
-- Join two call types.
joinCT :: CallType -> CallType -> CallType
joinCT AnyT ct = ct
joinCT (MCons tcs1) AnyT = MCons tcs1
joinCT (MCons tcs1) (MCons tcs2) =
MCons (intersect tcs1 tcs2) --TODO: refine
-- Least-upper bound (union) of call types.
unionCT :: CallType -> CallType -> CallType
unionCT AnyT _ = AnyT
unionCT (MCons _) AnyT = AnyT
unionCT (MCons m1) (MCons m2) = MCons (foldr insertCT m1 m2)
where
--- Least-upper bound (union) on lists of argument call types.
unionCTs :: [[CallType]] -> [[CallType]] -> [[CallType]]
unionCTs cts1 cts2 = foldr addCTArgs cts1 cts2
--- Adds a new list of argument types to a given list of alternative arg types
addCTArgs :: [CallType] -> [[CallType]] -> [[CallType]]
addCTArgs cts0 [] = [cts0]
addCTArgs cts0 (cts:mcts)
| diffs == 0 = cts : mcts
| diffs > 1 = cts0 : cts : mcts
| otherwise = combineOneDiffCT cts0 cts : mcts
where
diffs = numDiffs cts0 cts -- number of different arguments
--- Combine to argument call types having exact one different argument.
combineOneDiffCT :: [CallType] -> [CallType] -> [CallType]
combineOneDiffCT [] [] = []
combineOneDiffCT [] (_:_) = error "combineOneDiffCT: inconsistent arguments"
combineOneDiffCT (_:_) [] = error "combineOneDiffCT: inconsistent arguments"
combineOneDiffCT (ct1:cts1) (ct2:cts2)
| ct1 == ct2 = ct1 : combineOneDiffCT cts1 cts2
| otherwise = unionCT ct1 ct2 : cts1
-- Insert a call constructor with arguments into a given list of cons types.
insertCT :: (QName,[CallType]) -> [(QName,[CallType])] -> [(QName,[CallType])]
insertCT (qc,qcas) [] = [(qc,qcas)]
insertCT (qc,qcas) ((qc1,qc1as) : mcs)
| qc == qc1
= if diffs == 0 then (qc, qcas) : mcs
else if diffs > 1
then (qc,qcas) : (qc,qc1as) : mcs -- cannot combine
else (qc, combineOneDiffCT qcas qc1as) : mcs
| otherwise = (qc1,qc1as) : insertCT (qc,qcas) mcs
where
diffs = numDiffs qcas qc1as -- number of different arguments
--- Count the number of pairwise different elements in a list.
numDiffs :: Eq a => [a] -> [a] -> Int
numDiffs xs ys = sum (map (\ (x,y) -> if x == y then 0 else 1) (zip xs ys))
-- Describes a list of alternative call types a totally reducible operation?
isTotalCallType :: [[CallType]] -> Bool
isTotalCallType cts = not (null cts) && all (all (==AnyT)) cts
------------------------------------------------------------------------------
--- Adds a constructor with a given arity at a position
--- to a given list of argument call types.
addCons2CT :: QName -> Int -> Pos -> [CallType] -> [CallType]
addCons2CT _ _ [] _ = error "addCons2CT: try to add constructor at root"
addCons2CT qc ar (p:ps) cts = replace (addConsInCT qc ar ps (cts!!p)) p cts
addConsInCT :: QName -> Int -> Pos -> CallType -> CallType
addConsInCT qc ar [] ct =
joinCT ct (MCons [(qc, take ar (repeat AnyT))])
addConsInCT qc ar (p:ps) (MCons tcs) =
MCons (map (\ (c,ts) -> (c, addCons2CT qc ar (p:ps) ts)) tcs)
addConsInCT qc _ (p:ps) AnyT =
error $ "addCons2CT: deep position " ++ show (p:ps) ++
" occurred for constructor " ++ snd qc ++ " in AnyT"
testAddCons2CT1 :: [CallType]
testAddCons2CT1 = addCons2CT (pre "[]") 0 [1] [AnyT,AnyT]
testAddCons2CT2 :: [CallType]
testAddCons2CT2 = addCons2CT (pre ":") 2 [0] [AnyT,AnyT]
------------------------------------------------------------------------------
-- The implementation of an anlysis to get the call types of an operation.
-- This is useful to infer nonfailing conditions w.r.t. standard types.
--- The state passed to compute call types contains a mapping from
--- variables (indices) to their positions and the call type of the
--- current branch of the operation to be analyzed.
data CallTypeState = CallTypeState
{ ctstCurrFunc :: QName -- the name of the current function
, ctstVarPos :: [(Int,Pos)]
, ctstCallType :: [CallType]
, ctstToolOpts :: Options
}
initCallTypeState :: Options -> QName -> [Int] -> CallTypeState
initCallTypeState opts qf vs =
CallTypeState qf (zip vs (map (\i -> [i]) [0..]))
(take (length vs) (repeat AnyT)) opts
--- Computes the call type of a function where all constructors are
--- provided as the second argument.
--- The computed call type for an `n`-ary function is a disjunction
--- (represented as a list) of alternative call types
--- where each element in the disjunction is list of `n` call types for
--- each argument.
callTypeFunc :: Options -> [(QName,ConsInfo)] -> FuncDecl -> (QName,[[CallType]])
callTypeFunc opts consinfos (Func qf ar _ _ rule) =
maybe
(case rule of
External _ -> callTypeExternalFunc qf ar
Rule vs exp ->
if length vs /= ar
then error $ "Func " ++ show qf ++ ": inconsistent variables"
else (qf, simpFuncCallType consinfos
(callTypeExpr (initCallTypeState opts qf vs) exp)))
(\ct -> (qf,ct))
(lookup qf defaultCallTypes)
--- Some call types for predefined operations.
--- The fail call types for arithmetic operations could be improved
--- in the future by considering refined number types.
defaultCallTypes :: [(QName,[[CallType]])]
defaultCallTypes =
map (\qf -> (pre qf, failCallType))
[ "=:=", "=:<=", "=:<<="
, "div", "divFloat", "prim_divFloat", "divInt", "prim_divInt"
, "mod", "modInt", "prim_modInt"
, "quot", "quotInt", "prim_quotInt"
, "rem", "remInt", "prim_remInt"
, "_impl#div#Prelude.Integral#Prelude.Int"
, "_impl#mod#Prelude.Integral#Prelude.Int"
, "_impl#quot#Prelude.Integral#Prelude.Int"
, "_impl#rem#Prelude.Integral#Prelude.Int"
, "_impl#/#Prelude.Fractional#Prelude.Float", "/"
, "sqrt", "sqrtFloat", "prim_sqrtFloat"
, "_impl#sqrt#Prelude.Floating#Prelude.Float"
-- TODO: extend to further float operations, like log, asin,...
] ++
[ (pre "&", [[MCons [(pre "True",[])], MCons [(pre "True",[])]]])
, (pre "cond",[[MCons [(pre "True",[])], AnyT]])
, (pre "aValueChar",[[]])
]
--- Computes the call type of an external (primitive) function.
--- Currently, we assume that they are total functions.
callTypeExternalFunc :: QName -> Int -> (QName,[[CallType]])
callTypeExternalFunc qf ar
| qf == pre "failed" = (qf, [])
| otherwise = (qf, [take ar (repeat AnyT)])
-- Add new variables not occurring in the left-hand side:
addFreshVars :: [Int] -> CallTypeState -> CallTypeState
addFreshVars vs ctst =
ctst { ctstVarPos = ctstVarPos ctst ++ map (\vi -> (vi, freshVarPos)) vs }
callTypeExpr :: CallTypeState -> Expr -> [[CallType]]
callTypeExpr ctst exp = case exp of
Var _ -> [ctstCallType ctst]
Lit _ -> [ctstCallType ctst]
Comb _ _ _ -> [ctstCallType ctst]
Let bs e -> callTypeExpr (addFreshVars (map fst bs) ctst) e
Free vs e -> callTypeExpr (addFreshVars vs ctst) e
Or e1 e2 -> unionCTs (callTypeExpr ctst e1) (callTypeExpr ctst e2)
Case _ ce bs ->
case ce of
Var v -> foldr1 unionCTs
(map (\ (Branch p e) ->
callTypeExpr (addVarBranchPattern v p) e)
(filter (not . isFailedBranch) bs))
_ -> foldr1 unionCTs
(map (\ (Branch p e) ->
callTypeExpr (addBranchPattern p) e)
(filter (not . isFailedBranch) bs))
Typed e _ -> callTypeExpr ctst e
where
varNotFound v = error $ "Function " ++ snd (ctstCurrFunc ctst) ++
": variable " ++ show v ++ " not found"
isFailedBranch (Branch _ e) = case e of
Comb FuncCall qf _ -> qf == pre "failed" ||
(optError (ctstToolOpts ctst) && qf == pre "error")
_ -> False
addVarBranchPattern v pat
| isFreshVarPos vpos
= -- since the variable is fresh, we cannot specialize the call type
addFreshVars (patternArgs pat) ctst
| otherwise
= case pat of
Pattern qc vs -> ctst { ctstCallType = addCons2CT qc (length vs) vpos
(ctstCallType ctst)
, ctstVarPos = ctstVarPos ctst ++
map (\ (vi,i) -> (vi, vpos ++ [i]))
(zip vs [0..]) }
LPattern lit -> ctst { ctstCallType = addCons2CT (litAsCons lit) 0 vpos
(ctstCallType ctst) }
where vpos = maybe (varNotFound v) id (lookup v (ctstVarPos ctst))
addBranchPattern (Pattern _ vs) = addFreshVars vs ctst
addBranchPattern (LPattern _) = ctst
------------------------------------------------------------------------------
-- An abstract call type of an operation (parameterized over the abstract
-- domain) is either `Nothing` in case of an always failing operation,
-- or just a list of abstract types for the arguments.
-- In the following we provide some operations on abstract call types.
type ACallType a = Maybe [a]
--- Transforms a call type for an operation, i.e., a disjunction of a list
--- of alternative call types for the arguments, into an abstract call type.
--- Since the abstract call type of an operation is a single list of abstract
--- call types for the arguments so that a disjunction of argument lists
--- cannot be expressed, the disjunctions are joined (i.e., intersected).
funcCallType2AType :: TermDomain a => [(QName,ConsInfo)] -> (QName, [[CallType]])
-> (QName, ACallType a)
funcCallType2AType consinfos (qn,fct) =
(qn, if null fct
then failACallType
else foldr1 joinACallType (map callTypes2ATypes fct))
where
callTypes2ATypes cts = let ats = map callType2AType cts
in if any isEmptyType ats
then Nothing
else Just (map (normalizeAType consinfos) ats)
callType2AType AnyT = anyType
callType2AType (MCons cs) =
let cats = map (\(qc,cts) -> ((qc, length cts),
aCons qc (map callType2AType cts))) cs
in if isCompleteConstructorList consinfos (map fst cs) &&
all isAnyType -- are all abstract constructor arguments any type?
(concatMap (\((qc,ar),aqc) -> argTypesOfCons qc ar aqc) cats)
then anyType
else foldr lubType emptyType (map snd cats)
--- Normalize an abstract type by recursively replacing complete sets of
--- constructors with `anyType` arguments by `anyType`.
--- Note that this works only for abstract values which are depth-bounded,
--- i.e., not for regular types. Thus, this operation might be better moved
--- into the implementation of a particular abstract domain.
normalizeAType :: TermDomain a => [(QName,ConsInfo)] -> a -> a
normalizeAType consinfos at =
let cs = consOfType at
cats = map (\qc -> (qc, map (normalizeAType consinfos)
(argTypesOfCons qc 0 at))) cs
in if null cs
then at
else if isCompleteConstructorList consinfos cs &&
all isAnyType -- are all constructor arguments any type?
(concatMap snd cats)
then anyType
else foldr lubType emptyType
(map (\(qc,ats) -> aCons qc ats) cats)
-- Describes an abstract call type a totally reducible operation?
isTotalACallType :: TermDomain a => ACallType a -> Bool
isTotalACallType Nothing = False
isTotalACallType (Just ats) = all isAnyType ats
--- The call type of an operation which has no non-failing arguments
--- expressible by call types for the arguments.
failACallType :: TermDomain a => ACallType a
failACallType = Nothing
--- Is the call type a failure call type?
isFailACallType :: TermDomain a => ACallType a -> Bool
isFailACallType Nothing = True
isFailACallType (Just _) = False
-- Pretty print an abstract call type for an operation.
prettyFunCallAType :: TermDomain a => ACallType a -> String
prettyFunCallAType Nothing = ""
prettyFunCallAType (Just ats) = case ats of
[] -> "()"
[at] -> showType at
_ -> "(" ++ intercalate ", " (map showType ats) ++ ")"
--- Join two abstract call types.
joinACallType :: TermDomain a => ACallType a -> ACallType a -> ACallType a
joinACallType Nothing _ = Nothing
joinACallType (Just _) Nothing = Nothing
joinACallType (Just ats1) (Just ats2) =
let ats = map (uncurry joinType) (zip ats1 ats2)
in if any isEmptyType ats then Nothing
else Just ats
--- Is a list of abstract call types (first argument) a subtype of
--- the call type of an operation (second argument)?
subtypeOfRequiredCallType :: TermDomain a => [a] -> ACallType a -> Bool
subtypeOfRequiredCallType _ Nothing = False
subtypeOfRequiredCallType ats (Just rats) =
all (uncurry isSubtypeOf) (zip ats rats)
--- Is an abstract type `at1` a subtype of another abstract type `at2`?
--- Thus, are all values described by `at1` contained in the set of
--- values described by `at2`?
isSubtypeOf :: TermDomain a => a -> a -> Bool
isSubtypeOf at1 at2 = joinType at1 at2 == at1
------------------------------------------------------------------------------
--- Is it possible to specialize the abstract types of the given
--- argument variables so that their type is a subtype of the
--- function call type given in the second argument?
--- If yes, the specialized argument variable types are returned.
specializeToRequiredType :: TermDomain a => [(Int,a)] -> ACallType a
-> Maybe [(Int,a)]
specializeToRequiredType _ Nothing = Nothing
specializeToRequiredType ats (Just cts) =
let newtypes = map (uncurry joinType) (zip (map snd ats) cts)
in if any isEmptyType newtypes
then Nothing
else Just (zip (map fst ats) newtypes)
------------------------------------------------------------------------------