diff --git a/GenCIL.hs b/GenCIL.hs new file mode 100644 --- /dev/null +++ b/GenCIL.hs @@ -0,0 +1,400 @@ +-- | Parses OCaml cil_types.mli file and generates an equivalent CIL.hs file and a supporting Frama-C plugin (-dumpcil). +module Main (main) where + +import Data.Char +import Data.List hiding (group) +import System.Process +import Text.ParserCombinators.Poly.Plain +import Text.Printf + +main :: IO () +main = do + f <- readFile "cil_types.mli" + writeFile "cil_types_nocomments.mli" $ decomment f + let types = parseOCaml f + system "mkdir -p install-dumpcil-plugin" + writeFile "install-dumpcil-plugin/Makefile" $ dumpcilMakefile + writeFile "install-dumpcil-plugin/dump_cil.ml" $ dumpcilPlugin types + writeFile "CIL.hs" $ haskellCIL types + + +-- OCaml type types. + +-- Type definitions. +data TypeDef + = Sum [(String, [TypeApply])] + | Record [(String, TypeApply)] + | Alias TypeApply + deriving (Show, Eq) + +--- Type definition name with parameters. +data TypeName = TypeName String [String] deriving (Show, Eq) + +-- Type references. Either type applications or tuples. +data TypeApply + = TypeApply VarPar [TypeApply] + | TypeApplyGroup TypeApply + deriving (Show, Eq) + +-- Type variables or parameters. +data VarPar = Var String | Par String deriving (Show, Eq) + + + +cap :: String -> String +cap [] = [] +cap (a:b) = toUpper a : b + +isAlias :: TypeDef -> Bool +isAlias (Alias _) = True +isAlias _ = False + +-- Haskell CIL module generation. +haskellCIL :: [(TypeName, TypeDef)] -> String +haskellCIL types = unlines + [ "-- | A Haskell interface to OCaml's CIL library, via Frama-C, providing both a simplied C AST and the ACSL specification language." + , "module Language.CIL" + , " ( parseC" + , " , debugParseC" + , " , installPlugin" + , " , Exn (..)" + , " , Position (..)" + , " , Int64 (..)" + , unlines [ printf " , %-26s %s" (cap name) (if isAlias t then "" else "(..)") | (TypeName name _, t) <- types ] + , " )" + , " where" + , "" + , "import System.Exit" + , "import System.Process" + -- , "import Text.Parse" + , "" + , "-- | Parse a C compilation unit (file)." + , "parseC :: FilePath -> IO File" + , "parseC file = do" + , " (exitCode, out, err) <- readProcessWithExitCode \"frama-c\" [\"-dumpcil\", file] \"\"" + , " let code = unlines $ tail $ lines out" + , " case exitCode of" + , " ExitSuccess -> return $ read code" + , " ExitFailure _ -> putStrLn err >> exitWith exitCode" + , "" + , "-- | Prints output from frama-c -dumpcil." + , "debugParseC :: FilePath -> IO ()" + , "debugParseC file = do" + , " (exitCode, out, err) <- readProcessWithExitCode \"frama-c\" [\"-dumpcil\", file] \"\"" + , " putStrLn out" + , "" + -- {- + -- case exitCode of + -- ExitSuccess -> case runParser parse code of + -- (Left s, a) -> putStrLn ("parse error: " ++ s ++ "\n" ++ code ++ "\n" ++ a) >> exitFailure + -- (Right f, _) -> return f + -- ExitFailure _ -> putStrLn err >> exitWith exitCode + -- -} + , " -- | Installs Frama-C '-dumpcil' plugin. Creates 'install-dumpcil-pluging' directory, deposits a Makefile and dump_cil.ml, then runs 'make' and 'make install'." + , "installPlugin :: IO ()" + , "installPlugin = do" + , " putStrLn \"creating install-dumpcil-plugin directory for plugin compiling and installation ...\"" + , " system \"mkdir -p install-dumpcil-plugin\"" + , " writeFile \"install-dumpcil-plugin/Makefile\" " ++ show dumpcilMakefile + , " writeFile \"install-dumpcil-plugin/dump_cil.ml\" " ++ show (dumpcilPlugin types) + , " putStrLn \"running 'make' to compile dumpcil plugin ...\"" + , " system \"cd install-dumpcil-plugin && make\"" + , " putStrLn \"running 'make install' to install dumpcil plugin ...\"" + , " system \"cd install-dumpcil-plugin && make install\"" + , " return ()" + , "" + , "data Exn = Exn " ++ derives + , "data Position = Position FilePath Int Int " ++ derives + , "data Int64 = Int64 " ++ derives + , "" + , unlines [ printf "%s %s %s = %s %s" (if isAlias t then "type" else "data") (cap name) (intercalate " " params) (fType name t) (if isAlias t then "" else derives) | (TypeName name params, t) <- types ] + ] + where + derives = "deriving (Show, Read, Eq) {-! derive : Parse !-}" + fType :: String -> TypeDef -> String + fType name t = case t of + Sum constructors -> intercalate " | " [ constructorName name ++ concat [ " " ++ group (fTypeApply t) | t <- args ] | (name, args) <- constructors ] + Record fields -> printf "%s { %s }" (cap name) $ intercalate ", " [ printf "%s :: %s" field (fTypeApply tr) | (field, tr) <- fields ] + Alias tr -> fTypeApply tr + + fTypeApply :: TypeApply -> String + fTypeApply a = case a of + TypeApply a [] -> name a + TypeApply (Var "list") [a] -> "[" ++ fTypeApply a ++ "]" + TypeApply (Var "option") [a] -> "Maybe " ++ group (fTypeApply a) + TypeApply (Var "ref") [a] -> fTypeApply a + TypeApply (Var "tuple") args -> group $ intercalate ", " (map fTypeApply args) + TypeApply a args -> name a ++ concat [ " (" ++ fTypeApply t ++ ")" | t <- args ] + TypeApplyGroup a -> fTypeApply a + where + name (Var n) = cap n + name (Par n) = n + +constructorName :: String -> String +constructorName a = case a of + "Block" -> "Block'" + "True" -> "True'" + "False" -> "False'" + "Nothing" -> "Nothing'" + a -> cap a + + +-- Frama-C 'dumpcil' plugin generation. +dumpcilPlugin :: [(TypeName, TypeDef)] -> String +dumpcilPlugin types = unlines + [ "open Ast" + , "open Cil_types" + , "open File" + , "open Lexing" + , "open List" + , "open String" + , "open Int64" + , "open Char" + , "" + , "let string a = \"\\\"\" ^ a ^ \"\\\"\" (* XXX Doesn't handle '\\' or '\"' chars in string. *)" + , "let position t = \"Position \\\"\" ^ t.pos_fname ^ \"\\\" \" ^ string_of_int t.pos_lnum ^ \" \" ^ string_of_int (t.pos_cnum - t.pos_bol + 1)" + , "let bool a = if a then \"True\" else \"False\"" + , "let char = Char.escaped" + , "let int = string_of_int" + , "let int64 = Int64.to_string" + , "let float = string_of_float" + , "" + , "let rec " ++ intercalate "\nand " (map fType types) + , "" + , "let run () =" + , " File.init_from_cmdline ();" + , " print_endline (file (Ast.get ()))" + , "" + , "module Self =" + , " Plugin.Register" + , " (struct" + , " let name = \"dumpcil\"" + , " let shortname = \"dumpcil\"" + , " let descr = \"Dumps CIL and ACSL to stdout to be read by Haskell CIL.\"" + , " end);;" + , "" + , "module Enabled =" + , " Self.False" + , " (struct" + , " let option_name = \"-dumpcil\"" + , " let descr = \"Dumps CIL and ACSL to stdout to be read by Haskell CIL.\"" + , " end);;" + , "" + , "let () = Db.Main.extend (fun () -> if Enabled.get () then run ())" + ] + where + fType :: (TypeName, TypeDef) -> String + fType (TypeName name args, m) = name ++ concatMap (" " ++) args ++ " m = " ++ case m of -- Parametric types are passed formating functions for each of the parameters. + Sum constructors -> function (map constructor constructors) ++ " m" + Record fields -> "\"" ++ cap name ++ " { " ++ intercalate ", " (map field fields) ++ " }\"" + Alias m -> fTypeApply m ++ " m" + + constructor :: (String, [TypeApply]) -> (String, String) + constructor (name, []) = (name, show $ cap name) + constructor (name, [m]) = (name ++ " m1", show (constructorName name) ++ " ^ \" \" ^ " ++ fTypeApply m ++ " m1") + constructor (name, args) = (name ++ " " ++ group (intercalate ", " [ "m" ++ show i | i <- [1 .. length args] ]), show (constructorName name) ++ concat [ " ^ \" \" ^ " ++ metaGroup (fTypeApply m ++ " m" ++ show i) | (m, i) <- zip args [1..] ]) + + field :: (String, TypeApply) -> String + field (name, t) = name ++ " = " ++ "\" ^ " ++ fTypeApply t ++ " m." ++ name ++ " ^ \"" + + -- Returns an OCaml function :: Data -> String + fTypeApply :: TypeApply -> String + fTypeApply m = case m of + TypeApply (Var "exn") [] -> "(fun _ -> \"Exn\")" + TypeApply m [] -> name m -- Vars are top level functions, Params should be functions passed in and thus in scope. + TypeApply (Var "list") [m] -> function [("m", "\"[ \" ^ concat \", \" (map " ++ group (fTypeApply m) ++ " m) ^ \" ]\"")] + TypeApply (Var "option") [m] -> function [("None", show "Nothing"), ("Some m", show "Just " ++ " ^ " ++ metaGroup (fTypeApply m ++ " m"))] + TypeApply (Var "ref") [m] -> function [("m", metaGroup (fTypeApply m ++ " (!m)"))] + TypeApply (Var "tuple") args -> function [(group $ intercalate ", " [ "m" ++ show i | i <- [1 .. length args] ], metaGroup $ intercalate " ^ \", \" ^ " [ metaGroup (fTypeApply m ++ " m" ++ show i) | (m, i) <- zip args [1..] ])] + TypeApply m args -> function [("m", metaGroup (name m ++ concat [ " " ++ function [("m", metaGroup (fTypeApply arg ++ " m"))] | arg <- args ] ++ " m"))] + TypeApplyGroup a -> fTypeApply a + where + name (Var n) = n + name (Par n) = n + + function :: [(String, String)] -> String + function matches = group $ "function " ++ intercalate " | " [ a ++ " -> " ++ b | (a, b) <- matches ] + +group :: String -> String +group a = "(" ++ a ++ ")" + +metaGroup :: String -> String +metaGroup a = group $ "\"(\" ^ " ++ a ++ " ^ \")\"" + + +-- | Makefile used to install the dumpcil plugin. +dumpcilMakefile :: String +dumpcilMakefile = unlines + [ "FRAMAC_SHARE :=$(shell frama-c.byte -print-path)" + , "FRAMAC_LIBDIR :=$(shell frama-c.byte -print-libpath)" + , "PLUGIN_NAME = Dumpcil" + , "PLUGIN_CMO = dump_cil" + , "include $(FRAMAC_SHARE)/Makefile.dynamic" + ] + + + +-- Lexing. + +data Token + = Type + | Of + | Eq + | Pipe + | Colon + | SemiColon + | Star + | Comma + | ParenLeft + | ParenRight + | BraceLeft + | BraceRight + | Constructor String + | Variable String + | Parameter String + deriving (Show, Eq) + +lexer :: String -> [Token] +lexer = map t . filter (/= "mutable") . filter (not . null) . concatMap split . words . decomment + where + split :: String -> [String] + split a = case break isSym a of + (word, []) -> [word] + (word, (a:b)) -> [word, [a]] ++ split b + isSym = flip elem "=|;:*,(){}" + t :: String -> Token + t a = case a of + "type" -> Type + "and" -> Type + "of" -> Of + "=" -> Eq + "|" -> Pipe + ":" -> Colon + ";" -> SemiColon + "*" -> Star + "," -> Comma + "(" -> ParenLeft + ")" -> ParenRight + "{" -> BraceLeft + "}" -> BraceRight + '\'':a -> Parameter a + a | elem '.' a -> t $ tail $ dropWhile (/= '.') a + a:b | isUpper a -> Constructor (a : b) + | otherwise -> Variable (a : b) + a -> error $ "unexpected string: " ++ a + +decomment :: String -> String +decomment = decomment' 0 + where + decomment' :: Int -> String -> String + decomment' n "" | n == 0 = "" + | otherwise = error "reached end of file without closing comment" + decomment' n ('(':'*':a) = " " ++ decomment' (n + 1) a + decomment' n ('*':')':a) | n > 0 = " " ++ decomment' (n - 1) a + | otherwise = error "unexpected closing comment" + decomment' n (a:b) = (if n > 0 && a /= '\n' then ' ' else a) : decomment' n b + + + + + + + +-- Parsing. + +type OCaml a = Parser Token a + +parseOCaml :: String -> [(TypeName, TypeDef)] +parseOCaml a = case runParser (many typeDef `discard` eof) $ lexer a of + (Left msg, remaining) -> error $ msg ++ "\nremaining tokens: " ++ show (take 30 $ remaining) ++ " ..." + (Right a, []) -> a + (Right _, remaining) -> error $ "parsed, but with remaining tokens: " ++ show remaining + +tok :: Token -> OCaml () +tok a = satisfy (== a) >> return () + +parameter :: OCaml String +parameter = do + a <- satisfy (\ a -> case a of { Parameter _ -> True; _ -> False }) + case a of + Parameter s -> return s + _ -> undefined + +constructor :: OCaml String +constructor = do + a <- satisfy (\ a -> case a of { Constructor _ -> True; _ -> False }) + case a of + Constructor s -> return s + _ -> undefined + +variable :: OCaml String +variable = do + a <- satisfy (\ a -> case a of { Variable _ -> True; _ -> False }) + case a of + Variable s -> return s + _ -> undefined + +typeDef :: OCaml (TypeName, TypeDef) +typeDef = do { tok Type; n <- typeName; tok Eq; e <- typeExpr; return (n, e) } + +typeName :: OCaml TypeName +typeName = oneOf + [ do { tok ParenLeft; a <- parameter; b <- many1 (tok Comma >> parameter); tok ParenRight; n <- variable; return $ TypeName n $ a : b } + , do { p <- parameter; n <- variable; return $ TypeName n [p] } + , do { n <- variable; return $ TypeName n [] } + ] + +varPars :: OCaml [VarPar] +varPars = do { a <- varPar; b <- many varPar; return $ a : b } + where + varPar :: OCaml VarPar + varPar = oneOf [variable >>= return . Var, parameter >>= return . Par] + +typeApply :: OCaml TypeApply +typeApply = oneOf + [ do { tok ParenLeft; a <- varPars; b <- many1 (tok Comma >> varPars); tok ParenRight; c <- varPars; return $ TypeApplyGroup $ apply (map (apply []) (a : b)) c } + , do { tok ParenLeft; a <- typeApply; tok ParenRight; b <- varPars; return $ TypeApplyGroup $ apply [a] b } + , do { tok ParenLeft; a <- typeApply; tok ParenRight; return $ TypeApplyGroup a } + -- XXX Need to prevent nested tuples. + , do { a <- varPars; b <- many1 (tok Star >> typeApply); return $ TypeApply (Var "tuple") $ flattenTuples $ apply [] a : b } + , do { a <- varPars; return $ apply [] a } + ] + where + apply :: [TypeApply] -> [VarPar] -> TypeApply + apply _ [] = error "typeApply: no type to apply to" + apply args [a] = TypeApply a args + apply args (a:b) = apply [(apply args [a])] b + + flattenTuples :: [TypeApply] -> [TypeApply] + flattenTuples = concatMap flattenTuple + + flattenTuple :: TypeApply -> [TypeApply] + flattenTuple (TypeApply (Var "tuple") args) = args + flattenTuple a = [a] + +typeExpr :: OCaml TypeDef +typeExpr = oneOf + [ recordType >>= return . Record + , sumType >>= return . Sum + , typeApply >>= return . Alias + ] + +recordType :: OCaml [(String, TypeApply)] +recordType = do { tok BraceLeft; f <- recordField; fs <- many (tok SemiColon >> recordField); optional $ tok SemiColon; tok BraceRight; return $ f : fs } + +recordField :: OCaml (String, TypeApply) +recordField = do { n <- variable; tok Colon; t <- typeApply; return (n, t) } + +sumType :: OCaml [(String, [TypeApply])] +sumType = do { optional (tok Pipe); a <- sumConstructor; b <- many (tok Pipe >> sumConstructor); return $ a : b } + +sumConstructor :: OCaml (String, [TypeApply]) +sumConstructor = oneOf + [ do { n <- constructor; tok Of; a <- typeApply; return (n, detuple a) } + , do { n <- constructor; return (n, []) } + ] + where + detuple :: TypeApply -> [TypeApply] + detuple (TypeApply (Var "tuple") args) = args + detuple a = [a] + diff --git a/Language/CIL.hs b/Language/CIL.hs --- a/Language/CIL.hs +++ b/Language/CIL.hs @@ -1,20 +1,202 @@ -{- Generated by DrIFT (Automatic class derivations for Haskell) -} -{-# LINE 1 "Language/CIL.DrIFT.hs" #-} +-- | A Haskell interface to OCaml's CIL library, via Frama-C, providing both a simplied C AST and the ACSL specification language. module Language.CIL - ( File (..) + ( parseC + , debugParseC + , installPlugin + , Exn (..) + , Position (..) + , Int64 (..) + , BitsSizeofTyp (..) + , BitsSizeofTypCache (..) + , Termination_kind (..) + , File (..) + , Global (..) + , Typ (..) + , Ikind (..) + , Fkind (..) + , Attribute (..) + , Attributes + , Attrparam (..) + , Compinfo (..) + , Fieldinfo (..) + , Enuminfo (..) + , Enumitem (..) + , Typeinfo (..) + , Varinfo (..) + , Storage (..) + , Exp (..) + , Exp_node (..) + , Exp_info (..) + , Constant (..) + , Unop (..) + , Binop (..) + , Lval + , Lhost (..) + , Offset (..) + , Init (..) + , Initinfo (..) + , Fundec (..) + , Block (..) + , Stmt (..) + , Label (..) + , Stmtkind (..) + , Instr (..) + , Location + , Typsig (..) + , Logic_type (..) + , Identified_term (..) + , Logic_label (..) + , Term (..) + , Term_node (..) + , Term_lval + , Term_lhost (..) + , Term_offset (..) + , Logic_info (..) + , Builtin_logic_info (..) + , Logic_body (..) + , Logic_type_info (..) + , Logic_type_def (..) + , Logic_var (..) + , Logic_ctor_info (..) + , Quantifiers + , Relation (..) + , Predicate (..) + , Identified_predicate (..) + , Variant + , Zone (..) + , Assigns + , Named (..) + , Spec (..) + , Behavior (..) + , Loop_pragma (..) + , Slice_pragma (..) + , Impact_pragma (..) + , Pragma (..) + , Validity (..) + , Annot_checked_status (..) + , Annotation_status (..) + , Annot_status (..) + , Code_annot (..) + , Funspec + , Code_annotation (..) + , Funbehavior + , Global_annotation (..) + , Kinstr (..) + , Mach (..) + ) where -import Text.Parse +import System.Exit +import System.Process -data File = File String - deriving Show {-!derive : Parse !-} +-- | Parse a C compilation unit (file). +parseC :: FilePath -> IO File +parseC file = do + (exitCode, out, err) <- readProcessWithExitCode "frama-c" ["-dumpcil", file] "" + let code = unlines $ tail $ lines out + case exitCode of + ExitSuccess -> return $ read code + ExitFailure _ -> putStrLn err >> exitWith exitCode +-- | Prints output from frama-c -dumpcil. +debugParseC :: FilePath -> IO () +debugParseC file = do + (exitCode, out, err) <- readProcessWithExitCode "frama-c" ["-dumpcil", file] "" + putStrLn out -{-* Generated by DrIFT : Look, but Don't Touch. *-} -instance Parse File where - parse = constructors - [ ( "File" , fmap File parse ) - ] + -- | Installs Frama-C '-dumpcil' plugin. Creates 'install-dumpcil-pluging' directory, deposits a Makefile and dump_cil.ml, then runs 'make' and 'make install'. +installPlugin :: IO () +installPlugin = do + putStrLn "creating install-dumpcil-plugin directory for plugin compiling and installation ..." + system "mkdir -p install-dumpcil-plugin" + writeFile "install-dumpcil-plugin/Makefile" "FRAMAC_SHARE :=$(shell frama-c.byte -print-path)\nFRAMAC_LIBDIR :=$(shell frama-c.byte -print-libpath)\nPLUGIN_NAME = Dumpcil\nPLUGIN_CMO = dump_cil\ninclude $(FRAMAC_SHARE)/Makefile.dynamic\n" + writeFile "install-dumpcil-plugin/dump_cil.ml" "open Ast\nopen Cil_types\nopen File\nopen Lexing\nopen List\nopen String\nopen Int64\nopen Char\n\nlet string a = \"\\\"\" ^ a ^ \"\\\"\" (* XXX Doesn't handle '\\' or '\"' chars in string. *)\nlet position t = \"Position \\\"\" ^ t.pos_fname ^ \"\\\" \" ^ string_of_int t.pos_lnum ^ \" \" ^ string_of_int (t.pos_cnum - t.pos_bol + 1)\nlet bool a = if a then \"True\" else \"False\"\nlet char = Char.escaped\nlet int = string_of_int\nlet int64 = Int64.to_string\nlet float = string_of_float\n\nlet rec bitsSizeofTyp m = (function Not_Computed -> \"Not_Computed\" | Not_Computable m1 -> \"Not_Computable\" ^ \" \" ^ (fun _ -> \"Exn\") m1 | Computed m1 -> \"Computed\" ^ \" \" ^ int m1) m\nand bitsSizeofTypCache m = \"BitsSizeofTypCache { scache = \" ^ bitsSizeofTyp m.scache ^ \" }\"\nand termination_kind m = (function Normal -> \"Normal\" | Exits -> \"Exits\" | Breaks -> \"Breaks\" | Continues -> \"Continues\" | Returns -> \"Returns\") m\nand file m = \"File { fileName = \" ^ string m.fileName ^ \", globals = \" ^ (function m -> \"[ \" ^ concat \", \" (map (global) m) ^ \" ]\") m.globals ^ \", globinit = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ fundec m ^ \")\")) m.globinit ^ \", globinitcalled = \" ^ bool m.globinitcalled ^ \" }\"\nand global m = (function GType (m1, m2) -> \"GType\" ^ \" \" ^ (\"(\" ^ typeinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GCompTag (m1, m2) -> \"GCompTag\" ^ \" \" ^ (\"(\" ^ compinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GCompTagDecl (m1, m2) -> \"GCompTagDecl\" ^ \" \" ^ (\"(\" ^ compinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GEnumTag (m1, m2) -> \"GEnumTag\" ^ \" \" ^ (\"(\" ^ enuminfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GEnumTagDecl (m1, m2) -> \"GEnumTagDecl\" ^ \" \" ^ (\"(\" ^ enuminfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GVarDecl (m1, m2, m3) -> \"GVarDecl\" ^ \" \" ^ (\"(\" ^ funspec m1 ^ \")\") ^ \" \" ^ (\"(\" ^ varinfo m2 ^ \")\") ^ \" \" ^ (\"(\" ^ location m3 ^ \")\") | GVar (m1, m2, m3) -> \"GVar\" ^ \" \" ^ (\"(\" ^ varinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ initinfo m2 ^ \")\") ^ \" \" ^ (\"(\" ^ location m3 ^ \")\") | GFun (m1, m2) -> \"GFun\" ^ \" \" ^ (\"(\" ^ fundec m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GAsm (m1, m2) -> \"GAsm\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GPragma (m1, m2) -> \"GPragma\" ^ \" \" ^ (\"(\" ^ attribute m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | GText m1 -> \"GText\" ^ \" \" ^ string m1 | GAnnot (m1, m2) -> \"GAnnot\" ^ \" \" ^ (\"(\" ^ global_annotation m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\")) m\nand typ m = (function TVoid m1 -> \"TVoid\" ^ \" \" ^ attributes m1 | TInt (m1, m2) -> \"TInt\" ^ \" \" ^ (\"(\" ^ ikind m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m2 ^ \")\") | TFloat (m1, m2) -> \"TFloat\" ^ \" \" ^ (\"(\" ^ fkind m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m2 ^ \")\") | TPtr (m1, m2) -> \"TPtr\" ^ \" \" ^ (\"(\" ^ typ m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m2 ^ \")\") | TArray (m1, m2, m3, m4) -> \"TArray\" ^ \" \" ^ (\"(\" ^ typ m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ exp m ^ \")\")) m2 ^ \")\") ^ \" \" ^ (\"(\" ^ bitsSizeofTypCache m3 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m4 ^ \")\") | TFun (m1, m2, m3, m4) -> \"TFun\" ^ \" \" ^ (\"(\" ^ typ m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2, m3) -> (\"(\" ^ (\"(\" ^ string m1 ^ \")\") ^ \", \" ^ (\"(\" ^ typ m2 ^ \")\") ^ \", \" ^ (\"(\" ^ attributes m3 ^ \")\") ^ \")\"))) m) ^ \" ]\") m ^ \")\")) m2 ^ \")\") ^ \" \" ^ (\"(\" ^ bool m3 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m4 ^ \")\") | TNamed (m1, m2) -> \"TNamed\" ^ \" \" ^ (\"(\" ^ typeinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m2 ^ \")\") | TComp (m1, m2, m3) -> \"TComp\" ^ \" \" ^ (\"(\" ^ compinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ bitsSizeofTypCache m2 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m3 ^ \")\") | TEnum (m1, m2) -> \"TEnum\" ^ \" \" ^ (\"(\" ^ enuminfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attributes m2 ^ \")\") | TBuiltin_va_list m1 -> \"TBuiltin_va_list\" ^ \" \" ^ attributes m1) m\nand ikind m = (function IBool -> \"IBool\" | IChar -> \"IChar\" | ISChar -> \"ISChar\" | IUChar -> \"IUChar\" | IInt -> \"IInt\" | IUInt -> \"IUInt\" | IShort -> \"IShort\" | IUShort -> \"IUShort\" | ILong -> \"ILong\" | IULong -> \"IULong\" | ILongLong -> \"ILongLong\" | IULongLong -> \"IULongLong\") m\nand fkind m = (function FFloat -> \"FFloat\" | FDouble -> \"FDouble\" | FLongDouble -> \"FLongDouble\") m\nand attribute m = (function Attr (m1, m2) -> \"Attr\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attrparam) m) ^ \" ]\") m2 ^ \")\") | AttrAnnot m1 -> \"AttrAnnot\" ^ \" \" ^ string m1) m\nand attributes m = (function m -> \"[ \" ^ concat \", \" (map (attribute) m) ^ \" ]\") m\nand attrparam m = (function AInt m1 -> \"AInt\" ^ \" \" ^ int m1 | AStr m1 -> \"AStr\" ^ \" \" ^ string m1 | ACons (m1, m2) -> \"ACons\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attrparam) m) ^ \" ]\") m2 ^ \")\") | ASizeOf m1 -> \"ASizeOf\" ^ \" \" ^ typ m1 | ASizeOfE m1 -> \"ASizeOfE\" ^ \" \" ^ attrparam m1 | ASizeOfS m1 -> \"ASizeOfS\" ^ \" \" ^ typsig m1 | AAlignOf m1 -> \"AAlignOf\" ^ \" \" ^ typ m1 | AAlignOfE m1 -> \"AAlignOfE\" ^ \" \" ^ attrparam m1 | AAlignOfS m1 -> \"AAlignOfS\" ^ \" \" ^ typsig m1 | AUnOp (m1, m2) -> \"AUnOp\" ^ \" \" ^ (\"(\" ^ unop m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attrparam m2 ^ \")\") | ABinOp (m1, m2, m3) -> \"ABinOp\" ^ \" \" ^ (\"(\" ^ binop m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attrparam m2 ^ \")\") ^ \" \" ^ (\"(\" ^ attrparam m3 ^ \")\") | ADot (m1, m2) -> \"ADot\" ^ \" \" ^ (\"(\" ^ attrparam m1 ^ \")\") ^ \" \" ^ (\"(\" ^ string m2 ^ \")\") | AStar m1 -> \"AStar\" ^ \" \" ^ attrparam m1 | AAddrOf m1 -> \"AAddrOf\" ^ \" \" ^ attrparam m1 | AIndex (m1, m2) -> \"AIndex\" ^ \" \" ^ (\"(\" ^ attrparam m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attrparam m2 ^ \")\") | AQuestion (m1, m2, m3) -> \"AQuestion\" ^ \" \" ^ (\"(\" ^ attrparam m1 ^ \")\") ^ \" \" ^ (\"(\" ^ attrparam m2 ^ \")\") ^ \" \" ^ (\"(\" ^ attrparam m3 ^ \")\")) m\nand compinfo m = \"Compinfo { cstruct = \" ^ bool m.cstruct ^ \", cname = \" ^ string m.cname ^ \", ckey = \" ^ int m.ckey ^ \", cfields = \" ^ (function m -> \"[ \" ^ concat \", \" (map (fieldinfo) m) ^ \" ]\") m.cfields ^ \", cattr = \" ^ attributes m.cattr ^ \", cdefined = \" ^ bool m.cdefined ^ \", creferenced = \" ^ bool m.creferenced ^ \" }\"\nand fieldinfo m = \"Fieldinfo { fcomp = \" ^ compinfo m.fcomp ^ \", fname = \" ^ string m.fname ^ \", ftype = \" ^ typ m.ftype ^ \", fbitfield = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ int m ^ \")\")) m.fbitfield ^ \", fattr = \" ^ attributes m.fattr ^ \", floc = \" ^ location m.floc ^ \", faddrof = \" ^ bool m.faddrof ^ \", fsize_in_bits = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ int m ^ \")\")) m.fsize_in_bits ^ \", foffset_in_bits = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ int m ^ \")\")) m.foffset_in_bits ^ \", fpadding_in_bits = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ int m ^ \")\")) m.fpadding_in_bits ^ \" }\"\nand enuminfo m = \"Enuminfo { ename = \" ^ string m.ename ^ \", eitems = \" ^ (function m -> \"[ \" ^ concat \", \" (map (enumitem) m) ^ \" ]\") m.eitems ^ \", eattr = \" ^ attributes m.eattr ^ \", ereferenced = \" ^ bool m.ereferenced ^ \" }\"\nand enumitem m = \"Enumitem { einame = \" ^ string m.einame ^ \", eival = \" ^ exp m.eival ^ \", eihost = \" ^ enuminfo m.eihost ^ \", eiloc = \" ^ location m.eiloc ^ \" }\"\nand typeinfo m = \"Typeinfo { tname = \" ^ string m.tname ^ \", ttype = \" ^ typ m.ttype ^ \", treferenced = \" ^ bool m.treferenced ^ \" }\"\nand varinfo m = \"Varinfo { vname = \" ^ string m.vname ^ \", vorig_name = \" ^ string m.vorig_name ^ \", vtype = \" ^ typ m.vtype ^ \", vattr = \" ^ attributes m.vattr ^ \", vstorage = \" ^ storage m.vstorage ^ \", vglob = \" ^ bool m.vglob ^ \", vdefined = \" ^ bool m.vdefined ^ \", vformal = \" ^ bool m.vformal ^ \", vinline = \" ^ bool m.vinline ^ \", vdecl = \" ^ location m.vdecl ^ \", vid = \" ^ int m.vid ^ \", vaddrof = \" ^ bool m.vaddrof ^ \", vreferenced = \" ^ bool m.vreferenced ^ \", vgenerated = \" ^ bool m.vgenerated ^ \", vdescr = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ string m ^ \")\")) m.vdescr ^ \", vdescrpure = \" ^ bool m.vdescrpure ^ \", vghost = \" ^ bool m.vghost ^ \", vlogic = \" ^ bool m.vlogic ^ \", vlogic_var_assoc = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ logic_var m ^ \")\")) m.vlogic_var_assoc ^ \" }\"\nand storage m = (function NoStorage -> \"NoStorage\" | Static -> \"Static\" | Register -> \"Register\" | Extern -> \"Extern\") m\nand exp m = \"Exp { eid = \" ^ int m.eid ^ \", enode = \" ^ exp_node m.enode ^ \" }\"\nand exp_node m = (function Const m1 -> \"Const\" ^ \" \" ^ constant m1 | Lval m1 -> \"Lval\" ^ \" \" ^ lval m1 | SizeOf m1 -> \"SizeOf\" ^ \" \" ^ typ m1 | SizeOfE m1 -> \"SizeOfE\" ^ \" \" ^ exp m1 | SizeOfStr m1 -> \"SizeOfStr\" ^ \" \" ^ string m1 | AlignOf m1 -> \"AlignOf\" ^ \" \" ^ typ m1 | AlignOfE m1 -> \"AlignOfE\" ^ \" \" ^ exp m1 | UnOp (m1, m2, m3) -> \"UnOp\" ^ \" \" ^ (\"(\" ^ unop m1 ^ \")\") ^ \" \" ^ (\"(\" ^ exp m2 ^ \")\") ^ \" \" ^ (\"(\" ^ typ m3 ^ \")\") | BinOp (m1, m2, m3, m4) -> \"BinOp\" ^ \" \" ^ (\"(\" ^ binop m1 ^ \")\") ^ \" \" ^ (\"(\" ^ exp m2 ^ \")\") ^ \" \" ^ (\"(\" ^ exp m3 ^ \")\") ^ \" \" ^ (\"(\" ^ typ m4 ^ \")\") | CastE (m1, m2) -> \"CastE\" ^ \" \" ^ (\"(\" ^ typ m1 ^ \")\") ^ \" \" ^ (\"(\" ^ exp m2 ^ \")\") | AddrOf m1 -> \"AddrOf\" ^ \" \" ^ lval m1 | StartOf m1 -> \"StartOf\" ^ \" \" ^ lval m1 | Info (m1, m2) -> \"Info\" ^ \" \" ^ (\"(\" ^ exp m1 ^ \")\") ^ \" \" ^ (\"(\" ^ exp_info m2 ^ \")\")) m\nand exp_info m = \"Exp_info { exp_loc = \" ^ location m.exp_loc ^ \", exp_type = \" ^ logic_type m.exp_type ^ \", exp_name = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.exp_name ^ \" }\"\nand constant m = (function CInt64 (m1, m2, m3) -> \"CInt64\" ^ \" \" ^ (\"(\" ^ int64 m1 ^ \")\") ^ \" \" ^ (\"(\" ^ ikind m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ string m ^ \")\")) m3 ^ \")\") | CStr m1 -> \"CStr\" ^ \" \" ^ string m1 | CWStr m1 -> \"CWStr\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (int64) m) ^ \" ]\") m1 | CChr m1 -> \"CChr\" ^ \" \" ^ char m1 | CReal (m1, m2, m3) -> \"CReal\" ^ \" \" ^ (\"(\" ^ float m1 ^ \")\") ^ \" \" ^ (\"(\" ^ fkind m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ string m ^ \")\")) m3 ^ \")\") | CEnum m1 -> \"CEnum\" ^ \" \" ^ enumitem m1) m\nand unop m = (function Neg -> \"Neg\" | BNot -> \"BNot\" | LNot -> \"LNot\") m\nand binop m = (function PlusA -> \"PlusA\" | PlusPI -> \"PlusPI\" | IndexPI -> \"IndexPI\" | MinusA -> \"MinusA\" | MinusPI -> \"MinusPI\" | MinusPP -> \"MinusPP\" | Mult -> \"Mult\" | Div -> \"Div\" | Mod -> \"Mod\" | Shiftlt -> \"Shiftlt\" | Shiftrt -> \"Shiftrt\" | Lt -> \"Lt\" | Gt -> \"Gt\" | Le -> \"Le\" | Ge -> \"Ge\" | Eq -> \"Eq\" | Ne -> \"Ne\" | BAnd -> \"BAnd\" | BXor -> \"BXor\" | BOr -> \"BOr\" | LAnd -> \"LAnd\" | LOr -> \"LOr\") m\nand lval m = (function (m1, m2) -> (\"(\" ^ (\"(\" ^ lhost m1 ^ \")\") ^ \", \" ^ (\"(\" ^ offset m2 ^ \")\") ^ \")\")) m\nand lhost m = (function Var m1 -> \"Var\" ^ \" \" ^ varinfo m1 | Mem m1 -> \"Mem\" ^ \" \" ^ exp m1) m\nand offset m = (function NoOffset -> \"NoOffset\" | Field (m1, m2) -> \"Field\" ^ \" \" ^ (\"(\" ^ fieldinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ offset m2 ^ \")\") | Index (m1, m2) -> \"Index\" ^ \" \" ^ (\"(\" ^ exp m1 ^ \")\") ^ \" \" ^ (\"(\" ^ offset m2 ^ \")\")) m\nand init m = (function SingleInit m1 -> \"SingleInit\" ^ \" \" ^ exp m1 | CompoundInit (m1, m2) -> \"CompoundInit\" ^ \" \" ^ (\"(\" ^ typ m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2) -> (\"(\" ^ (\"(\" ^ offset m1 ^ \")\") ^ \", \" ^ (\"(\" ^ init m2 ^ \")\") ^ \")\"))) m) ^ \" ]\") m2 ^ \")\")) m\nand initinfo m = \"Initinfo { init = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ init m ^ \")\")) m.init ^ \" }\"\nand fundec m = \"Fundec { svar = \" ^ varinfo m.svar ^ \", sformals = \" ^ (function m -> \"[ \" ^ concat \", \" (map (varinfo) m) ^ \" ]\") m.sformals ^ \", slocals = \" ^ (function m -> \"[ \" ^ concat \", \" (map (varinfo) m) ^ \" ]\") m.slocals ^ \", smaxid = \" ^ int m.smaxid ^ \", sbody = \" ^ block m.sbody ^ \", smaxstmtid = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ int m ^ \")\")) m.smaxstmtid ^ \", sallstmts = \" ^ (function m -> \"[ \" ^ concat \", \" (map (stmt) m) ^ \" ]\") m.sallstmts ^ \", sspec = \" ^ funspec m.sspec ^ \" }\"\nand block m = \"Block { battrs = \" ^ attributes m.battrs ^ \", blocals = \" ^ (function m -> \"[ \" ^ concat \", \" (map (varinfo) m) ^ \" ]\") m.blocals ^ \", bstmts = \" ^ (function m -> \"[ \" ^ concat \", \" (map (stmt) m) ^ \" ]\") m.bstmts ^ \" }\"\nand stmt m = \"Stmt { labels = \" ^ (function m -> \"[ \" ^ concat \", \" (map (label) m) ^ \" ]\") m.labels ^ \", skind = \" ^ stmtkind m.skind ^ \", sid = \" ^ int m.sid ^ \", succs = \" ^ (function m -> \"[ \" ^ concat \", \" (map (stmt) m) ^ \" ]\") m.succs ^ \", preds = \" ^ (function m -> \"[ \" ^ concat \", \" (map (stmt) m) ^ \" ]\") m.preds ^ \", ghost = \" ^ bool m.ghost ^ \" }\"\nand label m = (function Label (m1, m2, m3) -> \"Label\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") ^ \" \" ^ (\"(\" ^ bool m3 ^ \")\") | Case (m1, m2) -> \"Case\" ^ \" \" ^ (\"(\" ^ exp m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | Default m1 -> \"Default\" ^ \" \" ^ location m1) m\nand stmtkind m = (function Instr m1 -> \"Instr\" ^ \" \" ^ instr m1 | Return (m1, m2) -> \"Return\" ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ exp m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | Goto (m1, m2) -> \"Goto\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ stmt (!m) ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\") | Break m1 -> \"Break\" ^ \" \" ^ location m1 | Continue m1 -> \"Continue\" ^ \" \" ^ location m1 | If (m1, m2, m3, m4) -> \"If\" ^ \" \" ^ (\"(\" ^ exp m1 ^ \")\") ^ \" \" ^ (\"(\" ^ block m2 ^ \")\") ^ \" \" ^ (\"(\" ^ block m3 ^ \")\") ^ \" \" ^ (\"(\" ^ location m4 ^ \")\") | Switch (m1, m2, m3, m4) -> \"Switch\" ^ \" \" ^ (\"(\" ^ exp m1 ^ \")\") ^ \" \" ^ (\"(\" ^ block m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (stmt) m) ^ \" ]\") m3 ^ \")\") ^ \" \" ^ (\"(\" ^ location m4 ^ \")\") | Loop (m1, m2, m3, m4, m5) -> \"Loop\" ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (code_annotation) m) ^ \" ]\") m1 ^ \")\") ^ \" \" ^ (\"(\" ^ block m2 ^ \")\") ^ \" \" ^ (\"(\" ^ location m3 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ stmt m ^ \")\")) m4 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ stmt m ^ \")\")) m5 ^ \")\") | Block m1 -> \"Block'\" ^ \" \" ^ block m1 | UnspecifiedSequence m1 -> \"UnspecifiedSequence\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2, m3, m4) -> (\"(\" ^ (\"(\" ^ stmt m1 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (lval) m) ^ \" ]\") m2 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (lval) m) ^ \" ]\") m3 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (lval) m) ^ \" ]\") m4 ^ \")\") ^ \")\"))) m) ^ \" ]\") m1 | TryFinally (m1, m2, m3) -> \"TryFinally\" ^ \" \" ^ (\"(\" ^ block m1 ^ \")\") ^ \" \" ^ (\"(\" ^ block m2 ^ \")\") ^ \" \" ^ (\"(\" ^ location m3 ^ \")\") | TryExcept (m1, m2, m3, m4) -> \"TryExcept\" ^ \" \" ^ (\"(\" ^ block m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function (m1, m2) -> (\"(\" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (instr) m) ^ \" ]\") m1 ^ \")\") ^ \", \" ^ (\"(\" ^ exp m2 ^ \")\") ^ \")\")) m2 ^ \")\") ^ \" \" ^ (\"(\" ^ block m3 ^ \")\") ^ \" \" ^ (\"(\" ^ location m4 ^ \")\")) m\nand instr m = (function Set (m1, m2, m3) -> \"Set\" ^ \" \" ^ (\"(\" ^ lval m1 ^ \")\") ^ \" \" ^ (\"(\" ^ exp m2 ^ \")\") ^ \" \" ^ (\"(\" ^ location m3 ^ \")\") | Call (m1, m2, m3, m4) -> \"Call\" ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ lval m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ exp m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (exp) m) ^ \" ]\") m3 ^ \")\") ^ \" \" ^ (\"(\" ^ location m4 ^ \")\") | Asm (m1, m2, m3, m4, m5, m6) -> \"Asm\" ^ \" \" ^ (\"(\" ^ attributes m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2, m3) -> (\"(\" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ string m ^ \")\")) m1 ^ \")\") ^ \", \" ^ (\"(\" ^ string m2 ^ \")\") ^ \", \" ^ (\"(\" ^ lval m3 ^ \")\") ^ \")\"))) m) ^ \" ]\") m3 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2, m3) -> (\"(\" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ string m ^ \")\")) m1 ^ \")\") ^ \", \" ^ (\"(\" ^ string m2 ^ \")\") ^ \", \" ^ (\"(\" ^ exp m3 ^ \")\") ^ \")\"))) m) ^ \" ]\") m4 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m5 ^ \")\") ^ \" \" ^ (\"(\" ^ location m6 ^ \")\") | Skip m1 -> \"Skip\" ^ \" \" ^ location m1 | Code_annot (m1, m2) -> \"Code_annot\" ^ \" \" ^ (\"(\" ^ code_annotation m1 ^ \")\") ^ \" \" ^ (\"(\" ^ location m2 ^ \")\")) m\nand location m = (function (m1, m2) -> (\"(\" ^ (\"(\" ^ position m1 ^ \")\") ^ \", \" ^ (\"(\" ^ position m2 ^ \")\") ^ \")\")) m\nand typsig m = (function TSArray (m1, m2, m3) -> \"TSArray\" ^ \" \" ^ (\"(\" ^ typsig m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ int64 m ^ \")\")) m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attribute) m) ^ \" ]\") m3 ^ \")\") | TSPtr (m1, m2) -> \"TSPtr\" ^ \" \" ^ (\"(\" ^ typsig m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attribute) m) ^ \" ]\") m2 ^ \")\") | TSComp (m1, m2, m3) -> \"TSComp\" ^ \" \" ^ (\"(\" ^ bool m1 ^ \")\") ^ \" \" ^ (\"(\" ^ string m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attribute) m) ^ \" ]\") m3 ^ \")\") | TSFun (m1, m2, m3, m4) -> \"TSFun\" ^ \" \" ^ (\"(\" ^ typsig m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (typsig) m) ^ \" ]\") m2 ^ \")\") ^ \" \" ^ (\"(\" ^ bool m3 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attribute) m) ^ \" ]\") m4 ^ \")\") | TSEnum (m1, m2) -> \"TSEnum\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (attribute) m) ^ \" ]\") m2 ^ \")\") | TSBase m1 -> \"TSBase\" ^ \" \" ^ typ m1) m\nand logic_type m = (function Ctype m1 -> \"Ctype\" ^ \" \" ^ typ m1 | Ltype (m1, m2) -> \"Ltype\" ^ \" \" ^ (\"(\" ^ logic_type_info m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_type) m) ^ \" ]\") m2 ^ \")\") | Lvar m1 -> \"Lvar\" ^ \" \" ^ string m1 | Linteger -> \"Linteger\" | Lreal -> \"Lreal\" | Larrow (m1, m2) -> \"Larrow\" ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_type) m) ^ \" ]\") m1 ^ \")\") ^ \" \" ^ (\"(\" ^ logic_type m2 ^ \")\")) m\nand identified_term m = \"Identified_term { it_id = \" ^ int m.it_id ^ \", it_content = \" ^ term m.it_content ^ \" }\"\nand logic_label m = (function StmtLabel m1 -> \"StmtLabel\" ^ \" \" ^ (function m -> (\"(\" ^ stmt (!m) ^ \")\")) m1 | LogicLabel m1 -> \"LogicLabel\" ^ \" \" ^ string m1) m\nand term m = \"Term { term_node = \" ^ term_node m.term_node ^ \", term_loc = \" ^ (function (m1, m2) -> (\"(\" ^ (\"(\" ^ position m1 ^ \")\") ^ \", \" ^ (\"(\" ^ position m2 ^ \")\") ^ \")\")) m.term_loc ^ \", term_type = \" ^ logic_type m.term_type ^ \", term_name = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.term_name ^ \" }\"\nand term_node m = (function TConst m1 -> \"TConst\" ^ \" \" ^ constant m1 | TLval m1 -> \"TLval\" ^ \" \" ^ term_lval m1 | TSizeOf m1 -> \"TSizeOf\" ^ \" \" ^ typ m1 | TSizeOfE m1 -> \"TSizeOfE\" ^ \" \" ^ term m1 | TSizeOfStr m1 -> \"TSizeOfStr\" ^ \" \" ^ string m1 | TAlignOf m1 -> \"TAlignOf\" ^ \" \" ^ typ m1 | TAlignOfE m1 -> \"TAlignOfE\" ^ \" \" ^ term m1 | TUnOp (m1, m2) -> \"TUnOp\" ^ \" \" ^ (\"(\" ^ unop m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") | TBinOp (m1, m2, m3) -> \"TBinOp\" ^ \" \" ^ (\"(\" ^ binop m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") ^ \" \" ^ (\"(\" ^ term m3 ^ \")\") | TCastE (m1, m2) -> \"TCastE\" ^ \" \" ^ (\"(\" ^ typ m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") | TAddrOf m1 -> \"TAddrOf\" ^ \" \" ^ term_lval m1 | TStartOf m1 -> \"TStartOf\" ^ \" \" ^ term_lval m1 | Tapp (m1, m2, m3) -> \"Tapp\" ^ \" \" ^ (\"(\" ^ logic_info m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2) -> (\"(\" ^ (\"(\" ^ logic_label m1 ^ \")\") ^ \", \" ^ (\"(\" ^ logic_label m2 ^ \")\") ^ \")\"))) m) ^ \" ]\") m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m3 ^ \")\") | Tlambda (m1, m2) -> \"Tlambda\" ^ \" \" ^ (\"(\" ^ quantifiers m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") | TDataCons (m1, m2) -> \"TDataCons\" ^ \" \" ^ (\"(\" ^ logic_ctor_info m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m2 ^ \")\") | Tif (m1, m2, m3) -> \"Tif\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") ^ \" \" ^ (\"(\" ^ term m3 ^ \")\") | Told m1 -> \"Told\" ^ \" \" ^ term m1 | Tat (m1, m2) -> \"Tat\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ logic_label m2 ^ \")\") | Tbase_addr m1 -> \"Tbase_addr\" ^ \" \" ^ term m1 | Tblock_length m1 -> \"Tblock_length\" ^ \" \" ^ term m1 | Tnull -> \"Tnull\" | TCoerce (m1, m2) -> \"TCoerce\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ typ m2 ^ \")\") | TCoerceE (m1, m2) -> \"TCoerceE\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") | TUpdate (m1, m2, m3) -> \"TUpdate\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ fieldinfo m2 ^ \")\") ^ \" \" ^ (\"(\" ^ term m3 ^ \")\") | Ttypeof m1 -> \"Ttypeof\" ^ \" \" ^ term m1 | Ttype m1 -> \"Ttype\" ^ \" \" ^ typ m1 | Tempty_set -> \"Tempty_set\" | Tunion m1 -> \"Tunion\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m1 | Tinter m1 -> \"Tinter\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m1 | Tcomprehension (m1, m2, m3) -> \"Tcomprehension\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ quantifiers m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m ^ \")\")) m3 ^ \")\") | Trange (m1, m2) -> \"Trange\" ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ term m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ term m ^ \")\")) m2 ^ \")\") | Tlet (m1, m2) -> \"Tlet\" ^ \" \" ^ (\"(\" ^ logic_info m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\")) m\nand term_lval m = (function (m1, m2) -> (\"(\" ^ (\"(\" ^ term_lhost m1 ^ \")\") ^ \", \" ^ (\"(\" ^ term_offset m2 ^ \")\") ^ \")\")) m\nand term_lhost m = (function TVar m1 -> \"TVar\" ^ \" \" ^ logic_var m1 | TResult m1 -> \"TResult\" ^ \" \" ^ typ m1 | TMem m1 -> \"TMem\" ^ \" \" ^ term m1) m\nand term_offset m = (function TNoOffset -> \"TNoOffset\" | TField (m1, m2) -> \"TField\" ^ \" \" ^ (\"(\" ^ fieldinfo m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term_offset m2 ^ \")\") | TIndex (m1, m2) -> \"TIndex\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term_offset m2 ^ \")\")) m\nand logic_info m = \"Logic_info { l_var_info = \" ^ logic_var m.l_var_info ^ \", l_labels = \" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_label) m) ^ \" ]\") m.l_labels ^ \", l_tparams = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.l_tparams ^ \", l_type = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ logic_type m ^ \")\")) m.l_type ^ \", l_profile = \" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_var) m) ^ \" ]\") m.l_profile ^ \", l_body = \" ^ logic_body m.l_body ^ \" }\"\nand builtin_logic_info m = \"Builtin_logic_info { bl_name = \" ^ string m.bl_name ^ \", bl_labels = \" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_label) m) ^ \" ]\") m.bl_labels ^ \", bl_params = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.bl_params ^ \", bl_type = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ logic_type m ^ \")\")) m.bl_type ^ \", bl_profile = \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2) -> (\"(\" ^ (\"(\" ^ string m1 ^ \")\") ^ \", \" ^ (\"(\" ^ logic_type m2 ^ \")\") ^ \")\"))) m) ^ \" ]\") m.bl_profile ^ \" }\"\nand logic_body m = (function LBnone -> \"LBnone\" | LBreads m1 -> \"LBreads\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (identified_term) m) ^ \" ]\") m1 | LBterm m1 -> \"LBterm\" ^ \" \" ^ term m1 | LBpred m1 -> \"LBpred\" ^ \" \" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 | LBinductive m1 -> \"LBinductive\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2, m3, m4) -> (\"(\" ^ (\"(\" ^ string m1 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_label) m) ^ \" ]\") m2 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m3 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m4 ^ \")\") ^ \")\"))) m) ^ \" ]\") m1) m\nand logic_type_info m = \"Logic_type_info { lt_name = \" ^ string m.lt_name ^ \", lt_params = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.lt_params ^ \", lt_def = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ logic_type_def m ^ \")\")) m.lt_def ^ \" }\"\nand logic_type_def m = (function LTsum m1 -> \"LTsum\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_ctor_info) m) ^ \" ]\") m1 | LTsyn m1 -> \"LTsyn\" ^ \" \" ^ logic_type m1) m\nand logic_var m = \"Logic_var { lv_name = \" ^ string m.lv_name ^ \", lv_id = \" ^ int m.lv_id ^ \", lv_type = \" ^ logic_type m.lv_type ^ \", lv_origin = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ varinfo m ^ \")\")) m.lv_origin ^ \" }\"\nand logic_ctor_info m = \"Logic_ctor_info { ctor_name = \" ^ string m.ctor_name ^ \", ctor_type = \" ^ logic_type_info m.ctor_type ^ \", ctor_params = \" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_type) m) ^ \" ]\") m.ctor_params ^ \" }\"\nand quantifiers m = (function m -> \"[ \" ^ concat \", \" (map (logic_var) m) ^ \" ]\") m\nand relation m = (function Rlt -> \"Rlt\" | Rgt -> \"Rgt\" | Rle -> \"Rle\" | Rge -> \"Rge\" | Req -> \"Req\" | Rneq -> \"Rneq\") m\nand predicate m = (function Pfalse -> \"Pfalse\" | Ptrue -> \"Ptrue\" | Papp (m1, m2, m3) -> \"Papp\" ^ \" \" ^ (\"(\" ^ logic_info m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2) -> (\"(\" ^ (\"(\" ^ logic_label m1 ^ \")\") ^ \", \" ^ (\"(\" ^ logic_label m2 ^ \")\") ^ \")\"))) m) ^ \" ]\") m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m3 ^ \")\") | Pseparated m1 -> \"Pseparated\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m1 | Prel (m1, m2, m3) -> \"Prel\" ^ \" \" ^ (\"(\" ^ relation m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") ^ \" \" ^ (\"(\" ^ term m3 ^ \")\") | Pand (m1, m2) -> \"Pand\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Por (m1, m2) -> \"Por\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Pxor (m1, m2) -> \"Pxor\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Pimplies (m1, m2) -> \"Pimplies\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Piff (m1, m2) -> \"Piff\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Pnot m1 -> \"Pnot\" ^ \" \" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 | Pif (m1, m2, m3) -> \"Pif\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m3 ^ \")\") | Plet (m1, m2) -> \"Plet\" ^ \" \" ^ (\"(\" ^ logic_info m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Pforall (m1, m2) -> \"Pforall\" ^ \" \" ^ (\"(\" ^ quantifiers m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Pexists (m1, m2) -> \"Pexists\" ^ \" \" ^ (\"(\" ^ quantifiers m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m2 ^ \")\") | Pold m1 -> \"Pold\" ^ \" \" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 | Pat (m1, m2) -> \"Pat\" ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \" \" ^ (\"(\" ^ logic_label m2 ^ \")\") | Pvalid m1 -> \"Pvalid\" ^ \" \" ^ term m1 | Pvalid_index (m1, m2) -> \"Pvalid_index\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") | Pvalid_range (m1, m2, m3) -> \"Pvalid_range\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\") ^ \" \" ^ (\"(\" ^ term m3 ^ \")\") | Pfresh m1 -> \"Pfresh\" ^ \" \" ^ term m1 | Psubtype (m1, m2) -> \"Psubtype\" ^ \" \" ^ (\"(\" ^ term m1 ^ \")\") ^ \" \" ^ (\"(\" ^ term m2 ^ \")\")) m\nand identified_predicate m = \"Identified_predicate { ip_name = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.ip_name ^ \", ip_loc = \" ^ location m.ip_loc ^ \", ip_id = \" ^ int m.ip_id ^ \", ip_content = \" ^ predicate m.ip_content ^ \" }\"\nand variant term m = (function (m1, m2) -> (\"(\" ^ (\"(\" ^ term m1 ^ \")\") ^ \", \" ^ (\"(\" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ string m ^ \")\")) m2 ^ \")\") ^ \")\")) m\nand zone locs m = (function Location m1 -> \"Location\" ^ \" \" ^ locs m1 | Nothing -> \"Nothing\") m\nand assigns locs m = (function (m1, m2) -> (\"(\" ^ (\"(\" ^ (function m -> (\"(\" ^ zone (function m -> (\"(\" ^ locs m ^ \")\")) m ^ \")\")) m1 ^ \")\") ^ \", \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map ((function m -> (\"(\" ^ zone (function m -> (\"(\" ^ locs m ^ \")\")) m ^ \")\"))) m) ^ \" ]\") m2 ^ \")\") ^ \")\")) m\nand named a m = \"Named { name = \" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m.name ^ \", loc = \" ^ location m.loc ^ \", content = \" ^ a m.content ^ \" }\"\nand spec term pred locs m = \"Spec { spec_requires = \" ^ (function m -> \"[ \" ^ concat \", \" (map (pred) m) ^ \" ]\") m.spec_requires ^ \", spec_behavior = \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function m -> (\"(\" ^ behavior (function m -> (\"(\" ^ pred m ^ \")\")) (function m -> (\"(\" ^ locs m ^ \")\")) m ^ \")\"))) m) ^ \" ]\") m.spec_behavior ^ \", spec_variant = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ (function m -> (\"(\" ^ variant (function m -> (\"(\" ^ term m ^ \")\")) m ^ \")\")) m ^ \")\")) m.spec_variant ^ \", spec_terminates = \" ^ (function None -> \"Nothing\" | Some m -> \"Just \" ^ (\"(\" ^ pred m ^ \")\")) m.spec_terminates ^ \", spec_complete_behaviors = \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\")) m) ^ \" ]\") m.spec_complete_behaviors ^ \", spec_disjoint_behaviors = \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\")) m) ^ \" ]\") m.spec_disjoint_behaviors ^ \" }\"\nand behavior pred locs m = \"Behavior { b_name = \" ^ string m.b_name ^ \", b_assumes = \" ^ (function m -> \"[ \" ^ concat \", \" (map (pred) m) ^ \" ]\") m.b_assumes ^ \", b_post_cond = \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function (m1, m2) -> (\"(\" ^ (\"(\" ^ termination_kind m1 ^ \")\") ^ \", \" ^ (\"(\" ^ pred m2 ^ \")\") ^ \")\"))) m) ^ \" ]\") m.b_post_cond ^ \", b_assigns = \" ^ (function m -> \"[ \" ^ concat \", \" (map ((function m -> (\"(\" ^ assigns (function m -> (\"(\" ^ locs m ^ \")\")) m ^ \")\"))) m) ^ \" ]\") m.b_assigns ^ \" }\"\nand loop_pragma term m = (function Unroll_level m1 -> \"Unroll_level\" ^ \" \" ^ term m1 | Widen_hints m1 -> \"Widen_hints\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m1 | Widen_variables m1 -> \"Widen_variables\" ^ \" \" ^ (function m -> \"[ \" ^ concat \", \" (map (term) m) ^ \" ]\") m1) m\nand slice_pragma term m = (function SPexpr m1 -> \"SPexpr\" ^ \" \" ^ term m1 | SPctrl -> \"SPctrl\" | SPstmt -> \"SPstmt\") m\nand impact_pragma term m = (function IPexpr m1 -> \"IPexpr\" ^ \" \" ^ term m1 | IPstmt -> \"IPstmt\") m\nand pragma term m = (function Loop_pragma m1 -> \"Loop_pragma\" ^ \" \" ^ (function m -> (\"(\" ^ loop_pragma (function m -> (\"(\" ^ term m ^ \")\")) m ^ \")\")) m1 | Slice_pragma m1 -> \"Slice_pragma\" ^ \" \" ^ (function m -> (\"(\" ^ slice_pragma (function m -> (\"(\" ^ term m ^ \")\")) m ^ \")\")) m1 | Impact_pragma m1 -> \"Impact_pragma\" ^ \" \" ^ (function m -> (\"(\" ^ impact_pragma (function m -> (\"(\" ^ term m ^ \")\")) m ^ \")\")) m1) m\nand validity m = (function True -> \"True\" | False -> \"False\" | Maybe -> \"Maybe\") m\nand annot_checked_status m = \"Annot_checked_status { emitter = \" ^ string m.emitter ^ \", valid = \" ^ validity m.valid ^ \" }\"\nand annotation_status m = (function Unknown -> \"Unknown\" | Checked m1 -> \"Checked\" ^ \" \" ^ annot_checked_status m1) m\nand annot_status m = \"Annot_status { status = \" ^ annotation_status m.status ^ \" }\"\nand code_annot term pred spec_pred locs m = (function AAssert (m1, m2, m3) -> \"AAssert\" ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m1 ^ \")\") ^ \" \" ^ (\"(\" ^ pred m2 ^ \")\") ^ \" \" ^ (\"(\" ^ annot_status m3 ^ \")\") | AStmtSpec m1 -> \"AStmtSpec\" ^ \" \" ^ (function m -> (\"(\" ^ spec (function m -> (\"(\" ^ term m ^ \")\")) (function m -> (\"(\" ^ spec_pred m ^ \")\")) (function m -> (\"(\" ^ locs m ^ \")\")) m ^ \")\")) m1 | AInvariant (m1, m2, m3) -> \"AInvariant\" ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m1 ^ \")\") ^ \" \" ^ (\"(\" ^ bool m2 ^ \")\") ^ \" \" ^ (\"(\" ^ pred m3 ^ \")\") | AVariant m1 -> \"AVariant\" ^ \" \" ^ (function m -> (\"(\" ^ variant (function m -> (\"(\" ^ term m ^ \")\")) m ^ \")\")) m1 | AAssigns (m1, m2) -> \"AAssigns\" ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ assigns (function m -> (\"(\" ^ locs m ^ \")\")) m ^ \")\")) m2 ^ \")\") | APragma m1 -> \"APragma\" ^ \" \" ^ (function m -> (\"(\" ^ pragma (function m -> (\"(\" ^ term m ^ \")\")) m ^ \")\")) m1) m\nand funspec m = (function m -> (\"(\" ^ spec (function m -> (\"(\" ^ term m ^ \")\")) (function m -> (\"(\" ^ identified_predicate m ^ \")\")) (function m -> (\"(\" ^ identified_term m ^ \")\")) m ^ \")\")) m\nand code_annotation m = \"Code_annotation { annot_content = \" ^ (function m -> (\"(\" ^ code_annot (function m -> (\"(\" ^ term m ^ \")\")) (function m -> (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m ^ \")\")) (function m -> (\"(\" ^ identified_predicate m ^ \")\")) (function m -> (\"(\" ^ identified_term m ^ \")\")) m ^ \")\")) m.annot_content ^ \", annot_id = \" ^ int m.annot_id ^ \" }\"\nand funbehavior m = (function m -> (\"(\" ^ behavior (function m -> (\"(\" ^ identified_predicate m ^ \")\")) (function m -> (\"(\" ^ identified_term m ^ \")\")) m ^ \")\")) m\nand global_annotation m = (function Dfun_or_pred m1 -> \"Dfun_or_pred\" ^ \" \" ^ logic_info m1 | Daxiomatic (m1, m2) -> \"Daxiomatic\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (global_annotation) m) ^ \" ]\") m2 ^ \")\") | Dtype m1 -> \"Dtype\" ^ \" \" ^ logic_type_info m1 | Dlemma (m1, m2, m3, m4, m5) -> \"Dlemma\" ^ \" \" ^ (\"(\" ^ string m1 ^ \")\") ^ \" \" ^ (\"(\" ^ bool m2 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (logic_label) m) ^ \" ]\") m3 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> \"[ \" ^ concat \", \" (map (string) m) ^ \" ]\") m4 ^ \")\") ^ \" \" ^ (\"(\" ^ (function m -> (\"(\" ^ named (function m -> (\"(\" ^ predicate m ^ \")\")) m ^ \")\")) m5 ^ \")\") | Dinvariant m1 -> \"Dinvariant\" ^ \" \" ^ logic_info m1 | Dtype_annot m1 -> \"Dtype_annot\" ^ \" \" ^ logic_info m1) m\nand kinstr m = (function Kstmt m1 -> \"Kstmt\" ^ \" \" ^ stmt m1 | Kglobal -> \"Kglobal\") m\nand mach m = \"Mach { version_major = \" ^ int m.version_major ^ \", version_minor = \" ^ int m.version_minor ^ \", version = \" ^ string m.version ^ \", underscore_name = \" ^ bool m.underscore_name ^ \", sizeof_short = \" ^ int m.sizeof_short ^ \", sizeof_int = \" ^ int m.sizeof_int ^ \", sizeof_long = \" ^ int m.sizeof_long ^ \", sizeof_longlong = \" ^ int m.sizeof_longlong ^ \", sizeof_ptr = \" ^ int m.sizeof_ptr ^ \", sizeof_enum = \" ^ int m.sizeof_enum ^ \", sizeof_float = \" ^ int m.sizeof_float ^ \", sizeof_double = \" ^ int m.sizeof_double ^ \", sizeof_longdouble = \" ^ int m.sizeof_longdouble ^ \", sizeof_void = \" ^ int m.sizeof_void ^ \", sizeof_fun = \" ^ int m.sizeof_fun ^ \", size_t = \" ^ string m.size_t ^ \", wchar_t = \" ^ string m.wchar_t ^ \", ptrdiff_t = \" ^ string m.ptrdiff_t ^ \", enum_are_signed = \" ^ bool m.enum_are_signed ^ \", alignof_short = \" ^ int m.alignof_short ^ \", alignof_int = \" ^ int m.alignof_int ^ \", alignof_long = \" ^ int m.alignof_long ^ \", alignof_longlong = \" ^ int m.alignof_longlong ^ \", alignof_ptr = \" ^ int m.alignof_ptr ^ \", alignof_enum = \" ^ int m.alignof_enum ^ \", alignof_float = \" ^ int m.alignof_float ^ \", alignof_double = \" ^ int m.alignof_double ^ \", alignof_longdouble = \" ^ int m.alignof_longdouble ^ \", alignof_str = \" ^ int m.alignof_str ^ \", alignof_fun = \" ^ int m.alignof_fun ^ \", alignof_char_array = \" ^ int m.alignof_char_array ^ \", char_is_unsigned = \" ^ bool m.char_is_unsigned ^ \", const_string_literals = \" ^ bool m.const_string_literals ^ \", little_endian = \" ^ bool m.little_endian ^ \" }\"\n\nlet run () =\n File.init_from_cmdline ();\n print_endline (file (Ast.get ()))\n\nmodule Self =\n Plugin.Register\n (struct\n let name = \"dumpcil\"\n let shortname = \"dumpcil\"\n let descr = \"Dumps CIL and ACSL to stdout to be read by Haskell CIL.\"\n end);;\n\nmodule Enabled =\n Self.False\n (struct\n let option_name = \"-dumpcil\"\n let descr = \"Dumps CIL and ACSL to stdout to be read by Haskell CIL.\"\n end);;\n\nlet () = Db.Main.extend (fun () -> if Enabled.get () then run ())\n" + putStrLn "running 'make' to compile dumpcil plugin ..." + system "cd install-dumpcil-plugin && make" + putStrLn "running 'make install' to install dumpcil plugin ..." + system "cd install-dumpcil-plugin && make install" + return () --- Imported from other files :- +data Exn = Exn deriving (Show, Read, Eq) {-! derive : Parse !-} +data Position = Position FilePath Int Int deriving (Show, Read, Eq) {-! derive : Parse !-} +data Int64 = Int64 deriving (Show, Read, Eq) {-! derive : Parse !-} + +data BitsSizeofTyp = Not_Computed | Not_Computable (Exn) | Computed (Int) deriving (Show, Read, Eq) {-! derive : Parse !-} +data BitsSizeofTypCache = BitsSizeofTypCache { scache :: BitsSizeofTyp } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Termination_kind = Normal | Exits | Breaks | Continues | Returns deriving (Show, Read, Eq) {-! derive : Parse !-} +data File = File { fileName :: String, globals :: [Global], globinit :: Maybe (Fundec), globinitcalled :: Bool } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Global = GType (Typeinfo) (Location) | GCompTag (Compinfo) (Location) | GCompTagDecl (Compinfo) (Location) | GEnumTag (Enuminfo) (Location) | GEnumTagDecl (Enuminfo) (Location) | GVarDecl (Funspec) (Varinfo) (Location) | GVar (Varinfo) (Initinfo) (Location) | GFun (Fundec) (Location) | GAsm (String) (Location) | GPragma (Attribute) (Location) | GText (String) | GAnnot (Global_annotation) (Location) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Typ = TVoid (Attributes) | TInt (Ikind) (Attributes) | TFloat (Fkind) (Attributes) | TPtr (Typ) (Attributes) | TArray (Typ) (Maybe (Exp)) (BitsSizeofTypCache) (Attributes) | TFun (Typ) (Maybe ([(String, Typ, Attributes)])) (Bool) (Attributes) | TNamed (Typeinfo) (Attributes) | TComp (Compinfo) (BitsSizeofTypCache) (Attributes) | TEnum (Enuminfo) (Attributes) | TBuiltin_va_list (Attributes) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Ikind = IBool | IChar | ISChar | IUChar | IInt | IUInt | IShort | IUShort | ILong | IULong | ILongLong | IULongLong deriving (Show, Read, Eq) {-! derive : Parse !-} +data Fkind = FFloat | FDouble | FLongDouble deriving (Show, Read, Eq) {-! derive : Parse !-} +data Attribute = Attr (String) ([Attrparam]) | AttrAnnot (String) deriving (Show, Read, Eq) {-! derive : Parse !-} +type Attributes = [Attribute] +data Attrparam = AInt (Int) | AStr (String) | ACons (String) ([Attrparam]) | ASizeOf (Typ) | ASizeOfE (Attrparam) | ASizeOfS (Typsig) | AAlignOf (Typ) | AAlignOfE (Attrparam) | AAlignOfS (Typsig) | AUnOp (Unop) (Attrparam) | ABinOp (Binop) (Attrparam) (Attrparam) | ADot (Attrparam) (String) | AStar (Attrparam) | AAddrOf (Attrparam) | AIndex (Attrparam) (Attrparam) | AQuestion (Attrparam) (Attrparam) (Attrparam) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Compinfo = Compinfo { cstruct :: Bool, cname :: String, ckey :: Int, cfields :: [Fieldinfo], cattr :: Attributes, cdefined :: Bool, creferenced :: Bool } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Fieldinfo = Fieldinfo { fcomp :: Compinfo, fname :: String, ftype :: Typ, fbitfield :: Maybe (Int), fattr :: Attributes, floc :: Location, faddrof :: Bool, fsize_in_bits :: Maybe (Int), foffset_in_bits :: Maybe (Int), fpadding_in_bits :: Maybe (Int) } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Enuminfo = Enuminfo { ename :: String, eitems :: [Enumitem], eattr :: Attributes, ereferenced :: Bool } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Enumitem = Enumitem { einame :: String, eival :: Exp, eihost :: Enuminfo, eiloc :: Location } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Typeinfo = Typeinfo { tname :: String, ttype :: Typ, treferenced :: Bool } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Varinfo = Varinfo { vname :: String, vorig_name :: String, vtype :: Typ, vattr :: Attributes, vstorage :: Storage, vglob :: Bool, vdefined :: Bool, vformal :: Bool, vinline :: Bool, vdecl :: Location, vid :: Int, vaddrof :: Bool, vreferenced :: Bool, vgenerated :: Bool, vdescr :: Maybe (String), vdescrpure :: Bool, vghost :: Bool, vlogic :: Bool, vlogic_var_assoc :: Maybe (Logic_var) } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Storage = NoStorage | Static | Register | Extern deriving (Show, Read, Eq) {-! derive : Parse !-} +data Exp = Exp { eid :: Int, enode :: Exp_node } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Exp_node = Const (Constant) | Lval (Lval) | SizeOf (Typ) | SizeOfE (Exp) | SizeOfStr (String) | AlignOf (Typ) | AlignOfE (Exp) | UnOp (Unop) (Exp) (Typ) | BinOp (Binop) (Exp) (Exp) (Typ) | CastE (Typ) (Exp) | AddrOf (Lval) | StartOf (Lval) | Info (Exp) (Exp_info) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Exp_info = Exp_info { exp_loc :: Location, exp_type :: Logic_type, exp_name :: [String] } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Constant = CInt64 (Int64) (Ikind) (Maybe (String)) | CStr (String) | CWStr ([Int64]) | CChr (Char) | CReal (Float) (Fkind) (Maybe (String)) | CEnum (Enumitem) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Unop = Neg | BNot | LNot deriving (Show, Read, Eq) {-! derive : Parse !-} +data Binop = PlusA | PlusPI | IndexPI | MinusA | MinusPI | MinusPP | Mult | Div | Mod | Shiftlt | Shiftrt | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr deriving (Show, Read, Eq) {-! derive : Parse !-} +type Lval = (Lhost, Offset) +data Lhost = Var (Varinfo) | Mem (Exp) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Offset = NoOffset | Field (Fieldinfo) (Offset) | Index (Exp) (Offset) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Init = SingleInit (Exp) | CompoundInit (Typ) ([(Offset, Init)]) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Initinfo = Initinfo { init :: Maybe (Init) } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Fundec = Fundec { svar :: Varinfo, sformals :: [Varinfo], slocals :: [Varinfo], smaxid :: Int, sbody :: Block, smaxstmtid :: Maybe (Int), sallstmts :: [Stmt], sspec :: Funspec } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Block = Block { battrs :: Attributes, blocals :: [Varinfo], bstmts :: [Stmt] } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Stmt = Stmt { labels :: [Label], skind :: Stmtkind, sid :: Int, succs :: [Stmt], preds :: [Stmt], ghost :: Bool } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Label = Label (String) (Location) (Bool) | Case (Exp) (Location) | Default (Location) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Stmtkind = Instr (Instr) | Return (Maybe (Exp)) (Location) | Goto (Stmt) (Location) | Break (Location) | Continue (Location) | If (Exp) (Block) (Block) (Location) | Switch (Exp) (Block) ([Stmt]) (Location) | Loop ([Code_annotation]) (Block) (Location) (Maybe (Stmt)) (Maybe (Stmt)) | Block' (Block) | UnspecifiedSequence ([(Stmt, [Lval], [Lval], [Lval])]) | TryFinally (Block) (Block) (Location) | TryExcept (Block) (([Instr], Exp)) (Block) (Location) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Instr = Set (Lval) (Exp) (Location) | Call (Maybe (Lval)) (Exp) ([Exp]) (Location) | Asm (Attributes) ([String]) ([(Maybe (String), String, Lval)]) ([(Maybe (String), String, Exp)]) ([String]) (Location) | Skip (Location) | Code_annot (Code_annotation) (Location) deriving (Show, Read, Eq) {-! derive : Parse !-} +type Location = (Position, Position) +data Typsig = TSArray (Typsig) (Maybe (Int64)) ([Attribute]) | TSPtr (Typsig) ([Attribute]) | TSComp (Bool) (String) ([Attribute]) | TSFun (Typsig) ([Typsig]) (Bool) ([Attribute]) | TSEnum (String) ([Attribute]) | TSBase (Typ) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Logic_type = Ctype (Typ) | Ltype (Logic_type_info) ([Logic_type]) | Lvar (String) | Linteger | Lreal | Larrow ([Logic_type]) (Logic_type) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Identified_term = Identified_term { it_id :: Int, it_content :: Term } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Logic_label = StmtLabel (Stmt) | LogicLabel (String) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Term = Term { term_node :: Term_node, term_loc :: (Position, Position), term_type :: Logic_type, term_name :: [String] } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Term_node = TConst (Constant) | TLval (Term_lval) | TSizeOf (Typ) | TSizeOfE (Term) | TSizeOfStr (String) | TAlignOf (Typ) | TAlignOfE (Term) | TUnOp (Unop) (Term) | TBinOp (Binop) (Term) (Term) | TCastE (Typ) (Term) | TAddrOf (Term_lval) | TStartOf (Term_lval) | Tapp (Logic_info) ([(Logic_label, Logic_label)]) ([Term]) | Tlambda (Quantifiers) (Term) | TDataCons (Logic_ctor_info) ([Term]) | Tif (Term) (Term) (Term) | Told (Term) | Tat (Term) (Logic_label) | Tbase_addr (Term) | Tblock_length (Term) | Tnull | TCoerce (Term) (Typ) | TCoerceE (Term) (Term) | TUpdate (Term) (Fieldinfo) (Term) | Ttypeof (Term) | Ttype (Typ) | Tempty_set | Tunion ([Term]) | Tinter ([Term]) | Tcomprehension (Term) (Quantifiers) (Maybe (Named (Predicate))) | Trange (Maybe (Term)) (Maybe (Term)) | Tlet (Logic_info) (Term) deriving (Show, Read, Eq) {-! derive : Parse !-} +type Term_lval = (Term_lhost, Term_offset) +data Term_lhost = TVar (Logic_var) | TResult (Typ) | TMem (Term) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Term_offset = TNoOffset | TField (Fieldinfo) (Term_offset) | TIndex (Term) (Term_offset) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Logic_info = Logic_info { l_var_info :: Logic_var, l_labels :: [Logic_label], l_tparams :: [String], l_type :: Maybe (Logic_type), l_profile :: [Logic_var], l_body :: Logic_body } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Builtin_logic_info = Builtin_logic_info { bl_name :: String, bl_labels :: [Logic_label], bl_params :: [String], bl_type :: Maybe (Logic_type), bl_profile :: [(String, Logic_type)] } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Logic_body = LBnone | LBreads ([Identified_term]) | LBterm (Term) | LBpred (Named (Predicate)) | LBinductive ([(String, [Logic_label], [String], Named (Predicate))]) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Logic_type_info = Logic_type_info { lt_name :: String, lt_params :: [String], lt_def :: Maybe (Logic_type_def) } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Logic_type_def = LTsum ([Logic_ctor_info]) | LTsyn (Logic_type) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Logic_var = Logic_var { lv_name :: String, lv_id :: Int, lv_type :: Logic_type, lv_origin :: Maybe (Varinfo) } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Logic_ctor_info = Logic_ctor_info { ctor_name :: String, ctor_type :: Logic_type_info, ctor_params :: [Logic_type] } deriving (Show, Read, Eq) {-! derive : Parse !-} +type Quantifiers = [Logic_var] +data Relation = Rlt | Rgt | Rle | Rge | Req | Rneq deriving (Show, Read, Eq) {-! derive : Parse !-} +data Predicate = Pfalse | Ptrue | Papp (Logic_info) ([(Logic_label, Logic_label)]) ([Term]) | Pseparated ([Term]) | Prel (Relation) (Term) (Term) | Pand (Named (Predicate)) (Named (Predicate)) | Por (Named (Predicate)) (Named (Predicate)) | Pxor (Named (Predicate)) (Named (Predicate)) | Pimplies (Named (Predicate)) (Named (Predicate)) | Piff (Named (Predicate)) (Named (Predicate)) | Pnot (Named (Predicate)) | Pif (Term) (Named (Predicate)) (Named (Predicate)) | Plet (Logic_info) (Named (Predicate)) | Pforall (Quantifiers) (Named (Predicate)) | Pexists (Quantifiers) (Named (Predicate)) | Pold (Named (Predicate)) | Pat (Named (Predicate)) (Logic_label) | Pvalid (Term) | Pvalid_index (Term) (Term) | Pvalid_range (Term) (Term) (Term) | Pfresh (Term) | Psubtype (Term) (Term) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Identified_predicate = Identified_predicate { ip_name :: [String], ip_loc :: Location, ip_id :: Int, ip_content :: Predicate } deriving (Show, Read, Eq) {-! derive : Parse !-} +type Variant term = (term, Maybe (String)) +data Zone locs = Location (locs) | Nothing' deriving (Show, Read, Eq) {-! derive : Parse !-} +type Assigns locs = (Zone (locs), [Zone (locs)]) +data Named a = Named { name :: [String], loc :: Location, content :: a } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Spec term pred locs = Spec { spec_requires :: [pred], spec_behavior :: [Behavior (pred) (locs)], spec_variant :: Maybe (Variant (term)), spec_terminates :: Maybe (pred), spec_complete_behaviors :: [[String]], spec_disjoint_behaviors :: [[String]] } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Behavior pred locs = Behavior { b_name :: String, b_assumes :: [pred], b_post_cond :: [(Termination_kind, pred)], b_assigns :: [Assigns (locs)] } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Loop_pragma term = Unroll_level (term) | Widen_hints ([term]) | Widen_variables ([term]) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Slice_pragma term = SPexpr (term) | SPctrl | SPstmt deriving (Show, Read, Eq) {-! derive : Parse !-} +data Impact_pragma term = IPexpr (term) | IPstmt deriving (Show, Read, Eq) {-! derive : Parse !-} +data Pragma term = Loop_pragma (Loop_pragma (term)) | Slice_pragma (Slice_pragma (term)) | Impact_pragma (Impact_pragma (term)) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Validity = True' | False' | Maybe deriving (Show, Read, Eq) {-! derive : Parse !-} +data Annot_checked_status = Annot_checked_status { emitter :: String, valid :: Validity } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Annotation_status = Unknown | Checked (Annot_checked_status) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Annot_status = Annot_status { status :: Annotation_status } deriving (Show, Read, Eq) {-! derive : Parse !-} +data Code_annot term pred spec_pred locs = AAssert ([String]) (pred) (Annot_status) | AStmtSpec (Spec (term) (spec_pred) (locs)) | AInvariant ([String]) (Bool) (pred) | AVariant (Variant (term)) | AAssigns ([String]) (Assigns (locs)) | APragma (Pragma (term)) deriving (Show, Read, Eq) {-! derive : Parse !-} +type Funspec = Spec (Term) (Identified_predicate) (Identified_term) +data Code_annotation = Code_annotation { annot_content :: Code_annot (Term) (Named (Predicate)) (Identified_predicate) (Identified_term), annot_id :: Int } deriving (Show, Read, Eq) {-! derive : Parse !-} +type Funbehavior = Behavior (Identified_predicate) (Identified_term) +data Global_annotation = Dfun_or_pred (Logic_info) | Daxiomatic (String) ([Global_annotation]) | Dtype (Logic_type_info) | Dlemma (String) (Bool) ([Logic_label]) ([String]) (Named (Predicate)) | Dinvariant (Logic_info) | Dtype_annot (Logic_info) deriving (Show, Read, Eq) {-! derive : Parse !-} +data Kinstr = Kstmt (Stmt) | Kglobal deriving (Show, Read, Eq) {-! derive : Parse !-} +data Mach = Mach { version_major :: Int, version_minor :: Int, version :: String, underscore_name :: Bool, sizeof_short :: Int, sizeof_int :: Int, sizeof_long :: Int, sizeof_longlong :: Int, sizeof_ptr :: Int, sizeof_enum :: Int, sizeof_float :: Int, sizeof_double :: Int, sizeof_longdouble :: Int, sizeof_void :: Int, sizeof_fun :: Int, size_t :: String, wchar_t :: String, ptrdiff_t :: String, enum_are_signed :: Bool, alignof_short :: Int, alignof_int :: Int, alignof_long :: Int, alignof_longlong :: Int, alignof_ptr :: Int, alignof_enum :: Int, alignof_float :: Int, alignof_double :: Int, alignof_longdouble :: Int, alignof_str :: Int, alignof_fun :: Int, alignof_char_array :: Int, char_is_unsigned :: Bool, const_string_literals :: Bool, little_endian :: Bool } deriving (Show, Read, Eq) {-! derive : Parse !-} + diff --git a/Makefile b/Makefile new file mode 100644 --- /dev/null +++ b/Makefile @@ -0,0 +1,24 @@ +.PHONY: all +all: Language/CIL.hs + +CIL.hs: GenCIL.hs + runhaskell -W GenCIL.hs + +Language/CIL.hs: CIL.hs + mkdir -p Language && cp CIL.hs Language/CIL.hs + +#DrIFT-cabalized -o Language/CIL.hs CIL.hs + +.PHONY: test +test: Test.hs Language/CIL.hs + runhaskell -W Test.hs + +.PHONY: clean +clean: + -rm *.o *.hi + -rm Language/*.o Language/*.hi + -rm cil_types_nocomments.mli + -rm CIL.hs + -rm -r Language + -rm -rf install-dumpcil-plugin + diff --git a/cil.cabal b/cil.cabal --- a/cil.cabal +++ b/cil.cabal @@ -1,5 +1,5 @@ name: cil -version: 0.0.0 +version: 0.0.1 category: Language @@ -20,8 +20,9 @@ cabal-version: >= 1.6 extra-source-files: - dumpcil/dump_cil.ml - dumpcil/Makefile + Makefile + cil_types.mli + GenCIL.hs library build-depends: diff --git a/cil_types.mli b/cil_types.mli new file mode 100644 --- /dev/null +++ b/cil_types.mli @@ -0,0 +1,1527 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2001-2003 *) +(* George C. Necula *) +(* Scott McPeak *) +(* Wes Weimer *) +(* Ben Liblit *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* *) +(* 3. The names of the contributors may not be used to endorse or *) +(* promote products derived from this software without specific prior *) +(* written permission. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *) +(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *) +(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *) +(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *) +(* COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *) +(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *) +(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; *) +(* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER *) +(* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT *) +(* LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN *) +(* ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE *) +(* POSSIBILITY OF SUCH DAMAGE. *) +(* *) +(* File modified by CEA (Commissariat a l'energie atomique et aux *) +(* energies alternatives). *) +(**************************************************************************) + +(** The Abstract Syntax of CIL. + @plugin development guide *) + +(**************************** WARNING ***************************************) +(* Remember to reflect any change here into the visitor and pretty-printer *) +(* in cil.ml. In particular, if a type becomes mutable, it is necessary to *) +(* adapt the Cil.behavior type and the copy_behavior accordingly. *) +(* A first test to see if something has been broken by a change is to launch*) +(* ptests.byte -add-options '-files-debug "-check -copy"' *) +(* In addition, it is a good idea to add some invariant checks in the *) +(* check_file class in frama-c/src/file.ml (before lauching the tests) *) +(****************************************************************************) + +(** This is used to cache the computation of the size of types in bits. *) +type bitsSizeofTyp = Not_Computed | Not_Computable of exn | Computed of int +type bitsSizeofTypCache = { mutable scache : bitsSizeofTyp} + +(** kind of termination a post-condition applies to. See ACSL manual. *) +type termination_kind = Normal | Exits | Breaks | Continues | Returns + +(** The top-level representation of a CIL source file (and the result of the + * parsing and elaboration). Its main contents is the list of global + * declarations and definitions. You can iterate over the globals in a + * {!Cil_types.file} using the following iterators: {!Cil.mapGlobals}, + * {!Cil.iterGlobals} and {!Cil.foldGlobals}. You can also use the + * {!Cil.dummyFile} when you need a {!Cil_types.file} as a placeholder. For each + * global item CIL stores the source location where it appears (using the + * type {!Cil_types.location}) *) +type file = + { mutable fileName: string; (** The complete file name *) + mutable globals: global list; (** List of globals as they will appear + in the printed file *) + mutable globinit: fundec option; + (** An optional global initializer function. This is a function where + * you can put stuff that must be executed before the program is + * started. This function, is conceptually at the end of the file, + * although it is not part of the globals list. Use {!Cil.getGlobInit} + * to create/get one. *) + mutable globinitcalled: bool; + (** Whether the global initialization function is called in main. This + should always be false if there is no global initializer. When + you create a global initialization CIL will try to insert code in + main to call it. *) + } +(** Top-level representation of a C source file. + @plugin development guide *) + +(** The main type for representing global declarations and definitions. A list + of these form a CIL file. The order of globals in the file is generally + important. + @plugin development guide *) +and global = + | GType of typeinfo * location + (** A typedef. All uses of type names (through the [TNamed] constructor) + must be preceeded in the file by a definition of the name. The string + is the defined name and always not-empty. *) + + | GCompTag of compinfo * location + (** Defines a struct/union tag with some fields. There must be one of + these for each struct/union tag that you use (through the [TComp] + constructor) since this is the only context in which the fields are + printed. Consequently nested structure tag definitions must be + broken into individual definitions with the innermost structure + defined first. *) + + | GCompTagDecl of compinfo * location + (** Declares a struct/union tag. Use as a forward declaration. This is + * printed without the fields. *) + + | GEnumTag of enuminfo * location + (** Declares an enumeration tag with some fields. There must be one of + these for each enumeration tag that you use (through the [TEnum] + constructor) since this is the only context in which the items are + printed. *) + + | GEnumTagDecl of enuminfo * location + (** Declares an enumeration tag. Use as a forward declaration. This is + * printed without the items. *) + + | GVarDecl of funspec * varinfo * location + (** A variable declaration (not a definition). If the variable has a + function type then this is a prototype. There can be several + declarations and at most one definition for a given variable. If both + forms appear then they must share the same varinfo structure. A + prototype shares the varinfo with the fundec of the definition. Either + has storage Extern or there must be a definition in this file *) + + | GVar of varinfo * initinfo * location + (** A variable definition. Can have an initializer. The initializer is + * updateable so that you can change it without requiring to recreate + * the list of globals. There can be at most one definition for a + * variable in an entire program. Cannot have storage Extern or function + * type. *) + + + | GFun of fundec * location + (** A function definition. *) + + | GAsm of string * location (** Global asm statement. These ones + can contain only a template *) + | GPragma of attribute * location (** Pragmas at top level. Use the same + syntax as attributes *) + | GText of string (** Some text (printed verbatim) at + top level. E.g., this way you can + put comments in the output. *) + | GAnnot of global_annotation * location + (** a global annotation. Can be + - an axiom or a lemma + - a predicate declaration or definition + - a global type invariant + - a global invariant + - a logic function declaration or definition. + *) + +(** {b Types}. A C type is represented in CIL using the type {!Cil_types.typ}. + * Among types we differentiate the integral types (with different kinds + * denoting the sign and precision), floating point types, enumeration types, + * array and pointer types, and function types. Every type is associated with + * a list of attributes, which are always kept in sorted order. Use + * {!Cil.addAttribute} and {!Cil.addAttributes} to construct list of + * attributes. If you want to inspect a type, you should use + * {!Cil.unrollType} or {!Cil.unrollTypeDeep} to see through the uses of + * named types. *) +(** CIL is configured at build-time with the sizes and alignments of the + * underlying compiler (GCC or MSVC). CIL contains functions that can compute + * the size of a type (in bits) {!Cil.bitsSizeOf}, the alignment of a type + * (in bytes) {!Cil.alignOf_int}, and can convert an offset into a start and + * width (both in bits) using the function {!Cil.bitsOffset}. At the moment + * these functions do not take into account the [packed] attributes and + * pragmas. *) + +and typ = + TVoid of attributes (** Void type. Also predefined as {!Cil.voidType} *) + | TInt of ikind * attributes + (** An integer type. The kind specifies the sign and width. Several + * useful variants are predefined as {!Cil.intType}, {!Cil.uintType}, + * {!Cil.longType}, {!Cil.charType}. *) + + | TFloat of fkind * attributes + (** A floating-point type. The kind specifies the precision. You can + * also use the predefined constant {!Cil.doubleType}. *) + + | TPtr of typ * attributes + (** Pointer type. Several useful variants are predefined as + * {!Cil.charPtrType}, {!Cil.charConstPtrType} (pointer to a + * constant character), {!Cil.voidPtrType}, + * {!Cil.intPtrType} *) + + | TArray of typ * exp option * bitsSizeofTypCache * attributes + (** Array type. It indicates the base type and the array length. *) + + | TFun of typ * (string * typ * attributes) list option * bool * attributes + (** Function type. Indicates the type of the result, the name, type + * and name attributes of the formal arguments ([None] if no + * arguments were specified, as in a function whose definition or + * prototype we have not seen; [Some \[\]] means void). Use + * {!Cil.argsToList} to obtain a list of arguments. The boolean + * indicates if it is a variable-argument function. If this is the + * type of a varinfo for which we have a function declaration then + * the information for the formals must match that in the + * function's sformals. Use {!Cil.setFormals}, or + * {!Cil.setFunctionType}, or {!Cil.makeFormalVar} for this + * purpose. *) + + | TNamed of typeinfo * attributes + (** The use of a named type. All uses of the same type name must + * share the typeinfo. Each such type name must be preceeded + * in the file by a [GType] global. This is printed as just the + * type name. The actual referred type is not printed here and is + * carried only to simplify processing. To see through a sequence + * of named type references, use {!Cil.unrollType}. The attributes + * are in addition to those given when the type name was defined. *) + + | TComp of compinfo * bitsSizeofTypCache * attributes + (** A reference to a struct or a union type. All references to the + same struct or union must share the same compinfo among them and + with a [GCompTag] global that preceeds all uses (except maybe + those that are pointers to the composite type). The attributes + given are those pertaining to this use of the type and are in + addition to the attributes that were given at the definition of + the type and which are stored in the compinfo. *) + + | TEnum of enuminfo * attributes + (** A reference to an enumeration type. All such references must + share the enuminfo among them and with a [GEnumTag] global that + preceeds all uses. The attributes refer to this use of the + enumeration and are in addition to the attributes of the + enumeration itself, which are stored inside the enuminfo *) + + | TBuiltin_va_list of attributes + (** This is the same as the gcc's type with the same name *) + +(** Various kinds of integers *) +and ikind = + IBool (** [_Bool] *) + | IChar (** [char] *) + | ISChar (** [signed char] *) + | IUChar (** [unsigned char] *) + | IInt (** [int] *) + | IUInt (** [unsigned int] *) + | IShort (** [short] *) + | IUShort (** [unsigned short] *) + | ILong (** [long] *) + | IULong (** [unsigned long] *) + | ILongLong (** [long long] (or [_int64] on Microsoft Visual C) *) + | IULongLong (** [unsigned long long] (or [unsigned _int64] on Microsoft + Visual C) *) + +(** Various kinds of floating-point numbers*) +and fkind = + FFloat (** [float] *) + | FDouble (** [double] *) + | FLongDouble (** [long double] *) + +(** {b Attributes.} *) + +and attribute = + | Attr of string * attrparam list +(** An attribute has a name and some optional parameters. The name should not + * start or end with underscore. When CIL parses attribute names it will + * strip leading and ending underscores (to ensure that the multitude of GCC + * attributes such as const, __const and __const__ all mean the same thing.) *) + | AttrAnnot of string + +(** Attributes are lists sorted by the attribute name. Use the functions + * {!Cil.addAttribute} and {!Cil.addAttributes} to insert attributes in an + * attribute list and maintain the sortedness. *) +and attributes = attribute list + +(** The type of parameters of attributes *) +and attrparam = + | AInt of int (** An integer constant *) + | AStr of string (** A string constant *) + | ACons of string * attrparam list (** Constructed attributes. These + are printed [foo(a1,a2,...,an)]. + The list of parameters can be + empty and in that case the + parentheses are not printed. *) + | ASizeOf of typ (** A way to talk about types *) + | ASizeOfE of attrparam + | ASizeOfS of typsig (** Replacement for ASizeOf in type + signatures. Only used for + attributes inside typsigs.*) + | AAlignOf of typ + | AAlignOfE of attrparam + | AAlignOfS of typsig + | AUnOp of unop * attrparam + | ABinOp of binop * attrparam * attrparam + | ADot of attrparam * string (** a.foo **) + | AStar of attrparam (** * a *) + | AAddrOf of attrparam (** & a **) + | AIndex of attrparam * attrparam (** a1[a2] *) + | AQuestion of attrparam * attrparam * attrparam (** a1 ? a2 : a3 **) + + +(** {b Structures.} The {!Cil_types.compinfo} describes the definition of a + * structure or union type. Each such {!Cil_types.compinfo} must be defined at the + * top-level using the [GCompTag] constructor and must be shared by all + * references to this type (using either the [TComp] type constructor or from + * the definition of the fields. + + If all you need is to scan the definition of each + * composite type once, you can do that by scanning all top-level [GCompTag]. + + * Constructing a {!Cil_types.compinfo} can be tricky since it must contain fields + * that might refer to the host {!Cil_types.compinfo} and furthermore the type of + * the field might need to refer to the {!Cil_types.compinfo} for recursive types. + * Use the {!Cil.mkCompInfo} function to create a {!Cil_types.compinfo}. You can + * easily fetch the {!Cil_types.fieldinfo} for a given field in a structure with + * {!Cil.getCompField}. *) + +(** The definition of a structure or union type. Use {!Cil.mkCompInfo} to + * make one and use {!Cil.copyCompInfo} to copy one (this ensures that a new + * key is assigned and that the fields have the right pointers to parents.). + @plugin development guide *) +and compinfo = { + mutable cstruct: bool; + (** True if struct, False if union *) + mutable cname: string; + (** The name. Always non-empty. Use {!Cil.compFullName} to get the full + * name of a comp (along with the struct or union) *) + mutable ckey: int; + (** A unique integer. This is assigned by {!Cil.mkCompInfo} using a + * global variable in the Cil module. Thus two identical structs in two + * different files might have different keys. Use {!Cil.copyCompInfo} to + * copy structures so that a new key is assigned. *) + mutable cfields: fieldinfo list; + (** Information about the fields. Notice that each fieldinfo has a + * pointer back to the host compinfo. This means that you should not + * share fieldinfo's between two compinfo's *) + mutable cattr: attributes; + (** The attributes that are defined at the same time as the composite + * type. These attributes can be supplemented individually at each + * reference to this [compinfo] using the [TComp] type constructor. *) + mutable cdefined: bool; + (** This boolean flag can be used to distinguish between structures + that have not been defined and those that have been defined but have + no fields (such things are allowed in gcc). *) + mutable creferenced: bool; + (** True if used. Initially set to false. *) + } + +(** {b Structure fields.} The {!Cil_types.fieldinfo} structure is used to describe + * a structure or union field. Fields, just like variables, can have + * attributes associated with the field itself or associated with the type of + * the field (stored along with the type of the field). *) + +(** Information about a struct/union field. + @plugin development guide *) +and fieldinfo = { + mutable fcomp: compinfo; + (** The host structure that contains this field. There can be only one + * [compinfo] that contains the field. *) + mutable fname: string; + (** The name of the field. Might be the value of {!Cil.missingFieldName} + * in which case it must be a bitfield and is not printed and it does not + * participate in initialization *) + mutable ftype: typ; + (** The type *) + mutable fbitfield: int option; + (** If a bitfield then ftype should be an integer type and the width of + * the bitfield must be 0 or a positive integer smaller or equal to the + * width of the integer type. A field of width 0 is used in C to control + * the alignment of fields. *) + mutable fattr: attributes; + (** The attributes for this field (not for its type) *) + mutable floc: location; + (** The location where this field is defined *) + mutable faddrof: bool; + (** Adapted from CIL [vaddrof] field for variables. Only set for + * non-array fields. Variable whose field address is taken is not marked + * anymore as having its own address taken. + * True if the address of this field is taken. CIL will set these + * flags when it parses C, but you should make sure to set the flag + * whenever your transformation create [AddrOf] expression. *) + mutable fsize_in_bits: int option; + (** Similar to [fbitfield] for all types of fields. Useful when + * the type of the field is changed in the analyzer, to recall the size + * of the original field. + @deprecated only Jessie uses this + *) + mutable foffset_in_bits: int option; + (** Store the offset at which the field starts in the structure. + @deprecated only Jessie uses this *) + mutable fpadding_in_bits: int option; + (** Store the size of the padding that follows the field, if any. + @deprecated only Jessie uses this *) +} + + + +(** {b Enumerations.} Information about an enumeration. This is shared by all + * references to an enumeration. Make sure you have a [GEnumTag] for each + * of these. *) + +(** Information about an enumeration. + @plugin development guide *) +and enuminfo = { + mutable ename: string; + (** The name. Always non-empty. *) + mutable eitems: enumitem list; + (** Items. The list must be non-empty *) + mutable eattr: attributes; + (** The attributes that are defined at the same time as the enumeration + * type. These attributes can be supplemented individually at each + * reference to this [enuminfo] using the [TEnum] type constructor. *) + mutable ereferenced: bool; + (** True if used. Initially set to false*) +} + +and enumitem = + { mutable einame: string; (** the name, always non-empty. *) + mutable eival: exp; (** value of the item. + Must be a compile-time constant *) + mutable eihost: enuminfo; (** the host enumeration in which the + item is declared. *) + eiloc: location; + } + +(** Information about a defined type. + @plugin development guide *) +and typeinfo = { + mutable tname: string; + (** The name. Can be empty only in a [GType] when introducing a composite + * or enumeration tag. If empty cannot be refered to from the file *) + mutable ttype: typ; + (** The actual type. This includes the attributes that were present in + * the typedef *) + mutable treferenced: bool; + (** True if used. Initially set to false*) +} + +(** {b Variables.} + Each local or global variable is represented by a unique {!Cil_types.varinfo} +structure. A global {!Cil_types.varinfo} can be introduced with the [GVarDecl] or +[GVar] or [GFun] globals. A local varinfo can be introduced as part of a +function definition {!Cil_types.fundec}. + + All references to a given global or local variable must refer to the same +copy of the [varinfo]. Each [varinfo] has a globally unique identifier that +can be used to index maps and hashtables (the name can also be used for this +purpose, except for locals from different functions). This identifier is +constructor using a global counter. + + It is very important that you construct [varinfo] structures using only one + of the following functions: +- {!Cil.makeGlobalVar} : to make a global variable +- {!Cil.makeTempVar} : to make a temporary local variable whose name +will be generated so that to avoid conflict with other locals. +- {!Cil.makeLocalVar} : like {!Cil.makeTempVar} but you can specify the +exact name to be used. +- {!Cil.copyVarinfo}: make a shallow copy of a varinfo assigning a new name +and a new unique identifier + + A [varinfo] is also used in a function type to denote the list of formals. + +*) + +(** Information about a variable. + @plugin development guide *) +and varinfo = { + mutable vname: string; + (** The name of the variable. Cannot be empty. It is primarily your + * responsibility to ensure the uniqueness of a variable name. For local + * variables {!Cil.makeTempVar} helps you ensure that the name is unique. + *) + + vorig_name: string; + (** the original name of the variable. Need not be unique. *) + + mutable vtype: typ; + (** The declared type of the variable. *) + + mutable vattr: attributes; + (** A list of attributes associated with the variable.*) + mutable vstorage: storage; + (** The storage-class *) + + mutable vglob: bool; + (** True if this is a global variable*) + + mutable vdefined: bool; + (** True if the variable or function is defined in the file. + * Only relevant for functions and global variables. + * Not used in particular for local variables and logic variables. *) + + mutable vformal: bool; + (** True if the variable is a formal parameter of a function. *) + + mutable vinline: bool; + (** Whether this varinfo is for an inline function. *) + + mutable vdecl: location; + (** Location of variable declaration. *) + + mutable vid: int; + (** A unique integer identifier. This field will be + * set for you if you use one of the {!Cil.makeFormalVar}, + * {!Cil.makeLocalVar}, {!Cil.makeTempVar}, {!Cil.makeGlobalVar}, or + * {!Cil.copyVarinfo}. *) + + mutable vaddrof: bool; + (** True if the address of this variable is taken. CIL will set these + * flags when it parses C, but you should make sure to set the flag + * whenever your transformation create [AddrOf] expression. *) + + mutable vreferenced: bool; + (** True if this variable is ever referenced. This is computed by + * [removeUnusedVars]. It is safe to just initialize this to False *) + + vgenerated: bool; + (** true for temporary variables generated by CIL normalization. + false for variables coming directly from user input. + *) + + mutable vdescr: string option; (** For most temporary variables, a + description of what the var holds. + (e.g. for temporaries used for + function call results, this string + is a representation of the function + call.) *) + + mutable vdescrpure: bool; (** Indicates whether the vdescr above + is a pure expression or call. + True for all CIL expressions and + Lvals, but false for e.g. function + calls. + Printing a non-pure vdescr more + than once may yield incorrect + results. *) + + mutable vghost: bool; (** Indicates if the variable is declared in ghost code *) + + vlogic: bool; + (** False if this variable is a C variable. *) + + mutable vlogic_var_assoc: logic_var option + (** logic variable representing this variable in the logic world*) +} + +(** Storage-class information *) +and storage = + NoStorage (** The default storage. Nothing is printed *) + | Static + | Register + | Extern + + +(** {b Expressions.} The CIL expression language contains only the side-effect free expressions of +C. They are represented as the type {!Cil_types.exp}. There are several +interesting aspects of CIL expressions: + + Integer and floating point constants can carry their textual representation. +This way the integer 15 can be printed as 0xF if that is how it occurred in the +source. + + CIL uses 64 bits to represent the integer constants and also stores the width +of the integer type. Care must be taken to ensure that the constant is +representable with the given width. Use the functions {!Cil.kinteger}, +{!Cil.kinteger64} and {!Cil.integer} to construct constant +expressions. CIL predefines the constants {!Cil.zero}, +{!Cil.one} and {!Cil.mone} (for -1). + + Use the functions {!Cil.isConstant} and {!Cil.isInteger} to test if +an expression is a constant and a constant integer respectively. + + CIL keeps the type of all unary and binary expressions. You can think of that +type qualifying the operator. Furthermore there are different operators for +arithmetic and comparisons on arithmetic types and on pointers. + + Another unusual aspect of CIL is that the implicit conversion between an +expression of array type and one of pointer type is made explicit, using the +[StartOf] expression constructor (which is not printed). If you apply the +[AddrOf}]constructor to an lvalue of type [T] then you will be getting an +expression of type [TPtr(T)]. + + You can find the type of an expression with {!Cil.typeOf}. + + You can perform constant folding on expressions using the function +{!Cil.constFold}. +*) + +(** Expressions (Side-effect free)*) +and exp = { eid: int; (** unique identifier *) + enode: exp_node; (** the expression itself *) + } + +and exp_node = + Const of constant (** Constant *) + | Lval of lval (** Lvalue *) + | SizeOf of typ + (** sizeof(). Has [unsigned int] type (ISO 6.5.3.4). This is not + * turned into a constant because some transformations might want to + * change types *) + + | SizeOfE of exp + (** sizeof() *) + + | SizeOfStr of string + (** sizeof(string_literal). We separate this case out because this is the + * only instance in which a string literal should not be treated as + * having type pointer to character. *) + + | AlignOf of typ + (** This corresponds to the GCC __alignof_. Has [unsigned int] type *) + | AlignOfE of exp + + + | UnOp of unop * exp * typ + (** Unary operation. Includes the type of the result. *) + + | BinOp of binop * exp * exp * typ + (** Binary operation. Includes the type of the result. The arithmetic + * conversions are made explicit for the arguments. *) + + | CastE of typ * exp + (** Use {!Cil.mkCast} to make casts. *) + + | AddrOf of lval + (** Always use {!Cil.mkAddrOf} to construct one of these. Apply to an + * lvalue of type [T] yields an expression of type [TPtr(T)] *) + + | StartOf of lval + (** Conversion from an array to a pointer to the beginning of the array. + * Given an lval of type [TArray(T)] produces an expression of type + * [TPtr(T)]. In C this operation is implicit, the [StartOf] operator is + * not printed. We have it in CIL because it makes the typing rules + * simpler. *) + + | Info of exp * exp_info + (** Additional information on the underlying expression *) + +(** Additional information on an expression *) +and exp_info = { + exp_loc : location; + exp_type : logic_type; (** when used as placeholder for a term *) + exp_name: string list; +} + +(** {b Constants.} *) + +(** Literal constants *) +and constant = + | CInt64 of int64 * ikind * string option + (** Integer constant. Give the ikind (see ISO9899 6.1.3.2) and the + * textual representation, if available. (This allows us to print a + * constant as, for example, 0xF instead of 15.) Use {!Cil.integer} or + * {!Cil.kinteger} to create these. Watch out for integers that cannot be + * represented on 64 bits. OCAML does not give Overflow exceptions. *) + | CStr of string + (** String constant. The escape characters inside the string have been + * already interpreted. This constant has pointer to character type! The + * only case when you would like a string literal to have an array type + * is when it is an argument to sizeof. In that case you should use + * SizeOfStr. *) + | CWStr of int64 list + (** Wide character string constant. Note that the local interpretation + * of such a literal depends on {!Cil.theMachine.wcharType} and {!Cil.theMachine.wcharKind}. + * Such a constant has type pointer to {!Cil.theMachine.wcharType}. The + * escape characters in the string have not been "interpreted" in + * the sense that L"A\xabcd" remains "A\xabcd" rather than being + * represented as the wide character list with two elements: 65 and + * 43981. That "interpretation" depends on the underlying wide + * character type. *) + | CChr of char + (** Character constant. This has type int, so use charConstToInt + * to read the value in case sign-extension is needed. *) + | CReal of float * fkind * string option + (** Floating point constant. Give the fkind (see ISO 6.4.4.2) and also + * the textual representation, if available. *) + | CEnum of enumitem + (** An enumeration constant + * Use [Cillower.lowerEnumVisitor] to replace these with integer + * constants. *) + +(** Unary operators *) +and unop = + Neg (** Unary minus *) + | BNot (** Bitwise complement (~) *) + | LNot (** Logical Not (!) *) + +(** Binary operations *) +and binop = + PlusA (** arithmetic + *) + | PlusPI (** pointer + integer *) + | IndexPI (** pointer + integer but only when + * it arises from an expression + * [e\[i\]] when [e] is a pointer and + * not an array. This is semantically + * the same as PlusPI but CCured uses + * this as a hint that the integer is + * probably positive. *) + | MinusA (** arithmetic - *) + | MinusPI (** pointer - integer *) + | MinusPP (** pointer - pointer *) + | Mult (** * *) + | Div (** / *) + | Mod (** % *) + | Shiftlt (** shift left *) + | Shiftrt (** shift right *) + + | Lt (** < (arithmetic comparison) *) + | Gt (** > (arithmetic comparison) *) + | Le (** <= (arithmetic comparison) *) + | Ge (** >= (arithmetic comparison) *) + | Eq (** == (arithmetic comparison) *) + | Ne (** != (arithmetic comparison) *) + | BAnd (** bitwise and *) + | BXor (** exclusive-or *) + | BOr (** inclusive-or *) + + | LAnd (** logical and. Unlike other + * expressions this one does not + * always evaluate both operands. If + * you want to use these, you must + * set {!Cil.useLogicalOperators}. *) + | LOr (** logical or. Unlike other + * expressions this one does not + * always evaluate both operands. If + * you want to use these, you must + * set {!Cil.useLogicalOperators}. *) + +(** {b Lvalues.} Lvalues are the sublanguage of expressions that can appear at the left of an assignment or as operand to the address-of operator. +In C the syntax for lvalues is not always a good indication of the meaning +of the lvalue. For example the C value +{v +a[0][1][2] + v} + might involve 1, 2 or 3 memory reads when used in an expression context, +depending on the declared type of the variable [a]. If [a] has type [int +\[4\]\[4\]\[4\]] then we have one memory read from somewhere inside the area +that stores the array [a]. On the other hand if [a] has type [int ***] then +the expression really means [* ( * ( * (a + 0) + 1) + 2)], in which case it is +clear that it involves three separate memory operations. + +An lvalue denotes the contents of a range of memory addresses. This range +is denoted as a host object along with an offset within the object. The +host object can be of two kinds: a local or global variable, or an object +whose address is in a pointer expression. We distinguish the two cases so +that we can tell quickly whether we are accessing some component of a +variable directly or we are accessing a memory location through a pointer. +To make it easy to +tell what an lvalue means CIL represents lvalues as a host object and an +offset (see {!Cil_types.lval}). The host object (represented as +{!Cil_types.lhost}) can be a local or global variable or can be the object +pointed-to by a pointer expression. The offset (represented as +{!Cil_types.offset}) is a sequence of field or array index designators. + + Both the typing rules and the meaning of an lvalue is very precisely +specified in CIL. + + The following are a few useful function for operating on lvalues: +- {!Cil.mkMem} - makes an lvalue of [Mem] kind. Use this to ensure +that certain equivalent forms of lvalues are canonized. +For example, [*&x = x]. +- {!Cil.typeOfLval} - the type of an lvalue +- {!Cil.typeOffset} - the type of an offset, given the type of the +host. +- {!Cil.addOffset} and {!Cil.addOffsetLval} - extend sequences +of offsets. +- {!Cil.removeOffset} and {!Cil.removeOffsetLval} - shrink sequences +of offsets. + +The following equivalences hold {v +Mem(AddrOf(Mem a, aoff)), off = Mem a, aoff + off +Mem(AddrOf(Var v, aoff)), off = Var v, aoff + off +AddrOf (Mem a, NoOffset) = a + v} *) + +and lval = + lhost * offset + +(** The host part of an {!Cil_types.lval}. *) +and lhost = + | Var of varinfo + (** The host is a variable. *) + + | Mem of exp + (** The host is an object of type [T] when the expression has pointer + * [TPtr(T)]. *) + + +(** The offset part of an {!Cil_types.lval}. Each offset can be applied to certain + * kinds of lvalues and its effect is that it advances the starting address + * of the lvalue and changes the denoted type, essentially focussing to some + * smaller lvalue that is contained in the original one. + @plugin development guide *) +and offset = + | NoOffset (** No offset. Can be applied to any lvalue and does + * not change either the starting address or the type. + * This is used when the lval consists of just a host + * or as a terminator in a list of other kinds of + * offsets. *) + + | Field of fieldinfo * offset + (** A field offset. Can be applied only to an lvalue + * that denotes a structure or a union that contains + * the mentioned field. This advances the offset to the + * beginning of the mentioned field and changes the + * type to the type of the mentioned field. *) + + | Index of exp * offset + (** An array index offset. Can be applied only to an + * lvalue that denotes an array. This advances the + * starting address of the lval to the beginning of the + * mentioned array element and changes the denoted type + * to be the type of the array element *) + + +(** {b Initializers.} +A special kind of expressions are those that can appear as initializers for +global variables (initialization of local variables is turned into +assignments). The initializers are represented as type {!Cil_types.init}. You +can create initializers with {!Cil.makeZeroInit} and you can conveniently +scan compound initializers them with {!Cil.foldLeftCompound}. +*) +(** Initializers for global variables. *) +and init = + | SingleInit of exp (** A single initializer *) + | CompoundInit of typ * (offset * init) list + (** Used only for initializers of structures, unions and arrays. + * The offsets are all of the form [Field(f, NoOffset)] or + * [Index(i, NoOffset)] and specify the field or the index being + * initialized. For structures all fields + * must have an initializer (except the unnamed bitfields), in + * the proper order. This is necessary since the offsets are not + * printed. For arrays the list must contain a prefix of the + * initializers; the rest are 0-initialized. + * For unions there must be exactly one initializer. If + * the initializer is not for the first field then a field + * designator is printed, so you better be on GCC since MSVC does + * not understand this. You can scan an initializer list with + * {!Cil.foldLeftCompound}. *) + +(** We want to be able to update an initializer in a global variable, so we + * define it as a mutable field *) +and initinfo = { + mutable init : init option; + } + +(** {b Function definitions.} +A function definition is always introduced with a [GFun] constructor at the +top level. All the information about the function is stored into a +{!Cil_types.fundec}. Some of the information (e.g. its name, type, +storage, attributes) is stored as a {!Cil_types.varinfo} that is a field of the +[fundec]. To refer to the function from the expression language you must use +the [varinfo]. + + The function definition contains, in addition to the body, a list of all the +local variables and separately a list of the formals. Both kind of variables +can be referred to in the body of the function. The formals must also be shared +with the formals that appear in the function type. For that reason, to +manipulate formals you should use the provided functions +{!Cil.makeFormalVar} and {!Cil.setFormals}. +*) +(** Function definitions. + @plugin development guide *) +and fundec = + { mutable svar: varinfo; + (** Holds the name and type as a variable, so we can refer to it + * easily from the program. All references to this function either + * in a function call or in a prototype must point to the same + * [varinfo]. *) + mutable sformals: varinfo list; + (** Formals. These must be in the same order and with the same + * information as the formal information in the type of the function. + * Use {!Cil.setFormals} or + * {!Cil.setFunctionType} to set these formals and ensure that they + * are reflected in the function type. Do not make copies of these + * because the body refers to them. *) + mutable slocals: varinfo list; + (** Locals. Does NOT include the sformals. Do not make copies of + * these because the body refers to them. *) + mutable smaxid: int; (** Max local id. Starts at 0. Used for + * creating the names of new temporary + * variables. Updated by + * {!Cil.makeLocalVar} and + * {!Cil.makeTempVar}. You can also use + * {!Cil.setMaxId} to set it after you + * have added the formals and locals. *) + mutable sbody: block; (** The function body. *) + mutable smaxstmtid: int option; (** max id of a (reachable) statement + * in this function, if we have + * computed it. range = 0 ... + * (smaxstmtid-1). This is computed by + * {!Cil.computeCFGInfo}. *) + mutable sallstmts: stmt list; (** After you call {!Cil.computeCFGInfo} + * this field is set to contain all + * statements in the function *) + mutable sspec: funspec; + } + + +(** A block is a sequence of statements with the control falling through from + one element to the next *) +and block = + { mutable battrs: attributes; (** Attributes for the block *) + mutable blocals: varinfo list; (** variables that are local to + the block. It is a subset of the + slocals of the enclosing function. + *) + mutable bstmts: stmt list; (** The statements comprising the block*) + } + +(** {b Statements}. +CIL statements are the structural elements that make the CFG. They are +represented using the type {!Cil_types.stmt}. Every +statement has a (possibly empty) list of labels. The +{!Cil_types.stmtkind} field of a statement indicates what kind of statement it +is. + + Use {!Cil.mkStmt} to make a statement and the fill-in the fields. + +CIL also comes with support for control-flow graphs. The [sid] field in +[stmt] can be used to give unique numbers to statements, and the [succs] +and [preds] fields can be used to maintain a list of successors and +predecessors for every statement. The CFG information is not computed by +default. Instead you must explicitly use the functions +{!Cil.prepareCFG} and {!Cil.computeCFGInfo} to do it. + +*) +(** Statements. + @plugin development guide *) +and stmt = { + mutable labels: label list; + (** Whether the statement starts with some labels, case statements or + * default statements. *) + + mutable skind: stmtkind; + (** The kind of statement *) + + mutable sid: int; + (** A number (>= 0) that is unique in a function. Filled in only after + * the CFG is computed. *) + mutable succs: stmt list; + (** The successor statements. They can always be computed from the skind + * and the context in which this statement appears. Filled in only after + * the CFG is computed. *) + mutable preds: stmt list; + (** The inverse of the succs function. *) + + mutable ghost : bool + } + +(** Labels *) +and label = + Label of string * location * bool + (** A real label. If the bool is "true", the label is from the + * input source program. If the bool is "false", the label was + * created by CIL or some other transformation *) + | Case of exp * location (** A case statement. This expression + * is lowered into a constant if + * {!Cil.lowerConstants} is set to + * true. *) + | Default of location (** A default statement *) + + + +(* The various kinds of statements *) +and stmtkind = + | Instr of instr + (** A group of instructions that do not contain control flow. Control + * implicitly falls through. *) + + | Return of exp option * location + (** The return statement. This is a leaf in the CFG. *) + + | Goto of stmt ref * location + (** A goto statement. Appears from actual goto's in the code or from + * goto's that have been inserted during elaboration. The reference + * points to the statement that is the target of the Goto. This means that + * you have to update the reference whenever you replace the target + * statement. The target statement MUST have at least a label. *) + + | Break of location + (** A break to the end of the nearest enclosing Loop or Switch *) + + | Continue of location + (** A continue to the start of the nearest enclosing [Loop] *) + | If of exp * block * block * location + (** A conditional. Two successors, the "then" and the "else" branches. + * Both branches fall-through to the successor of the If statement. *) + + | Switch of exp * block * (stmt list) * location + (** A switch statement. The statements that implement the cases can be + * reached through the provided list. For each such target you can find + * among its labels what cases it implements. The statements that + * implement the cases are somewhere within the provided [block]. *) + + | Loop of code_annotation list * + block * location * (stmt option) * (stmt option) + (** A [while(1)] loop. The termination test is implemented in the body of + * a loop using a [Break] statement. If prepareCFG has been called, + * the first stmt option will point to the stmt containing the continue + * label for this loop and the second will point to the stmt containing + * the break label for this loop. *) + + | Block of block + (** Just a block of statements. Use it as a way to keep some block + * attributes local *) + + | UnspecifiedSequence of (stmt * lval list * lval list * lval list) list + (** statements whose order of execution is not specified by + ISO/C. This is important for the order of side effects + during evaluation of expressions. Each statement comes + together with three list of lval + - lvals that are written during the sequence and whose future + value depends upon the statement (it is legal to read from them) + - lvals that are written during the evaluation of the statement itself + - lval that are read. + Note that this include only a subset of the affectations + of the statement. Namely, the + temporary variables generated by cil are excluded (i.e. it + is assumed that the "compilation" is correct). In addition, + side effects caused by function applications are not taken + into account in the list. For a single statement, the written lvals + are supposed to be ordered (or their order of evaluation doesn't + matter), so that an alarm should be emitted only if the lvals read by + a statement overlap with the lvals written (or read) by another + statement of the sequence. + + At this time this feature is + experimental and may miss some unspecified sequences. + + In case you do not care about this feature just handle it + like a block (see {!Cil.block_from_unspecified_sequence}) *) + | TryFinally of block * block * location + (** On MSVC we support structured exception handling. This is what you + * might expect. Control can get into the finally block either from the + * end of the body block, or if an exception is thrown. *) + + | TryExcept of block * (instr list * exp) * block * location + (** On MSVC we support structured exception handling. The try/except + * statement is a bit tricky: +{v __try \{ blk \} + __except (e) \{ + handler + \} +v} + + The argument to __except must be an expression. However, we keep a + list of instructions AND an expression in case you need to make + function calls. We'll print those as a comma expression. The control + can get to the __except expression only if an exception is thrown. + After that, depending on the value of the expression the control + goes to the handler, propagates the exception, or retries the + exception !!! The location corresponds to the try keyword. + *) + + +(** Instructions. They may cause effects directly but may not have control + flow.*) +and instr = + Set of lval * exp * location (** An assignment. A cast is present + if the exp has different type + from lval *) + | Call of lval option * exp * exp list * location + (** optional: result is an lval. A cast might be + necessary if the declared result type of the + function is not the same as that of the + destination. If the function is declared then + casts are inserted for those arguments that + correspond to declared formals. (The actual + number of arguments might be smaller or larger + than the declared number of arguments. C allows + this.) If the type of the result variable is not + the same as the declared type of the function + result then an implicit cast exists. *) + + (* See the GCC specification for the meaning of ASM. + * If the source is MS VC then only the templates + * are used *) + (* sm: I've added a notes.txt file which contains more + * information on interpreting Asm instructions *) + | Asm of attributes * (* Really only const and volatile can appear + * here *) + string list * (* templates (CR-separated) *) + (string option * string * lval) list * + (* outputs must be lvals with + * optional names and constraints. + * I would like these + * to be actually variables, but I + * run into some trouble with ASMs + * in the Linux sources *) + (string option * string * exp) list * + (* inputs with optional names and constraints *) + string list * (* register clobbers *) + location + (** An inline assembly instruction. The arguments are (1) a list of + attributes (only const and volatile can appear here and only for + GCC), (2) templates (CR-separated), (3) a list of + outputs, each of which is an lvalue with a constraint, (4) a list + of input expressions along with constraints, (5) clobbered + registers, and (5) location information *) + + | Skip of location + + | Code_annot of code_annotation * location + +(** Describes a location in a source file *) +and location = Lexing.position * Lexing.position + +(** Type signatures. Two types are identical iff they have identical + signatures *) +and typsig = + TSArray of typsig * int64 option * attribute list + | TSPtr of typsig * attribute list + | TSComp of bool * string * attribute list + | TSFun of typsig * typsig list * bool * attribute list + | TSEnum of string * attribute list + | TSBase of typ + +(** Abstract syntax trees for annotations *) + +(** Types of logic terms. *) +and logic_type = + | Ctype of typ (** a C type *) + | Ltype of logic_type_info * logic_type list + (** an user-defined logic type with its parameters *) + | Lvar of string (** a type variable. *) + | Linteger (** mathematical integers, {i i.e.} Z *) + | Lreal (** mathematical reals, {i i.e.} R *) + | Larrow of logic_type list * logic_type (** (n-ary) function type *) + +(** tsets with an unique identifier. + Use [Logic_const.new_location] to generate a new id. *) +and identified_term = + { it_id: int; (** the identifier. *) + it_content: term (** the term *) + } + +(** logic label referring to a particular program point. *) +and logic_label = + | StmtLabel of stmt ref (** label of a C statement. *) + | LogicLabel of string (** builtin logic label ({t Here, Pre}, ...) *) + +(* Expressions follow CIL constructs (with prefix T) *) + +(** Logic terms. *) +and term = { + term_node : term_node; (** kind of term. *) + term_loc : Lexing.position * Lexing.position; + (** position in the source file. *) + term_type : logic_type; (** type of the term. *) + term_name: string list; (** names of the term if any. *) +} + +(** the various kind of terms. *) +and term_node = + (* same constructs as exp *) + | TConst of constant (** a constant. *) + | TLval of term_lval (** an L-value *) + | TSizeOf of typ (** size of a given C type. *) + | TSizeOfE of term (** size of the type of an expression. *) + | TSizeOfStr of string (** size of a string constant. *) + | TAlignOf of typ (** alignment of a type. *) + | TAlignOfE of term (** alignment of the type of an expression. *) + | TUnOp of unop * term (** unary operator. *) + | TBinOp of binop * term * term (** binary operators. *) + | TCastE of typ * term (** cast to a C type. *) + | TAddrOf of term_lval (** address of a term. *) + | TStartOf of term_lval (** beginning of an array. *) + (* additional constructs *) + | Tapp of logic_info * (logic_label * logic_label) list * term list + (** application of a logic function. *) + | Tlambda of quantifiers * term (** lambda abstraction. *) + | TDataCons of logic_ctor_info * term list + (** constructor of logic sum-type. *) + | Tif of term * term * term + (** conditional operator*) + | Told of term (** term refers to the pre-state of the function. *) + | Tat of term * logic_label + (** term refers to a particular program point. *) + | Tbase_addr of term (** base address of a pointer. *) + | Tblock_length of term (** length of the block pointed to by the term. *) + | Tnull (** the null pointer. *) + | TCoerce of term * typ (** coercion to a given C type. *) + | TCoerceE of term * term (** coercion to the type of a given term. *) + | TUpdate of term * fieldinfo * term + (** functional update of a field. *) + | Ttypeof of term (** type tag for a term. *) + | Ttype of typ (** type tag for a C type. *) + | Tempty_set (** the empty set. *) + | Tunion of term list (** union of terms. *) + | Tinter of term list (** intersection of terms. *) + | Tcomprehension of + term * quantifiers * predicate named option + (** set defined in comprehension ({t \{ t[i] | integer i; 0 <= i < 5\}}) + *) + | Trange of term option * term option (** range of integers. *) + | Tlet of logic_info * term (** local binding *) + +(** lvalue: base address and offset. *) +and term_lval = + term_lhost * term_offset + +(** base address of an lvalue. *) +and term_lhost = + | TVar of logic_var (** a variable. *) + | TResult of typ (** value returned by a C function. + Only used in post-conditions or assigns + *) + | TMem of term (** memory access. *) + +(** offset of an lvalue. *) +and term_offset = + | TNoOffset (** no further offset. *) + | TField of fieldinfo * term_offset + (** access to the field of a compound type. *) + | TIndex of term * term_offset + (** index. Note that a range is denoted by [TIndex(t,Trange(i1,i2))] *) + +(** description of a logic function or predicate. +@plugin development guide *) +and logic_info = { +(* + mutable l_name : string; (** name of the function. *) +*) + mutable l_var_info : logic_var; + (** we use only fields lv_name and lv_id of l_var_info + we should factorize lv_type and l_type+l_profile below *) + mutable l_labels : logic_label list; (** label arguments of the function. *) + mutable l_tparams : string list; (** type parameters *) + mutable l_type : logic_type option; (** return type. None for predicates *) + mutable l_profile : logic_var list; (** type of the arguments. *) + mutable l_body : logic_body; (** body of the function. *) +} + +and builtin_logic_info = + { mutable bl_name: string; + mutable bl_labels: logic_label list; + mutable bl_params: string list; + mutable bl_type: logic_type option; + mutable bl_profile: (string * logic_type) list; + } + +and logic_body = + | LBnone + (** no definition and no reads clause *) + | LBreads of identified_term list + (** read accesses performed by a function. *) + | LBterm of term (** direct definition of a function. *) + | LBpred of predicate named (** direct definition of a predicate. *) + | LBinductive of + (string * logic_label list * string list * predicate named) list + (** inductive definition *) + +(** description of a logic type*) +and logic_type_info = + { lt_name: string; + lt_params : string list; (** type parameters*) + mutable lt_def: logic_type_def option + (** definition of the type. None for abstract types. *) + } + (* will be expanded when dealing with concrete types *) + +and logic_type_def = + | LTsum of logic_ctor_info list (** sum type with its constructors. *) + | LTsyn of logic_type (** Synonym of another type. *) + +(** description of a logic variable +@plugin development guide *) +and logic_var = { + mutable lv_name : string; (** name of the variable. *) + mutable lv_id : int; (** unique identifier *) + mutable lv_type : logic_type; (** type of the variable. *) + mutable lv_origin : varinfo option (** when the logic variable stems from a + C variable, set to the original C variable. + *) +} + +(** description of a constructor of a logic sum-type*) +and logic_ctor_info = + { ctor_name: string; (** name of the constructor. *) + ctor_type: logic_type_info; (** type to which the constructor belongs. *) + ctor_params: logic_type list + (** types of the parameters of the constructor. *) + } + +(* Predicates *) + +(** variables bound by a quantifier. *) +and quantifiers = logic_var list + +(** comparison relations*) +and relation = Rlt | Rgt | Rle | Rge | Req | Rneq + +(** predicates *) +and predicate = + | Pfalse (** always-false predicate. *) + | Ptrue (** always-true predicate. *) + | Papp of logic_info * (logic_label * logic_label) list * term list + (** application of a predicate. *) + | Pseparated of term list + | Prel of relation * term * term + (** comparison of two terms. *) + | Pand of predicate named * predicate named + (** conjunction *) + | Por of predicate named * predicate named + (** disjunction. *) + | Pxor of predicate named * predicate named + (** logical xor. *) + | Pimplies of predicate named * predicate named + (** implication. *) + | Piff of predicate named * predicate named + (** equivalence. *) + | Pnot of predicate named + (** negation. *) + | Pif of term * predicate named * predicate named + (** conditional *) + | Plet of logic_info * predicate named + (** definition of a local variable *) + | Pforall of quantifiers * predicate named + (** universal quantification. *) + | Pexists of quantifiers * predicate named + (** existential quantification. *) + | Pold of predicate named + (** predicate refers to the pre-state of a function. *) + | Pat of predicate named * logic_label + (** predicate refers to a particular program point. *) + | Pvalid of term + (** the given locations are valid. *) + | Pvalid_index of term * term + (** {b deprecated:} Use [Pvalid(TLval(TBinOp(PlusPI,p,i)))] instead + + [Pvalid_index(p,i)] indicates that accessing the [i]th element + of [p] is valid. + *) + | Pvalid_range of term * term * term + (** {b deprecated:} Use [Pvalid(TLVal(TBinOp(PlusPI(p,Trange(i1,i2)))))] + instead + + similar to [Pvalid_index] but for a range of indices.*) + | Pfresh of term + (** The given term is newly allocated in the post-state of a function.*) + | Psubtype of term * term + (** First term is a type tag that is a subtype of the second. *) + +(** predicate with an unique identifier. +Use [Logic_const.new_predicate] to create fresh predicates *) +and identified_predicate = { + ip_name: string list; (** names given to the predicate if any.*) + ip_loc: location; (** location in the source code. *) + ip_id: int; (** identifier *) + ip_content: predicate; (** the predicate itself*) +} + +(* Polymorphic types shared with parsed trees (Logic_ptree) *) +(** variant of a loop or a recursive function. Type shared with Logic_ptree. *) +and 'term variant = 'term * string option + +(** zone assigned by a C function. Type shared with Logic_ptree. *) +and 'locs zone = + Location of 'locs (** tsets *) + | Nothing (** nothing is assigned. *) + +(** zone assigned with its dependencies. Type shared with Logic_ptree.*) +and 'locs assigns = 'locs zone * ('locs zone list) + +(** object that can be named (in particular predicates). *) +and 'a named = { name : string list; (** list of given names *) + loc : location; (** position in the source code. *) + content : 'a; (** content *) + } + +(** function contract. Type shared with Logic_ptree. *) +and ('term,'pred,'locs) spec = { + mutable spec_requires : 'pred list; (** global requirements. *) + mutable spec_behavior : ('pred,'locs) behavior list; + (** behaviors *) + mutable spec_variant : 'term variant option; + (** variant for recursive functions. *) + mutable spec_terminates: 'pred option; + (** termination condition. *) + mutable spec_complete_behaviors: string list list; + (** list of complete behaviors. + It is possible to have more than one set of complete behaviors *) + mutable spec_disjoint_behaviors: string list list; + (** list of disjoint behaviors. + It is possible to have more than one set of disjoint behaviors *) +} + +(** behavior of a function. Type shared with Logic_ptree. + @modify Boron-20100401 [b_ensures] is replaced by [b_post_cond]. + Old [b_ensures] represent the [Normal] case of [b_post_cond]. + *) +and ('pred,'locs) behavior = { + mutable b_name : string; (** name of the behavior. *) + mutable b_assumes : 'pred list; (** assume clauses. *) + mutable b_post_cond : (termination_kind * 'pred) list; (** post-condition. *) + mutable b_assigns : 'locs assigns list; (** assignments. *) +} + +(** pragmas for the value analysis plugin of Frama-C. +Type shared with Logic_ptree.*) +and 'term loop_pragma = + | Unroll_level of 'term + | Widen_hints of 'term list + | Widen_variables of 'term list + +(** pragmas for the slicing plugin of Frama-C. Type shared with Logic_ptree.*) +and 'term slice_pragma = + | SPexpr of 'term + | SPctrl + | SPstmt + +(** pragmas for the impact plugin of Frama-C. Type shared with Logic_ptree.*) +and 'term impact_pragma = + | IPexpr of 'term + | IPstmt + +(** the various kinds of pragmas. Type shared with Logic_ptree. *) +and 'term pragma = + | Loop_pragma of 'term loop_pragma + | Slice_pragma of 'term slice_pragma + | Impact_pragma of 'term impact_pragma + +(** Annotation status *) +and validity = True | False | Maybe +and annot_checked_status = { mutable emitter : string; + mutable valid : validity } +and annotation_status = | Unknown (* Nothing was ever tried to check it *) + | Checked of annot_checked_status (* Something was tried *) +and annot_status = { mutable status : annotation_status } +(** all annotations that can be found in the code. + Type shared with Logic_ptree. *) +and ('term, 'pred, 'spec_pred, 'locs) code_annot = + | AAssert of string list * 'pred * annot_status + (** assertion to be checked. The list of strings is the list of + behaviors to which this assertion applies. + @deprecated since Beryllium-20090902, the annot_status + field is no longer updated by anyone. Use {!Db.Annotations.Status} + functions to access the true status. *) + + | AStmtSpec of ('term, 'spec_pred, 'locs) spec (** statement contract. *) + | AInvariant of string list * bool * 'pred + (** code invariant. The list of strings is the list of + behaviors to which this invariant applies. + The boolean flag is true for normal loop invariants + and false for invariant-as-assertions. + TODO: remove this constructor: + - normal loop invariants are now under constructor ALoopBehavior + - invariant-as-assertions should be just one variant of AAssert + *) + | AVariant of 'term variant (** loop variant. Note that + there can be at most one variant + associated to a given statement + *) + | AAssigns of string list * 'locs assigns + | APragma of 'term pragma (** pragma. *) + +(** function contract. *) +and funspec = (term, identified_predicate, identified_term) spec + +(** code annotation with an unique identifier. + Use [Logic_const.new_code_annotation] to create new code annotations with + a fresh id. *) +and code_annotation = + { annot_content : + (term, predicate named, identified_predicate, identified_term) + code_annot; (** content of the annotation. *) + annot_id: int (** identifier. *) } + +(** behavior of a function. *) +and funbehavior = (identified_predicate,identified_term) behavior + +(** global annotations, not attached to a statement or a function. *) +and global_annotation = + | Dfun_or_pred of logic_info + | Daxiomatic of string * global_annotation list + | Dtype of logic_type_info (** declaration of a logic type. *) + | Dlemma of string * bool * logic_label list * string list * predicate named + (** definition of a lemma. The boolean flag is true if the property. + should be taken as an axiom and false if it must be proved. + *) + | Dinvariant of logic_info + (** global invariant. The predicate does not have any argument. *) + | Dtype_annot of logic_info + (** type invariant. The predicate has exactly one argument. *) + +type kinstr = + | Kstmt of stmt + | Kglobal + +type mach = { + version_major: int; (* Major version number *) + version_minor: int; (* Minor version number *) + version: string; (* version number *) + underscore_name: bool; (* If assembly names have leading underscore *) + sizeof_short: int; (* Size of "short" *) + sizeof_int: int; (* Size of "int" *) + sizeof_long: int ; (* Size of "long" *) + sizeof_longlong: int; (* Size of "long long" *) + sizeof_ptr: int; (* Size of pointers *) + sizeof_enum: int; (* Size of enum types *) + sizeof_float: int; (* Size of "float" *) + sizeof_double: int; (* Size of "double" *) + sizeof_longdouble: int; (* Size of "long double" *) + sizeof_void: int; (* Size of "void" *) + sizeof_fun: int; (* Size of function *) + size_t: string; (* Type of "sizeof(T)" *) + wchar_t: string; (* Type of "wchar_t" *) + ptrdiff_t: string; (* Type of "ptrdiff_t" *) + enum_are_signed: bool; (* Sign of enum types *) + alignof_short: int; (* Alignment of "short" *) + alignof_int: int; (* Alignment of "int" *) + alignof_long: int; (* Alignment of "long" *) + alignof_longlong: int; (* Alignment of "long long" *) + alignof_ptr: int; (* Alignment of pointers *) + alignof_enum: int; (* Alignment of enum types *) + alignof_float: int; (* Alignment of "float" *) + alignof_double: int; (* Alignment of "double" *) + alignof_longdouble: int; (* Alignment of "long double" *) + alignof_str: int; (* Alignment of strings *) + alignof_fun: int; (* Alignment of function *) + alignof_char_array: int; (* Alignment of arrays of char *) + char_is_unsigned: bool; (* Whether "char" is unsigned *) + const_string_literals: bool; (* Whether string literals have const chars *) + little_endian: bool; (* whether the machine is little endian *) +} + +(* +Local Variables: +compile-command: "LC_ALL=C make -C ../.." +End: +*) diff --git a/dumpcil/Makefile b/dumpcil/Makefile deleted file mode 100644 --- a/dumpcil/Makefile +++ /dev/null @@ -1,11 +0,0 @@ -FRAMAC_SHARE :=$(shell frama-c.byte -print-path) -FRAMAC_LIBDIR :=$(shell frama-c.byte -print-libpath) -PLUGIN_NAME = DumpCIL -PLUGIN_CMO = dump_cil - -include $(FRAMAC_SHARE)/Makefile.dynamic - -.PHONY:clean-all -clean-all: clean - -rm -f .depend - -rm -f $(FRAMAC_LIBDIR)/DumpCIL.* diff --git a/dumpcil/dump_cil.ml b/dumpcil/dump_cil.ml deleted file mode 100644 --- a/dumpcil/dump_cil.ml +++ /dev/null @@ -1,59 +0,0 @@ -open Ast -open Cil_types -open File -open Lexing -open List - -let error loc msg = prerr_endline ("ERROR: " ^ msg); exit 1 - -let unknown = - { pos_fname = "unknown" - ; pos_lnum = 0 - ; pos_bol = 0 - ; pos_cnum = 0 - } - -let format_fundec _ _ = "function declaration" - -let format_global a = match a with - GType (a, loc) -> "typedef" - | GCompTag (a, loc) -> "struct-union definition" - | GCompTagDecl (a, loc) -> "struct-union declaration" - | GEnumTag (a, loc) -> "enum definition" - | GEnumTagDecl (a, loc) -> "enum declaration" - | GVarDecl (f, v, loc) -> "variable declaration" - | GVar (v, i, loc) -> "variable definition" - | GFun (a, loc) -> format_fundec a loc - | GAsm (_, loc) -> error loc "asm not supported" - | GPragma (a, loc) -> "" - | GText _ -> "text" - | GAnnot _ -> "annot" - -let dump file = - (match file.globinit with - None -> () - | Some f -> error unknown "initializer not supported"); - iter (fun a -> if String.length a == 0 then () else print_endline a) (map format_global file.globals) - -let run () = - File.init_from_cmdline (); - dump (Ast.get ()) - -module Self = - Plugin.Register - (struct - let name = "DumpCIL" - let shortname = "DumpCIL" - let descr = "Dumps CIL and ACSL to stdout." - end);; - -module Enabled = - Self.False - (struct - let option_name = "-dumpcil" - let descr = "Dumps CIL and ACSL to stdout." - end);; - -let () = Db.Main.extend (fun () -> if Enabled.get () then run ()) - -