hic-0.0.0.1: src/Language/Cimple/Analysis/OrderedSolver.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wno-unused-top-binds #-}
module Language.Cimple.Analysis.OrderedSolver
( OrderedSolverResult (..)
, runOrderedSolver
) where
import Control.Applicative ((<|>))
import Control.Monad (foldM, forM_,
void, when,
zipWithM_,
(<=<))
import Control.Monad.State.Strict (State, StateT,
evalState,
execState,
lift)
import qualified Control.Monad.State.Strict as State
import Data.Aeson (ToJSON)
import Data.Bifunctor (Bifunctor (..))
import Data.Fix (Fix (..),
foldFix,
unFix)
import Data.List (find, foldl',
nub)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe,
mapMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.Tree as Tree
import qualified Debug.Trace as Debug
import GHC.Generics (Generic)
import Language.Cimple (Lexeme (..))
import qualified Language.Cimple as C
import Language.Cimple.Analysis.CallGraphAnalysis (SccType (..))
import Language.Cimple.Analysis.ConstraintGeneration (Constraint (..),
ConstraintGenResult (..))
import Language.Cimple.Analysis.Errors (Context (..),
ErrorInfo (..),
MismatchReason (..),
Provenance (..),
TypeError (..))
import qualified Language.Cimple.Analysis.Pretty as P
import Language.Cimple.Analysis.TypeSystem (pattern Array, pattern BuiltinType,
pattern Const,
FullTemplate,
pattern FullTemplate,
FullTemplateF (..),
pattern Function,
pattern Nonnull,
pattern Nullable,
pattern Owner,
Phase (..),
pattern Pointer,
pattern Singleton,
pattern Sized,
StdType (..),
pattern Template,
TemplateId (..),
TypeDescr (..),
TypeInfo,
TypeInfoF (..),
TypeRef (..),
pattern TypeRef,
TypeSystem,
pattern Var,
pattern VarArg,
isPointerLike,
isVarArg,
isVoid,
stripAllWrappers,
templateIdBaseName,
templateIdToText,
unwrap)
import qualified Language.Cimple.Analysis.TypeSystem as TS
import qualified Language.Cimple.Analysis.TypeSystem.GraphSolver as GS
import qualified Language.Cimple.Analysis.TypeSystem.TypeGraph as TG
import qualified Language.Cimple.Analysis.TypeSystem.Unification as U
data OrderedSolverResult = OrderedSolverResult
{ osrErrors :: [ErrorInfo 'Local]
, osrInferredSigs :: Map Text (TypeInfo 'Local)
} deriving (Show, Generic)
instance ToJSON OrderedSolverResult
debugging :: Bool
debugging = False
dtraceM :: Monad m => String -> m ()
dtraceM msg = if debugging then Debug.traceM msg else return ()
data SolverState = SolverState
{ ssBindings :: Map (FullTemplate 'Local) (TypeInfo 'Local, Provenance 'Local)
, ssErrors :: [ErrorInfo 'Local]
, ssTypeSystem :: TypeSystem
, ssInferred :: Map Text (TypeInfo 'Local)
, ssFuncPhases :: Map Text Integer
, ssActivePhases :: Set Integer
, ssNextId :: Int
, ssFinalPass :: Bool
}
type Solver = State SolverState
runOrderedSolver :: TypeSystem -> [SccType] -> ConstraintGenResult -> OrderedSolverResult
runOrderedSolver ts sccs cgr =
let initialState = SolverState Map.empty [] ts Map.empty (cgrFuncPhases cgr) Set.empty 0 True
finalState = execState (mapM_ (solveScc (cgrConstraints cgr)) sccs) initialState
in OrderedSolverResult (ssErrors finalState) (ssInferred finalState)
solveScc :: Map Text [Constraint 'Local] -> SccType -> Solver ()
solveScc constrMap scc = do
dtraceM $ "Solving SCC: " ++ show scc
phases <- State.gets ssFuncPhases
let activePhases = case scc of
Acyclic func -> maybe Set.empty Set.singleton (Map.lookup func phases)
Cyclic funcs -> Set.fromList $ mapMaybe (`Map.lookup` phases) funcs
State.modify $ \s -> s { ssActivePhases = activePhases }
case scc of
Acyclic func -> do
State.modify $ \s -> s { ssFinalPass = True }
let constrs = Map.findWithDefault [] func constrMap
dtraceM $ "Solving Acyclic SCC " ++ show func ++ " with " ++ show (length constrs) ++ " constraints: " ++ show constrs
mapM_ solveConstraint constrs
captureSignature func
Cyclic funcs -> do
State.modify $ \s -> s { ssFinalPass = False }
let constrs = concatMap (\f -> Map.findWithDefault [] f constrMap) funcs
-- Structural Pass 1: Build initial structural bindings
mapM_ solveConstraint constrs
resolveBindings
-- Structural Pass 2: Resolve MemberAccess/Callable using Pass 1 info
mapM_ solveConstraint constrs
resolveBindings
-- Pass 3: Final propagation and settling
State.modify $ \s -> s { ssFinalPass = True }
mapM_ solveConstraint constrs
resolveBindings
mapM_ captureSignature funcs
-- | Resolves all current bindings co-inductively to their fixed points.
-- This replaces manual fixpoint loops with a structural recursion scheme (Anamorphism).
resolveBindings :: Solver ()
resolveBindings = do
bindings <- State.gets ssBindings
let graph = Map.map (\(ty, _) -> Set.singleton (TG.fromTypeInfo ty)) bindings
resolvedMap = GS.solveAll graph (Map.keys bindings)
State.modify $ \s -> s { ssBindings = Map.mapWithKey (\k (ty, prov) -> (maybe ty TG.toTypeInfo (Map.lookup k resolvedMap), prov)) (ssBindings s) }
captureSignature :: Text -> Solver ()
captureSignature func = do
ts <- State.gets ssTypeSystem
case TS.lookupType func ts of
Just descr -> case descr of
FuncDescr l _ ret ps -> do
-- Apply bindings to the entire signature at once to ensure consistency
phId <- fromMaybe 0 . Map.lookup func <$> State.gets ssFuncPhases
sig <- applyBindingsDeep (Function (TS.toLocal phId (Just func) ret) (map (TS.toLocal phId (Just func)) ps))
case sig of
Function ret' ps' -> do
dtraceM $ "captureSignature: before norm: ret'=" ++ show ret' ++ " ps'=" ++ show ps'
let (tys', templates) = TS.normalizeDescr (map convertBack (ret':ps'))
dtraceM $ "captureSignature: after norm: tys'=" ++ show tys' ++ " templates=" ++ show templates
let (ret'', ps'') = case tys' of (r:p) -> (r, p); _ -> (ret, ps)
let descr' = FuncDescr l templates ret'' ps''
let sig'' = Function (TS.toLocal 0 Nothing ret'') (map (TS.toLocal 0 Nothing) ps'')
dtraceM $ "Captured Signature for " ++ show func ++ ": " ++ show sig''
State.modify $ \s -> s { ssInferred = Map.insert func sig'' (ssInferred s)
, ssTypeSystem = Map.insert func descr' (ssTypeSystem s)
}
_ -> return ()
_ -> return ()
_ -> return ()
where
convertBack :: TypeInfo 'Local -> TypeInfo 'Global
convertBack = foldFix alg
alg :: TypeInfoF (TemplateId 'Local) (TypeInfo 'Global) -> TypeInfo 'Global
alg f = case f of
TemplateF (FullTemplate t i) ->
case t of
TIdInst _ tid' -> Template tid' i
TIdPoly _ idx h _ -> Template (TIdParam idx h) i
TIdSolver idx h -> Template (TIdParam idx h) i
TIdAnonymous h -> Template (TIdParam 0 h) i
TIdRec idx -> Template (TIdRec idx) i
_ -> Fix (bimap convertId id f)
convertId :: TemplateId 'Local -> TemplateId 'Global
convertId (TIdInst _ tid') = tid'
convertId (TIdPoly _ i h _) = TIdParam i h
convertId (TIdSolver i h) = TIdParam i h
convertId (TIdAnonymous h) = TIdParam 0 h
convertId (TIdRec i) = TIdRec i
solveConstraint :: Constraint 'Local -> Solver ()
solveConstraint c = do
dtraceM $ "solveConstraint: " ++ show c
st <- State.get
let action = case c of
Equality t1 t2 loc ctx reason -> void $ U.unify t1 t2 reason loc ctx
Subtype actual expected loc ctx reason -> void $ U.subtype actual expected reason loc ctx
_ -> return ()
let initialState = U.UnifyState (ssBindings st) [] (ssTypeSystem st) Set.empty (ssNextId st) (ssFinalPass st)
let finalUnifyState = execState action initialState
when (not $ null $ U.usErrors finalUnifyState) $
dtraceM $ "solveConstraint result errors: " ++ show (U.usErrors finalUnifyState)
State.modify $ \s -> s
{ ssBindings = U.usBindings finalUnifyState
, ssErrors = if ssFinalPass st then ssErrors s ++ U.usErrors finalUnifyState else ssErrors s
, ssNextId = U.usNextId finalUnifyState
}
case c of
Callable ft atys rt loc ctx csId shouldRefresh -> do
dtraceM $ "solve Callable: " ++ show ft ++ " args=" ++ show atys
solveCallable ft atys rt GeneralMismatch loc ctx csId shouldRefresh
MemberAccess t field mt loc ctx reason -> solveMemberAccess t field mt reason loc ctx
CoordinatedPair trigger actual expected loc ctx mCsId -> solveCoordinatedPair trigger actual expected loc ctx mCsId
_ -> return ()
-- Solvers delegate to Unification engine
-- Core logic adapted from old Solver.hs, will implement piece by piece for soundness
solveCoordinatedPair :: TypeInfo 'Local -> TypeInfo 'Local -> TypeInfo 'Local -> Maybe (Lexeme Text) -> [Context 'Local] -> Maybe Integer -> Solver ()
solveCoordinatedPair trigger actual expected loc ctx mCsId = do
st <- State.get
let initialState = U.UnifyState (ssBindings st) [] (ssTypeSystem st) Set.empty (ssNextId st) (ssFinalPass st)
let tr = evalState (U.resolveType =<< U.applyBindings trigger) initialState
dtraceM $ "solve CoordinatedPair: trigger=" ++ show tr
let isNull = \case
BuiltinType NullPtrTy -> True
_ -> False
case tr of
_ | isNull tr -> return ()
_ -> do
expected' <- refreshTemplates mCsId expected
dtraceM $ "solve CoordinatedPair unify: actual=" ++ show actual ++ " expected'=" ++ show expected'
let finalUnifyState = execState (void $ U.unify actual expected' GeneralMismatch loc ctx) initialState
State.modify $ \s -> s
{ ssBindings = U.usBindings finalUnifyState
, ssErrors = ssErrors s ++ U.usErrors finalUnifyState
, ssNextId = U.usNextId finalUnifyState
}
bind :: TemplateId 'Local -> Maybe (TypeInfo 'Local) -> TypeInfo 'Local -> MismatchReason -> Maybe (Lexeme Text) -> [Context 'Local] -> Solver ()
bind tid index ty reason ml ctx = do
rep <- applyBindingsDeep (Template tid index)
case rep of
Template tid' index' -> do
bindings <- State.gets ssBindings
let k = FullTemplate tid' index'
case Map.lookup k bindings of
Just (existing, _) -> solveConstraint (Equality existing ty ml ctx reason)
Nothing ->
case ty of
Template tid'' i'' | tid'' == tid' && i'' == index' -> return ()
_ | occurs tid' index' ty -> reportError ml ctx (InfiniteType (T.pack $ show tid') ty)
_ -> do
let prov = FromContext (ErrorInfo ml ctx (TypeMismatch (Template tid' index') ty reason Nothing) [])
dtraceM $ "BIND: " ++ show (Template tid' index') ++ " -> " ++ show ty
State.modify $ \s -> s { ssBindings = Map.insert k (ty, prov) (ssBindings s) }
_ -> solveConstraint (Equality rep ty ml ctx reason)
occurs :: TemplateId p -> Maybe (TypeInfo p) -> TypeInfo p -> Bool
occurs tid index ty = snd $ foldFix alg ty
where
alg f = (Fix (fmap fst f), (Fix (fmap fst f) == Template tid index) || any snd f)
applyBindings :: TypeInfo 'Local -> Solver (TypeInfo 'Local)
applyBindings ty = applyBindingsWith Set.empty ty
applyBindingsWith :: Set (FullTemplate 'Local) -> TypeInfo 'Local -> Solver (TypeInfo 'Local)
applyBindingsWith seen ty = case unFix ty of
TemplateF (FullTemplate tid i) ->
let k = FullTemplate tid i in
if Set.member k seen
then return ty
else do
bindings <- State.gets ssBindings
case Map.lookup k bindings of
Just (target, _) -> applyBindingsWith (Set.insert k seen) target
Nothing -> return ty
_ -> return ty
applyBindingsDeep :: TypeInfo 'Local -> Solver (TypeInfo 'Local)
applyBindingsDeep ty = do
bindings <- State.gets ssBindings
let graph = Map.map (\(ty', _) -> Set.singleton (TG.fromTypeInfo ty')) bindings
initialKeys = TS.collectUniqueTemplateVars [ty]
resolvedMap = GS.solveAll graph initialKeys
return $ foldFix (alg resolvedMap) ty
where
alg m (TemplateF (FullTemplate tid i)) =
maybe (Template tid i) TG.toTypeInfo (Map.lookup (FullTemplate tid i) m)
alg _ f = Fix f
resolveType :: TypeInfo 'Local -> Solver (TypeInfo 'Local)
resolveType ty = do
st <- State.get
let initialState = U.UnifyState (ssBindings st) [] (ssTypeSystem st) Set.empty (ssNextId st) (ssFinalPass st)
return $ evalState (U.resolveType ty) initialState
reportError :: Maybe (Lexeme Text) -> [Context 'Local] -> TypeError 'Local -> Solver ()
reportError ml ctx err = do
isFinal <- State.gets ssFinalPass
when isFinal $ do
bindings <- State.gets ssBindings
let allTypes = case err of
TypeMismatch expected actual _ _ -> expected : actual : concatMap getContextTypes ctx
_ -> concatMap getContextTypes ctx
let expls = concatMap (P.explainType bindings) allTypes
State.modify $ \s -> s { ssErrors = ssErrors s ++ [ErrorInfo ml ctx err (P.dedupDocs expls)] }
where
getContextTypes = \case
InUnification e a _ -> [e, a]
_ -> []
solveCallable :: TypeInfo 'Local -> [TypeInfo 'Local] -> TypeInfo 'Local -> MismatchReason -> Maybe (Lexeme Text) -> [Context 'Local] -> Maybe Integer -> Bool -> Solver ()
solveCallable ft atys rt reason ml ctx mCsId shouldRefresh = do
ft' <- case ft of
TypeRef TS.FuncRef (L _ _ tid) _ -> do
let name = templateIdBaseName tid
inferred <- State.gets ssInferred
case Map.lookup name inferred of
Just sig -> applyBindings sig
Nothing -> resolveType =<< applyBindings ft
_ -> resolveType =<< applyBindings ft
ft'' <- if shouldRefresh
then refreshTemplates mCsId ft'
else return ft'
when shouldRefresh $
case ft of
TypeRef TS.FuncRef (L _ _ tid) args -> do
ts <- State.gets ssTypeSystem
case TS.lookupType (TS.templateIdBaseName tid) ts of
Just descr ->
let tps = TS.getDescrTemplates descr
in when (length tps == length args) $ do
tps' <- mapM (refreshTemplates mCsId . TS.toLocal 0 Nothing . (\t -> Template t Nothing)) tps
zipWithM_ (\a t' -> solveConstraint (Equality a t' ml ctx reason)) args tps'
_ -> return ()
_ -> return ()
-- Also de-voidify the resolved type recursively
rt'' <- deVoidify ft''
dtraceM $ "solve Callable ft'=" ++ show ft' ++ " ft''=" ++ show ft'' ++ " rt''=" ++ show rt''
case stripAllWrappers rt'' of
Function ret params -> do
let isVariadic = any isVarArg params
isSpecial p' = isVarArg p' || TS.isVoid p'
expectedParams = filter (not . isSpecial) params
nExpected = length expectedParams
nActual = length atys
st <- State.get
let initialState = U.UnifyState (ssBindings st) [] (ssTypeSystem st) Set.empty (ssNextId st) (ssFinalPass st)
let action = do
void $ U.unify ret rt reason ml ctx
if isVariadic then
if nActual < nExpected then
U.reportError ml ctx (TooFewArgs nExpected nActual)
else
mapM_ (uncurry (\a p -> void $ U.subtype a p reason ml ctx)) (zip atys expectedParams)
else
if nActual < nExpected then
U.reportError ml ctx (TooFewArgs nExpected nActual)
else if nActual > nExpected then
U.reportError ml ctx (TooManyArgs nExpected nActual)
else
mapM_ (uncurry (\a p -> void $ U.subtype a p reason ml ctx)) (zip atys expectedParams)
let finalUnifyState = execState action initialState
dtraceM $ "solve Callable result errors: " ++ show (U.usErrors finalUnifyState)
State.modify $ \s -> s
{ ssBindings = U.usBindings finalUnifyState
, ssErrors = ssErrors s ++ U.usErrors finalUnifyState
, ssNextId = U.usNextId finalUnifyState
}
Template tid i -> do
-- Proactively bind the template to a function type based on how it's being called.
-- Deterministic template names based on csId ensure monotonicity.
bindings <- State.gets ssBindings
case mCsId of
Just csId -> do
let retTid = TIdInst csId (TIdName "ret")
case Map.lookup (FullTemplate tid i) bindings of
Just (Fix (TS.FunctionF _ _), _) -> return ()
_ -> bind tid i (Function (Template retTid Nothing) atys) reason ml ctx
Nothing -> return () -- Cannot proactively bind without stable ID
_ -> return ()
deVoidify :: TypeInfo 'Local -> Solver (TypeInfo 'Local)
deVoidify = snd . foldFix alg
where
alg :: TypeInfoF (TemplateId 'Local) (TypeInfo 'Local, Solver (TypeInfo 'Local)) -> (TypeInfo 'Local, Solver (TypeInfo 'Local))
alg f = (Fix (fmap fst f), case f of
PointerF (orig, _) | TS.isVoid orig -> do
tp <- nextSolverTemplate Nothing
let applyWrappers (BuiltinType VoidTy) x = x
applyWrappers (Const t') x = Const (applyWrappers t' x)
applyWrappers (Owner t') x = Owner (applyWrappers t' x)
applyWrappers (Nonnull t') x = Nonnull (applyWrappers t' x)
applyWrappers (Nullable t') x = Nullable (applyWrappers t' x)
applyWrappers (Var l t') x = Var l (applyWrappers t' x)
applyWrappers (Sized t' l) x = Sized (applyWrappers t' x) l
applyWrappers _ x = x
return $ Pointer (applyWrappers orig tp)
_ -> Fix <$> traverse snd f)
refreshTemplates :: Maybe Integer -> TypeInfo 'Local -> Solver (TypeInfo 'Local)
refreshTemplates mCsId ty = State.evalStateT (snd (foldFix alg ty)) Map.empty
where
alg :: TypeInfoF (TemplateId 'Local) (TypeInfo 'Local, StateT (Map (FullTemplate 'Local) (TypeInfo 'Local)) Solver (TypeInfo 'Local)) -> (TypeInfo 'Local, StateT (Map (FullTemplate 'Local) (TypeInfo 'Local)) Solver (TypeInfo 'Local))
alg f = (Fix (fmap fst f), do
case f of
TemplateF (FullTemplate tid i) -> do
m <- State.get
let k = FullTemplate tid (fst <$> i)
case Map.lookup k m of
Just t' -> return t'
Nothing -> do
i' <- maybe (return Nothing) (fmap Just . snd) i
case tid of
TIdPoly ph _ _ _ -> do
active <- lift $ State.gets ssActivePhases
if Set.member ph active
then return $ Template tid i'
else do
t' <- lift $ case mCsId of
Just csId -> return $ Template (TIdInst csId (convertId tid)) i'
Nothing -> nextSolverTemplate (Just $ templateIdToText tid)
State.modify $ Map.insert k t'
return t'
TIdSolver _ _ -> return $ Template tid i'
_ -> do
t' <- lift $ case mCsId of
Just csId -> return $ Template (TIdInst csId (convertId tid)) i'
Nothing -> nextSolverTemplate (Just $ templateIdBaseName tid)
State.modify $ Map.insert k t'
return t'
_ -> Fix <$> traverse snd f)
convertId :: TemplateId 'Local -> TemplateId 'Global
convertId (TIdInst _ tid') = tid'
convertId (TIdPoly _ i h _) = TIdParam i h
convertId (TIdSolver _ h) = TIdParam 0 h
convertId (TIdAnonymous h) = TIdParam 0 h
convertId (TIdRec i) = TIdRec i
nextSolverTemplate :: Maybe Text -> Solver (TypeInfo 'Local)
nextSolverTemplate mHint = do
i <- State.gets ssNextId
State.modify $ \s -> s { ssNextId = i + 1 }
return $ Template (TIdSolver i mHint) Nothing
solveMemberAccess :: TypeInfo 'Local -> Text -> TypeInfo 'Local -> MismatchReason -> Maybe (Lexeme Text) -> [Context 'Local] -> Solver ()
solveMemberAccess t field mt reason _ml _ctx = do
rt <- resolveType =<< applyBindings t
ts <- State.gets ssTypeSystem
case stripAllWrappers rt of
TypeRef _ (L _ _ tid) args ->
let name = TS.templateIdBaseName tid in
case TS.lookupType name ts of
Just descr -> do
let descr' = TS.instantiateDescr 0 Nothing (Map.fromList (zip (TS.getDescrTemplates descr) args)) descr
case TS.lookupMemberType field descr' of
Just mty -> do
st <- State.get
let initialState = U.UnifyState (ssBindings st) [] (ssTypeSystem st) Set.empty (ssNextId st) (ssFinalPass st)
let finalUnifyState = execState (U.unify mty mt reason Nothing []) initialState
when (not $ null $ U.usErrors finalUnifyState) $
dtraceM $ "solveMemberAccess result errors: " ++ show (U.usErrors finalUnifyState)
State.modify $ \s -> s
{ ssBindings = U.usBindings finalUnifyState
, ssErrors = ssErrors s ++ U.usErrors finalUnifyState
, ssNextId = U.usNextId finalUnifyState
}
Nothing -> return ()
_ -> return ()
_ -> return ()