--
-- Each instruction can be seen as taking parameters (optionally) from the
-- stack and pushing a result on the stack (optionally).
-- Analyzes how the stack looks like prior to an instruction: which entries
-- were defined by which instruction(s).
--
-- For each stack entry, the trick is to keep a set of instruction labels
-- such that for each label there exists a path in the control flow graph
-- where that stack entry was defined the last time.
--

MODULE {ParamAnalysis} {analyzeDefsSwf,analyzeDefsAbc,MethodDefInfo,MethodDefInfos,InstrDefInfo,StackDefInfo,DefInfo} {}

optpragmas
{
{-# LANGUAGE EmptyDataDecls, TypeFamilies #-}
}

INCLUDE "ByteCodeAst.ag"
INCLUDE "ByteCodeBranchInfo.ag"
INCLUDE "DistNameInfo.ag"
INCLUDE "InstructionInfo.ag"
INCLUDE "CommonImports.ag"
INCLUDE "NumberAstNodes.ag"

imports
{
import Fixpoint
}

WRAPPER SwfFile
WRAPPER AbcFile

{
analyzeDefsSwf :: SwfFile -> MethodDefInfos
analyzeDefsSwf m = out where
  inh = Inh_SwfFile {}
  sem = sem_SwfFile m
  syn = wrap_SwfFile sem inh
  out = output_Syn_SwfFile syn

analyzeDefsAbc :: AbcFile -> MethodDefInfo
analyzeDefsAbc m = out where
  inh = Inh_AbcFile {}
  sem = sem_AbcFile m
  syn = wrap_AbcFile sem inh
  out = output_Syn_AbcFile syn

type MethodDefInfos = [MethodDefInfo]
type MethodDefInfo = IntMap InstrDefInfo
type InstrDefInfo = IntMap StackDefInfo
}

ATTR SwfFile Tags Tag            [ | | output USE {++} {[]} : MethodDefInfos ]
ATTR AbcFile BodyInfos BodyInfo  [ | | output USE {`mappend`} {mempty} : MethodDefInfo ]

SEM Tag | Abc   lhs.output = [@file.output]
SEM BodyInfo | Info  lhs.output = IntMap.singleton @lhs.bodyId @loc.stacksRes


-- The stack stores for each entry the latest instructions where this entry is defined.
-- Thus, we take the union on all entries of a node in the CFG, and for each node, find out
-- how the stack is transformed.
{
type StackDefInfo = [DefInfo]
type DefInfo      = IntSet

joinStackDefs :: StackDefInfo -> StackDefInfo -> StackDefInfo
joinStackDefs []     ys     = ys
joinStackDefs xs     []     = xs
joinStackDefs (x:xs) (y:ys) = joinDefs x y : joinStackDefs xs ys

joinDefs :: DefInfo -> DefInfo -> DefInfo
joinDefs = IntSet.union

-- Instantiation of the fixpoint graph.
data TAbstractStack
type StackGraph = FixGraph TAbstractStack
type StackSem   = FixSem TAbstractStack
type instance EdgeVal TAbstractStack = StackDefInfo
type instance NodeVal TAbstractStack = (StackDefInfo, Int)  -- stack and iterations
type instance NodeId  TAbstractStack = Int
}


--
-- Semantics of nodes
--

{
nodeSem :: Word32 -> Int -> (StackDefInfo -> StackDefInfo) -> NodeFunIn TAbstractStack -> NodeFunOut TAbstractStack
nodeSem method label f (NodeFunIn inps mbCurrent mbPrev) = NodeFunOut (Just (outStack, n)) mbOutStack where
  mbOutStack = case mbPrev of                                  -- check if the output changed
    Just prevStack | prevStack == outStack -> Nothing          -- output has not changed
                   | n > iterLimit         -> Nothing          -- iteration limit reached
    _                                      -> Just outStack    -- output changed (into outStack)

  outStack = f inpStack       -- apply the stack transformation
  
  inpStack = case inps of
    []    -> []
    [inp] -> inp
    _     -> foldl1 joinStackDefs inps

  n = case mbCurrent of
        Just (_, m) -> ( if m == iterWarning
                         then trace ("param analysis " ++ show method ++ "," ++ show label ++ ": warning: more than " ++ show iterWarning ++ " iterations.") id
                         else id
                       ) (m+1)
        Nothing     -> 1

iterWarning :: Int
iterWarning = 80

iterLimit   :: Int
iterLimit   = 100

checkSem :: Word32 -> Int -> NodeFunIn TAbstractStack -> NodeFunOut TAbstractStack
checkSem method label (NodeFunIn inps _ _) = seq check NodeFunOut Nothing Nothing where
  check | all (\x -> length x == l) inps = ()
        | otherwise                      = trace ("param analysis " ++ show method ++ "," ++ show label ++ ": warning: unbalanced inputs: " ++ show inps) ()
        where l | null inps = 0
                | otherwise = length (head inps)
}

ATTR InstructionsLike LabInstruction [ methodId : Word32 | | ]
SEM BodyInfo | Info  instructions.methodId = @method

SEM LabInstruction | Instr
  lhs.gathNodes = node @label $ nodeSem @lhs.methodId @label @instruction.afterEffect
  lhs.gathCheck = node @label $ checkSem @lhs.methodId @label


--
-- Connecting it together
--

-- Collect edges
ATTR InstructionsLike LabInstruction
  [ | | gathEdges USE {`mappend`} {mempty} : StackGraph ]

SEM LabInstruction | Instr
  lhs.gathEdges = mconcat [ edge @label t | t <- @loc.targets ]

-- Collect semantics for nodes
ATTR InstructionsLike LabInstruction
  [ | | gathNodes, gathCheck USE {`mappend`} {mempty} : StackSem ]

SEM BodyInfo | Info
  loc.rootEdges   = mconcat (edge methodStart @loc.methodRoot : [ edge excptStart r | r <- @exceptions.roots ])
  loc.allEdges    = @loc.rootEdges `mappend` @instructions.gathEdges
  loc.methodRoot  = maybe 0 id @instructions.followup
  loc.stacksInit  = Map.fromList [(methodStart, []),(excptStart, [IntSet.empty])]
  loc.stacks1     = Map.map fst $ solve @loc.allEdges @instructions.gathNodes @loc.stacksInit
  loc.stacks2     = Map.map fst $ solve @loc.allEdges @instructions.gathCheck @loc.stacks1
  loc.stacksRes   = IntMap.fromAscList $ Map.assocs @loc.stacks2

ATTR Exceptions Exception [ | | roots USE {++} {[]} : {[Int]} ]
SEM Exception | Info  lhs.roots = [fromIntegral @target]

{
methodStart :: Int
methodStart = -1

excptStart :: Int
excptStart  = -2
}


--
-- Abstract interpretation of each instruction
--

ATTR Instruction [ label : Int | | afterEffect : {StackDefInfo -> StackDefInfo} ]
SEM LabInstruction | Instr
  instruction.label = @label

SEM Instruction | *
  lhs.afterEffect = mut @lhs.label @loc.inputs @loc.outputs

{
mut :: (Integral a, Integral b) => Int -> a -> b -> StackDefInfo -> StackDefInfo
mut label inputs outputs
  = (replicate (fromIntegral outputs) (IntSet.singleton label) ++)
  . drop (fromIntegral inputs)
}