{-
Static Analysis using CTL Model Checking
Unfortunately the current implementation of CTL Model Checking doesn't give counter examples
which makes it kind of useless for these purposes. It only gives us a Boolean result. Ie it
tells us IF something is not right but doesn't tell us what it is nor where it is.

Usage: Reads a C source file from the standard input and prints out any warning messages it finds.
-}

module Main where

import AST
import CFG
import Parser
import Text.ParserCombinators.Parsec
import Control.Monad.State

import System.Cmd
import System.Environment
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Data.Graph.Inductive.Graph as Graph
import Data.Graph.Inductive.Tree
import Data.Graph.Inductive.Graphviz
import Data.List(nub)
import Text.Printf

import CTLModelChecker

-- type Succ st = st -> [st]
-- type Interp p st = p -> st -> Bool

nothing = putStr ""

main = do
   args <- getArgs
   s <- getContents
   if (null args) then nothing else if (head args == "-graphviz") then cfgViz$functionToCFG s else nothing
   putStr $ checkFile s

ctlFormulasFor x = [
    allUnless (Not (Atomic (Assigned x))) (Atomic (Decl x))   -- A (! Assigned x) W (Decl x)
   ,allUnless (Not (Atomic (Used x))) (Atomic (Assigned x))   -- A (! Used x) W (Assigned x)
   ,allGlobal (ctlImplies (Atomic (Decl x)) (existsFuture (Atomic (Used x))))    -- AG ((Decl x) => (EF (Used x)))
   ]

formulaErrorMsgs = [
   "\"%s\" is assigned a value before being declared",
   "\"%s\" is used before being initialised",
   "\"%s\" is declared but never used"]

ctlOr x y = Not (And (Not x) (Not y))
ctlImplies x y = ctlOr (Not x) y
existsUnless x y = Not (AllUntil (And x (Not y)) (And (Not x) (Not y)))
allUnless x y = Not (ExUntil (And x (Not y)) (And (Not x) (Not y)))

--checkFile :: String -> [(String, [(String, [Bool])])]
--checkFile :: String -> [(String, [String])]
checkFile str = unlines $ (filter (not.null)) $ concat
   [("In function " ++ fname) : (concat
      [zipWith (\s b -> if b then "" else printf s x) formulaErrorMsgs (map (checkCTL interp succ start) (ctlFormulasFor x)) | x <- ids]) |
         (interp,succ,start,ids,fname) <- map cfgToInterpSucc cfgs]
   where cfgs = [(snd.(flip execState ([1..],emptyCFG 0)).function) f | f <- fileToFunctions str]

cfgToInterpSucc :: CFG -> (Interp Label ID,Succ ID,ID,[String],String)
cfgToInterpSucc (CFG ns as start _) = (interp,succ,start,nub$concatMap nodeIdentifiers (Map.elems ns),funcName (Map.elems ns))
   where interp lab x = nodeHasLabel lab (Map.lookup x ns)
         succ x = map snd $ Set.elems (Set.filter (\(y,_) -> y == x) as)

nodeIdentifiers :: Node -> [String]
nodeIdentifiers (Node ls _) = map labelIdentifier ls
nodeIdentifiers _ = []

labelIdentifier :: Label -> String
labelIdentifier (Decl x) = x
labelIdentifier (Used x) = x
labelIdentifier (Assigned x) = x
labelIdentifier (Defined x) = x

funcName :: [Node] -> String
funcName ns = head [s | (Defined s) <- concat [ls | (Node ls _) <- ns]]

nodeHasLabel :: Label -> Maybe Node -> Bool
nodeHasLabel lab (Just (Node labs _)) = elem lab labs
nodeHasLabel _ _ = False

fileToFunctions :: String -> [Global]
fileToFunctions s = either (\x -> error ("error: " ++ (show x))) (\gs -> [f | f@(FunctionDef _ _ _ _ _) <- gs]) (parse file "" s)

functionToCFG :: String -> CFG
functionToCFG source = either (\x -> error (show x)) (snd.(flip execState ([1..],emptyCFG 0)).function.head) (parse file "" source)

cfgToGraph :: CFG -> Gr String ()
cfgToGraph (CFG ns as _ _) = 
   Graph.insEdges [(x,y,()) | (x,y) <- Set.toList as]
   (Graph.insNodes [(x,showLabels node) | (x,node) <- Map.toList ns] Graph.empty)

cfgViz :: CFG -> IO ()
cfgViz cfg = do
   writeFile "chopsticks.graph" $ graphviz (cfgToGraph cfg) "Chopsticks" (8.5,11) (1,1) Portrait
   system "dot -Tsvg chopsticks.graph -o chopsticks.svg"
   return ()

showLabels (Node [] _) = ""
showLabels (Node ls _) = show ls
showLabels EmptyNode = ""