From 98875970732b00613701bfd05c7a57c923fcd885 Mon Sep 17 00:00:00 2001 From: Andor Penzes Date: Thu, 30 Apr 2020 01:14:22 +0200 Subject: [PATCH 01/15] Sketch of datalog exporter. --- grin/grin.cabal | 4 +- grin/src/Grin/ExtendedSyntax/Datalog.hs | 281 +++++++++++++++++++++ grin/src/Grin/ExtendedSyntax/SyntaxDefs.hs | 8 + stack.yaml | 2 + 4 files changed, 294 insertions(+), 1 deletion(-) create mode 100644 grin/src/Grin/ExtendedSyntax/Datalog.hs diff --git a/grin/grin.cabal b/grin/grin.cabal index 59b7fd9e..788c1272 100644 --- a/grin/grin.cabal +++ b/grin/grin.cabal @@ -115,6 +115,7 @@ library Grin.ExtendedSyntax.TypeEnv Grin.ExtendedSyntax.TypeEnvDefs Grin.ExtendedSyntax.GADT + Grin.ExtendedSyntax.Datalog Pipeline.Eval Pipeline.Optimizations Pipeline.Pipeline @@ -239,7 +240,8 @@ library random, set-extra, deepseq, - binary + binary, + souffle-haskell default-language: Haskell2010 diff --git a/grin/src/Grin/ExtendedSyntax/Datalog.hs b/grin/src/Grin/ExtendedSyntax/Datalog.hs new file mode 100644 index 00000000..78b202cd --- /dev/null +++ b/grin/src/Grin/ExtendedSyntax/Datalog.hs @@ -0,0 +1,281 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +module Grin.ExtendedSyntax.Datalog where + +import Control.Monad (forM_) +import Data.Int +import Language.Souffle.Interpreted as Souffle +import GHC.Generics +import Control.Monad.Trans +import Control.Monad.Trans.Reader +import Data.Text (Text) +import qualified Grin.ExtendedSyntax.Syntax as Grin +import qualified Data.Text as Text + +data HPT = HPT + +instance Souffle.Program HPT where + type ProgramFacts HPT = + '[ External + , ExternalParam + , Move + , LitAssign + , Node + , NodeArgument + , Fetch + , Store + , Update + , Call + , CallArgument + , NodePattern + , NodeParameter + , Case + , Alt + , AltLiteral + , AltDefault + , ReturnValue + , FirstInst + , NextInst + , FunctionParameter + , AltParameter + ] + programName = const "hpt" + +type Function = Text +type Boolean = Int32 +type SimpleType = Text +type Number = Int32 +type Variable = Text +type Literal = Text +type Tag = Text -- TODO: TagType? +type CodeName = Text + +--instance Souffle.Marshal Grin.Name where +-- push (Grin.NM n) = push n +-- pop = Grin.NM <$> pop + +data External = External !Function !Boolean !SimpleType deriving (Eq, Show, Generic) +data ExternalParam = ExternalParam !Function !Number !SimpleType deriving (Eq, Show, Generic) +data Move = Move !Variable !Variable deriving (Eq, Show, Generic) +data LitAssign = LitAssign !Variable !SimpleType !Literal deriving (Eq, Show, Generic) +data Node = Node !Variable !Tag deriving (Eq, Show, Generic) +data NodeArgument = NodeArgument !Variable !Number !Variable deriving (Eq, Show, Generic) +data Fetch = Fetch !Variable !Variable deriving (Eq, Show, Generic) +data Store = Store !Variable !Variable deriving (Eq, Show, Generic) +data Update = Update !Variable !Variable !Variable deriving (Eq, Show, Generic) +data Call = Call !Variable !Function deriving (Eq, Show, Generic) +data CallArgument = CallArgument !Variable !Number !Variable deriving (Eq, Show, Generic) +data NodePattern = NodePattern !Variable !Tag !Variable deriving (Eq, Show, Generic) +data NodeParameter = NodeParameter !Variable !Number !Variable deriving (Eq, Show, Generic) +data Case = Case !Variable !Variable deriving (Eq, Show, Generic) +data Alt = Alt !Variable !Variable !Tag deriving (Eq, Show, Generic) +data AltLiteral = AltLiteral !Variable !Variable !Literal deriving (Eq, Show, Generic) +data AltDefault = AltDefault !Variable !Variable deriving (Eq, Show, Generic) +data ReturnValue = ReturnValue !CodeName !Variable deriving (Eq, Show, Generic) +data FirstInst = FirstInst !CodeName !Variable deriving (Eq, Show, Generic) +data NextInst = NextInst !Variable !Variable deriving (Eq, Show, Generic) +data FunctionParameter = FunctionParameter !Function !Number !Variable deriving (Eq, Show, Generic) +data AltParameter = AltParameter !Variable !Tag !Number {-!Variable-} deriving (Eq, Show, Generic) + +instance Souffle.Marshal External +instance Souffle.Marshal ExternalParam +instance Souffle.Marshal Move +instance Souffle.Marshal LitAssign +instance Souffle.Marshal Node +instance Souffle.Marshal NodeArgument +instance Souffle.Marshal Fetch +instance Souffle.Marshal Store +instance Souffle.Marshal Update +instance Souffle.Marshal Call +instance Souffle.Marshal CallArgument +instance Souffle.Marshal NodePattern +instance Souffle.Marshal NodeParameter +instance Souffle.Marshal Case +instance Souffle.Marshal Alt +instance Souffle.Marshal AltLiteral +instance Souffle.Marshal AltDefault +instance Souffle.Marshal ReturnValue +instance Souffle.Marshal FirstInst +instance Souffle.Marshal NextInst +instance Souffle.Marshal FunctionParameter +instance Souffle.Marshal AltParameter + +instance Souffle.Fact External where factName = const "external" +instance Souffle.Fact ExternalParam where factName = const "externalparam" +instance Souffle.Fact Move where factName = const "move" +instance Souffle.Fact LitAssign where factName = const "litassign" +instance Souffle.Fact Node where factName = const "node" +instance Souffle.Fact NodeArgument where factName = const "nodeargument" +instance Souffle.Fact Fetch where factName = const "fetch" +instance Souffle.Fact Store where factName = const "store" +instance Souffle.Fact Update where factName = const "update" +instance Souffle.Fact Call where factName = const "call" +instance Souffle.Fact CallArgument where factName = const "callargument" +instance Souffle.Fact NodePattern where factName = const "nodepattern" +instance Souffle.Fact NodeParameter where factName = const "nodeparameter" +instance Souffle.Fact Case where factName = const "case" +instance Souffle.Fact Alt where factName = const "alt" +instance Souffle.Fact AltLiteral where factName = const "altliteral" +instance Souffle.Fact AltDefault where factName = const "altdefault" +instance Souffle.Fact ReturnValue where factName = const "returnvalue" +instance Souffle.Fact FirstInst where factName = const "firstinst" +instance Souffle.Fact NextInst where factName = const "nextinst" +instance Souffle.Fact FunctionParameter where factName = const "functionparameter" +instance Souffle.Fact AltParameter where factName = const "altparameter" + + +gtagToDtag :: Grin.Tag -> Tag +gtagToDtag (Grin.Tag tt name) = (renderTagType tt) <> Grin.nameText name + where + renderTagType :: Grin.TagType -> Text + renderTagType Grin.C = "C" + renderTagType Grin.F = "F" + renderTagType (Grin.P m) = "P-" <> Text.pack (show m) <> "-" + +-- type Souffle a = ReaderT (Handle HPT) SouffleM a + +convertExternals :: [Grin.External] -> SouffleM () +convertExternals = undefined + +emitAlg :: Handle HPT -> Grin.ExpF (Grin.Exp, SouffleM ()) -> SouffleM () +emitAlg prog = \case + Grin.ProgramF externals defs -> do + convertExternals externals + mapM_ snd defs + + -- f param0 param1 = ... + -- .decl FunctionParameter(f:Function, i:number, parameter:Variable) + Grin.DefF name args (_, body) -> do + Souffle.addFacts prog $ + zipWith (\n a -> FunctionParameter (Grin.nameText name) n (Grin.nameText a)) [0..] args + body + + -- result <- pure value + -- .decl Move(result:Variable, value:Variable) + Grin.EBindF (Grin.SReturn (Grin.Var val), lhs) (Grin.VarPat res) (_, rhs) -> do + lhs + Souffle.addFact prog $ Move (Grin.nameText res) (Grin.nameText val) + rhs + + -- result <- pure 1 + -- .decl LitAssign(result:Variable, l:Literal) + Grin.EBindF (Grin.SReturn (Grin.Lit l), lhs) (Grin.VarPat res) (_, rhs) -> do + lhs + Souffle.addFact prog $ litAssignFact res l + rhs + + -- result_node <- pure (Ctag item0 item1) + -- .decl Node(result_node:Variable, t:Tag) + -- .decl NodeArgument(result_node:Variable, i:number, item:Variable) + Grin.EBindF ((Grin.SReturn (Grin.ConstTagNode tag items)), lhs) (Grin.VarPat res) (_, rhs) -> do + lhs + Souffle.addFact prog $ Node (Grin.nameText res) (gtagToDtag tag) + Souffle.addFacts prog $ + zipWith (\n v -> NodeArgument (Grin.nameText res) n (Grin.nameText v)) [0..] items + rhs + + -- example: result <- fetch value + -- .decl Fetch(result:Variable, value:Variable) + Grin.EBindF (Grin.SFetch val, lhs) (Grin.VarPat res) (_, rhs) -> do + lhs + Souffle.addFact prog $ Fetch (Grin.nameText res) (Grin.nameText val) + rhs + + -- example: result <- store value + -- .decl Store(result:Variable, value:Variable) + Grin.EBindF (Grin.SStore val, lhs) (Grin.VarPat res) (_, rhs) -> do + lhs + Souffle.addFact prog $ Store (Grin.nameText res) (Grin.nameText val) + rhs + + -- example: result <- update target value + -- .decl Update(result:Variable, target:Variable, value:Variable) + Grin.EBindF (Grin.SUpdate target val, lhs) (Grin.VarPat res) (_, rhs) -> do + lhs + Souffle.addFact prog $ Update (Grin.nameText res) (Grin.nameText target) (Grin.nameText val) + rhs + + -- call_result <- f value0 value1 + -- .decl Call(call_result:Variable, f:Function) + -- .decl CallArgument(call_result:Variable, i:number, value:Variable) + Grin.EBindF (Grin.SApp fun args, lhs) (Grin.VarPat res) (_, rhs) -> do + lhs + Souffle.addFact prog $ Call (Grin.nameText res) (Grin.nameText fun) + Souffle.addFacts prog $ + zipWith (\n a -> CallArgument (Grin.nameText res) n (Grin.nameText a)) [0..] args + rhs + + -- AsPat { _bPatTag :: Tag + -- , _bPatFields :: [Name] + -- , _bPatVar :: Name + -- } + + -- bind pattern + -- node@(Ctag param0 param1) <- pure input_value + -- .decl NodePattern(node:Variable, t:Tag, input_value:Variable) + -- .decl NodeParameter(node:Variable, i:number, parameter:Variable) + Grin.EBindF (Grin.SReturn (Grin.Var inp_val), lhs) (Grin.AsPat tag pms nd) (_, rhs) -> do + lhs + Souffle.addFact prog $ NodePattern (Grin.nameText nd) (gtagToDtag tag) (Grin.nameText inp_val) + Souffle.addFacts prog $ + zipWith (\n p -> NodeParameter (Grin.nameText nd) n (Grin.nameText p)) [0..] pms + rhs + + -- case + alt + -- example: + -- case_result <- case scrut of + -- alt_value@(Ctag param0 param1) -> basic_block_name arg0 arg1 + -- .decl Case(case_result:Variable, scrutinee:Variable) + -- .decl Alt(case_result:Variable, alt_value:Variable, t:Tag) + -- .decl AltParameter(case_result:Variable, t:Tag, i:number, parameter:Variable) + -- .decl AltLiteral(case_result:Variable, alt_value:Variable, l:Literal) + -- .decl AltDefault(case_result:Variable, alt_value :: Variable) + Grin.EBindF (Grin.ECase scr alts, lhs) (Grin.VarPat cs_res) (_, rhs) -> do + lhs + Souffle.addFact prog $ Case (Grin.nameText cs_res) (Grin.nameText scr) + -- -- TODO: Improve performance by grouping alternatives + forM_ alts $ \case + Grin.Alt (Grin.NodePat tag args) n _ -> do + Souffle.addFact prog $ Alt (Grin.nameText cs_res) (Grin.nameText n) (gtagToDtag tag) + Souffle.addFacts prog $ + zipWith + (\j a -> AltParameter (Grin.nameText cs_res) (gtagToDtag tag) j {-(Grin.nameText a)-}) + [0..] + args + + -- TODO: Handle literals better + -- Grin.Alt (Grin.LitPat (G.SInt64 i)) n _ -> + -- [ AltLiteral + -- { case_result = Variable cs_res + -- , alt_value = Variable n + -- , l = Literal (show i) + -- } + -- ] + + Grin.Alt Grin.DefaultPat n _ -> do + Souffle.addFact prog $ AltDefault (Grin.nameText cs_res) (Grin.nameText n) + + rhs + +litAssignFact :: Grin.Name -> Grin.Lit -> LitAssign +litAssignFact v sv = (\(ty, value) -> LitAssign (Grin.nameText v) ty value) $ case sv of + Grin.LInt64 i -> (stToDatalogST Grin.T_Int64, Text.pack $ show i) + Grin.LWord64 w -> (stToDatalogST Grin.T_Word64, Text.pack $ show w) + Grin.LFloat f -> (stToDatalogST Grin.T_Float, Text.pack $ show f) + Grin.LBool b -> (stToDatalogST Grin.T_Bool, Text.pack $ show b) + Grin.LChar c -> (stToDatalogST Grin.T_Char, Text.pack $ show c) + Grin.LString s -> (stToDatalogST Grin.T_String, s) -- TODO + +stToDatalogST :: Grin.SimpleType -> SimpleType +stToDatalogST = \case + Grin.T_Int64 -> "Int64" + Grin.T_Word64 -> "Word64" + Grin.T_Float -> "Float" + Grin.T_Bool -> "Bool" + Grin.T_Char -> "Char" + Grin.T_Unit -> "Unit" + Grin.T_String -> "String" + other -> error $ "stToDatalogST: None handled case: " ++ show other diff --git a/grin/src/Grin/ExtendedSyntax/SyntaxDefs.hs b/grin/src/Grin/ExtendedSyntax/SyntaxDefs.hs index 5f40c516..15ba0d69 100644 --- a/grin/src/Grin/ExtendedSyntax/SyntaxDefs.hs +++ b/grin/src/Grin/ExtendedSyntax/SyntaxDefs.hs @@ -17,6 +17,9 @@ data Name | NI !Int deriving (Generic, Data, NFData, Binary, Eq, Ord, Show) +mkName :: Text -> Name +mkName = NM + nMap :: (Text -> Text) -> Name -> Name nMap f (NM n) = NM (f n) @@ -32,6 +35,11 @@ instance IsString Name where instance PrintfArg Name where formatArg = formatString . unpack . unNM +nameText :: Name -> Text +nameText = \case + NM n -> n + _ -> error "Name index found." -- This could have left in the AST after a problematic deserialisation. + nameString :: Name -> String nameString = \case NM n -> unpack n diff --git a/stack.yaml b/stack.yaml index 25a6097b..e6fe3df2 100644 --- a/stack.yaml +++ b/stack.yaml @@ -18,6 +18,8 @@ extra-deps: subdirs: - llvm-hs - llvm-hs-pure + - github: luc-tielen/souffle-haskell + commit: c76bd446c210b32e7a1de55b37a4df051586f108 flags: llvm-hs: From bc8f9d3e73bb04bb0260a24049ffa10f1f39f731 Mon Sep 17 00:00:00 2001 From: Andor Penzes Date: Fri, 1 May 2020 23:19:16 +0200 Subject: [PATCH 02/15] Run Souffle HPT --- datalog/hpt/hpt.dl | 340 ++++++++++++++++++ grin/app/CLI/Lib.hs | 1 + grin/grin.cabal | 1 + grin/src/Grin/ExtendedSyntax/Datalog.hs | 251 +++++++++---- grin/src/Pipeline/Pipeline.hs | 19 +- .../ExtendedSyntax/Normalisation.hs | 64 ++++ .../ExtendedSyntax/NormalisationSpec.hs | 37 ++ stack.yaml | 2 +- 8 files changed, 650 insertions(+), 65 deletions(-) create mode 100644 datalog/hpt/hpt.dl create mode 100644 grin/src/Transformations/ExtendedSyntax/Normalisation.hs create mode 100644 grin/test/Transformations/ExtendedSyntax/NormalisationSpec.hs diff --git a/datalog/hpt/hpt.dl b/datalog/hpt/hpt.dl new file mode 100644 index 00000000..f886e619 --- /dev/null +++ b/datalog/hpt/hpt.dl @@ -0,0 +1,340 @@ +.type Function +.type Variable +.type Tag +.type Literal +.type SimpleType +.type CodeName = Variable | Function + +// External function (name, effectful) +.decl External(f:Function,effectful:number,ret:SimpleType) +.decl ExternalParam(f:Function, i:number, st:SimpleType) + +// variable +// example: result <- pure value +.decl Move(result:Variable, value:Variable) + +// literal value +// example: result <- pure 1 +.decl LitAssign(result:Variable, st:SimpleType, l:Literal) + +// node value +// example: result_node <- pure (Ctag item0 item1) +.decl Node(result_node:Variable, t:Tag) +.decl NodeArgument(result_node:Variable, i:number, item:Variable) + +// store/fetch/update +// example: result <- fetch value +.decl Fetch(result:Variable, value:Variable) +// example: result <- store value +.decl Store(result:Variable, value:Variable) +// example: result <- update target value +.decl Update(result:Variable, target:Variable, value:Variable) + + +// app a.k.a. call +// example: call_result <- f value0 value1 +.decl Call(call_result:Variable, f:Function) +.decl CallArgument(call_result:Variable, i:number, value:Variable) + +// bind pattern +// example: node@(Ctag param0 param1) <- pure input_value +.decl NodePattern(node:Variable, t:Tag, input_value:Variable) +.decl NodeParameter(node:Variable, i:number, parameter:Variable) + +// function +// example: f param0 param1 = ... +.decl FunctionParameter(f:Function, i:number, parameter:Variable) + +// case + alt +// example: +// case_result <- case scrut of +// alt_value@(Ctag param0 param1) -> basic_block_name arg0 arg1 +.decl Case(case_result:Variable, scrutinee:Variable) +.decl Alt(case_result:Variable, alt_value:Variable, t:Tag) +.decl AltParameter(case_result:Variable, t:Tag, i:number, parameter:Variable) +.decl AltLiteral(case_result:Variable, alt_value:Variable, st:SimpleType, l:Literal) +.decl AltDefault(case_result:Variable, alt_value:Variable) + +// pure a.k.a. return value +// example: pure value +.decl ReturnValue(n:CodeName, value:Variable) + +// instruction ordering +.decl FirstInst(n:CodeName, result:Variable) +.decl NextInst(prev:Variable, next:Variable) + +.decl EntryPoint(n:CodeName) + +.input External +.input ExternalParam +.input Move +.input LitAssign +.input Node +.input NodeArgument +.input Fetch +.input Store +.input Update +.input Call +.input CallArgument +.input NodePattern +.input NodeParameter +.input FunctionParameter +.input Case +.input Alt +.input AltParameter +.input AltLiteral +.input AltDefault +.input ReturnValue +.input FirstInst +.input NextInst +.input EntryPoint + +// Reachability +.decl ReachableCode(n:CodeName) +.output ReachableCode(delimiter=",") +.decl CodeNameInst(n:CodeName, v:Variable) +.output CodeNameInst(delimiter=",") + +CodeNameInst(n, v) :- + FirstInst(n, v). +CodeNameInst(n, v) :- + CodeNameInst(n, v0), + NextInst(v0, v). + +ReachableCode(n) :- + EntryPoint(n). +ReachableCode(n) :- + ReachableCode(n0), + CodeNameInst(n0, v), + Call(v, n). + +.decl ReachableInst(v:Variable) + +ReachableInst(v) :- + ReachableCode(n), + CodeNameInst(n, v). + +.decl VarPointsTo(v:Variable, target:Variable) +.output VarPointsTo(delimiter=",") + +VarPointsTo(v,t) :- + Store(v, t), + ReachableInst(v). + +VarPointsTo(v,t) :- + Move(v, v0), + ReachableInst(v), + VarPointsTo(v0, t). + +VarPointsTo(v,t) :- + Update(r, v, t), + ReachableInst(r). + +VarPointsTo(v,t) :- + FunctionParameter(_, i, v), + CallArgument(r, i, v0), + VarPointsTo(v0, t), + ReachableInst(r). + +// Value Computation +.decl Value(v:Variable, value:Variable) +.output Value(delimiter=",") + +.decl Heap(orig:Variable, item:Variable) +.output Heap(delimiter=",") + +Heap(v,i) :- Store(v,i). + +// HPT: update +Heap(heap_orig, sv) :- + Update(_, heap, sv), + Value(heap, heap_orig), + Heap(heap_orig, _), + SharedLocation(heap). + +Value(n,n) :- + LitAssign(n,_,_). + +Value(n, n) :- + Node(n, _). + +Value(v, v) :- + Store(v, _). + +Value(v,v) :- + Update(v,_,_). + +Value(v,v) :- + External(f,_,_), + Call(v,f). + +Value(v, n) :- + Node(n, _), + Move(v, n). + +Value(v1,v2) :- + FunctionParameter(_,_,p), + Value(v1,p), + Value(p,v2). + +// HPT: fetch +Value(v, item_origin) :- + Fetch(v, heap), + Value(heap, heap_orig), + Heap(heap_orig, item), + Value(item, item_origin). + +// fun param +Value(p, val) :- + CallArgument(r, i, a), + Call(r, f), + FunctionParameter(f, i, p), + Value(a, val). + +// fun return +Value(r, val) :- + Call(r, f), + ReturnValue(f, v), + Value(v, val). + +// Node parameter matching node value created somewhere +Value(param, argval) :- + NodePattern(v, tag, n), + NodeParameter(v, i, param), + Value(n, nval), + Node(nval, tag), + NodeArgument(nval, i, arg), + Value(arg, argval). + +// Alt value when matched on tag. +Value(alt_val, scrut_val) :- + Case(case_result, scrut), + AltLiteral(case_result, alt_val, _, _), + Value(scrut, scrut_val). + +// Alt value when matched on tag +Value(alt_val, scrut_val) :- + Case(case_result, scrut), + Alt(case_result, alt_val, tag), + Value(scrut, scrut_val), + Node(scrut_val, tag). + +// Value of alt parameter when matched on tag +Value(parameter, val) :- + Case(case_res, scrut), + Alt(case_res, _alt_value, tag), + AltParameter(case_res, tag, i, parameter), + Value(scrut, scrut_val), + Node(scrut_val,tag), + NodeArgument(scrut_val,i,val). + +// Result of case/alt when matched on a node. +Value(case_result, val) :- + Case(case_result, _), + Alt(case_result, alt_value, _), + ReturnValue(alt_value, v), + Value(v, val). + +// Result of case/alt when matched on a literal. +Value(case_result, val) :- + Case(case_result, _), + AltLiteral(case_result, alt_value, _, _), + ReturnValue(alt_value, v), + Value(v, val). + +// Result of case/alt when matched on the default alternative. +Value(case_result, val) :- + Case(case_result, _), + AltDefault(case_result, alt_value), + ReturnValue(alt_value, v), + Value(v, val). + +// Type Env + +.type NodeParamType = Variable | SimpleType +.decl AbstractLocation(n: Variable) +.decl VariableSimpleType(n: Variable, st:SimpleType) +.decl VariableAbstractLocation(n:Variable, loc:Variable) +.decl VariableNodeTag(n:Variable, t:Tag) +.decl VariableNodeParamType(n: Variable, t:Tag, i:number, nt:NodeParamType) + +.output AbstractLocation(delimiter=",") +AbstractLocation(n) :- Heap(n,_). + +.output VariableSimpleType(delimiter=",") +VariableSimpleType(n,st) :- LitAssign(n,st,_). +VariableSimpleType(n,"Unit") :- Update(n,_,_). +VariableSimpleType(n,st) :- External(f,_,st), Call(n,f). +VariableSimpleType(n,st) :- ExternalParam(f,i,st), Call(r,f), CallArgument(r,i,n). +VariableSimpleType(n,st) :- Value(n,r), VariableSimpleType(r,st). + +.output VariableNodeParamType(delimiter=",") +VariableNodeParamType(n,t,i,al) + :- Node(n,t), NodeArgument(n,i,arg), Value(arg,al), AbstractLocation(al). +VariableNodeParamType(n,t,i,st) + :- Node(n,t), NodeArgument(n,i,arg), Value(arg,v), VariableSimpleType(v,st). +VariableNodeParamType(n,t,i,ty) + :- Value(n,n0), VariableNodeParamType(n0,t,i,ty). + +.output VariableNodeTag(delimiter=",") +VariableNodeTag(n,t) :- Value(n,r), Node(r,t). + +.output VariableAbstractLocation(delimiter=",") +VariableAbstractLocation(n,n) :- AbstractLocation(n). +VariableAbstractLocation(n,v) :- Value(n,v), AbstractLocation(v). + +.decl FunName(f: Function) +.output FunName(delimiter=",") + +.decl FunReturn(f:Function, n:Variable) +.output FunReturn(delimiter=",") + +.decl FunParam(f:Function, i:number, n:Variable) +.output FunParam(delimiter=",") + +FunName("main"). +FunName(f) :- Call(_,f), ReachableCode(f). + +FunReturn(f,n) :- FunName(f), ReturnValue(f,n). +FunReturn(f,n) :- External(f,_,_), Call(n,f). + +FunParam(f,i,p) :- FunctionParameter(f,i,p). +FunParam(f,i,p) :- ExternalParam(f,i,_), Call(r,f), CallArgument(r,i,p). + +/* If a concrete instance of the abstract location may be subject to a fetch more than once, */ +.decl SharedLocation(n:Variable) +.output SharedLocation(delimiter=",") + +SharedLocation(l) :- + AbstractLocation(l), Value(v,l), NonLinearVar(v). + +// For non-linear variables +// A location may only become shared if it is a possible value of a nonlinear variable. +// + +.decl AfterInst(b:Variable,a:Variable) +.output AfterInst(delimiter=",") + +AfterInst(b,a) :- NextInst(b,a). +AfterInst(b,c) :- AfterInst(b,a), NextInst(a,c). + +.decl NonLinearVar(v:Variable) +.output NonLinearVar(delimiter=",") + +// Variable used in different use cases. +// CA F M NP RV +// CallArgument CA -- - x xx xx +// Move M -- - - xx xx +// NodeParameter NP -- - - -- xx +// ReturnValue RV -- - - -- -- + +NonLinearVar(n) :- CallArgument(f,_,n), CallArgument(g,_,n), !(f=g). +NonLinearVar(n) :- CallArgument(_,i,n), CallArgument(_,j,n), !(i=j). +NonLinearVar(n) :- CallArgument(_,_,n), Move(_,n). +NonLinearVar(n) :- CallArgument(_,_,n), NodeArgument(_,_,n). +NonLinearVar(n) :- CallArgument(_,_,n), ReturnValue(_,n). +NonLinearVar(n) :- Fetch(r,n), Fetch(q,n), !(r=q). +NonLinearVar(n) :- Update(_,v0,n), Fetch(_,v1), AfterInst(v0,v1). +NonLinearVar(n) :- Move(_,n), NodeArgument(_,_,n). +NonLinearVar(n) :- Move(_,n), ReturnValue(_,n). +NonLinearVar(n) :- NodeParameter(_,_,n), ReturnValue(_,n). diff --git a/grin/app/CLI/Lib.hs b/grin/app/CLI/Lib.hs index 7491aa40..929adebb 100644 --- a/grin/app/CLI/Lib.hs +++ b/grin/app/CLI/Lib.hs @@ -134,6 +134,7 @@ pipelineOpts = <|> (T <$> transformOpts) <|> flg ConfluenceTest "confluence-test" "Checks transformation confluence by generating random two pipelines which reaches the fix points." <|> flg PrintErrors "print-errors" "Prints the error log" + <|> flg DatalogHPT "datalog-hpt" "Run HPT in souffle" maybeRenderingOpt :: String -> Maybe RenderingOption diff --git a/grin/grin.cabal b/grin/grin.cabal index 788c1272..5b082013 100644 --- a/grin/grin.cabal +++ b/grin/grin.cabal @@ -151,6 +151,7 @@ library Transformations.ExtendedSyntax.Optimising.CSE Transformations.ExtendedSyntax.Optimising.EvaluatedCaseElimination Transformations.ExtendedSyntax.Optimising.TrivialCaseElimination + Transformations.ExtendedSyntax.Normalisation Transformations.BindNormalisation Transformations.CountVariableUse diff --git a/grin/src/Grin/ExtendedSyntax/Datalog.hs b/grin/src/Grin/ExtendedSyntax/Datalog.hs index 78b202cd..96bcce95 100644 --- a/grin/src/Grin/ExtendedSyntax/Datalog.hs +++ b/grin/src/Grin/ExtendedSyntax/Datalog.hs @@ -3,23 +3,39 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TypeApplications #-} module Grin.ExtendedSyntax.Datalog where -import Control.Monad (forM_) +import Control.Monad (forM, forM_, void) import Data.Int import Language.Souffle.Interpreted as Souffle import GHC.Generics import Control.Monad.Trans import Control.Monad.Trans.Reader import Data.Text (Text) +import Data.Functor.Foldable +import Control.Comonad (extract) +import Control.Comonad.Cofree +import Data.Maybe (catMaybes, mapMaybe) +import Data.Proxy + import qualified Grin.ExtendedSyntax.Syntax as Grin import qualified Data.Text as Text +{- +TODO: +[ ] Handle As patterns +[x] Generate code that always have a single return value (In normalisation) +[ ] Add Datalog program to the resources +-} + data HPT = HPT instance Souffle.Program HPT where type ProgramFacts HPT = - '[ External + '[ EntryPoint + , External , ExternalParam , Move , LitAssign @@ -44,21 +60,26 @@ instance Souffle.Program HPT where ] programName = const "hpt" -type Function = Text -type Boolean = Int32 -type SimpleType = Text -type Number = Int32 -type Variable = Text -type Literal = Text -type Tag = Text -- TODO: TagType? -type CodeName = Text +type Function = Text +type Boolean = Int32 +type SimpleType = Text +type Number = Int32 +type Variable = Text +type Literal = Text +type Tag = Text +type CodeName = Text +type ExternalKind = Text + +mkBoolean :: Bool -> Boolean +mkBoolean = \case + False -> 0 + True -> 1 --instance Souffle.Marshal Grin.Name where -- push (Grin.NM n) = push n -- pop = Grin.NM <$> pop -data External = External !Function !Boolean !SimpleType deriving (Eq, Show, Generic) -data ExternalParam = ExternalParam !Function !Number !SimpleType deriving (Eq, Show, Generic) +data EntryPoint = EntryPoint !CodeName deriving (Eq, Show, Generic) data Move = Move !Variable !Variable deriving (Eq, Show, Generic) data LitAssign = LitAssign !Variable !SimpleType !Literal deriving (Eq, Show, Generic) data Node = Node !Variable !Tag deriving (Eq, Show, Generic) @@ -72,14 +93,17 @@ data NodePattern = NodePattern !Variable !Tag !Variable data NodeParameter = NodeParameter !Variable !Number !Variable deriving (Eq, Show, Generic) data Case = Case !Variable !Variable deriving (Eq, Show, Generic) data Alt = Alt !Variable !Variable !Tag deriving (Eq, Show, Generic) -data AltLiteral = AltLiteral !Variable !Variable !Literal deriving (Eq, Show, Generic) +data AltLiteral = AltLiteral !Variable !Variable !SimpleType !Literal deriving (Eq, Show, Generic) data AltDefault = AltDefault !Variable !Variable deriving (Eq, Show, Generic) data ReturnValue = ReturnValue !CodeName !Variable deriving (Eq, Show, Generic) data FirstInst = FirstInst !CodeName !Variable deriving (Eq, Show, Generic) data NextInst = NextInst !Variable !Variable deriving (Eq, Show, Generic) data FunctionParameter = FunctionParameter !Function !Number !Variable deriving (Eq, Show, Generic) -data AltParameter = AltParameter !Variable !Tag !Number {-!Variable-} deriving (Eq, Show, Generic) +data AltParameter = AltParameter !Variable !Tag !Number !Variable deriving (Eq, Show, Generic) +data External = External !Function !Boolean !SimpleType !ExternalKind deriving (Eq, Show, Generic) +data ExternalParam = ExternalParam !Function !Number !SimpleType deriving (Eq, Show, Generic) +instance Souffle.Marshal EntryPoint instance Souffle.Marshal External instance Souffle.Marshal ExternalParam instance Souffle.Marshal Move @@ -103,47 +127,49 @@ instance Souffle.Marshal NextInst instance Souffle.Marshal FunctionParameter instance Souffle.Marshal AltParameter -instance Souffle.Fact External where factName = const "external" -instance Souffle.Fact ExternalParam where factName = const "externalparam" -instance Souffle.Fact Move where factName = const "move" -instance Souffle.Fact LitAssign where factName = const "litassign" -instance Souffle.Fact Node where factName = const "node" -instance Souffle.Fact NodeArgument where factName = const "nodeargument" -instance Souffle.Fact Fetch where factName = const "fetch" -instance Souffle.Fact Store where factName = const "store" -instance Souffle.Fact Update where factName = const "update" -instance Souffle.Fact Call where factName = const "call" -instance Souffle.Fact CallArgument where factName = const "callargument" -instance Souffle.Fact NodePattern where factName = const "nodepattern" -instance Souffle.Fact NodeParameter where factName = const "nodeparameter" -instance Souffle.Fact Case where factName = const "case" -instance Souffle.Fact Alt where factName = const "alt" -instance Souffle.Fact AltLiteral where factName = const "altliteral" -instance Souffle.Fact AltDefault where factName = const "altdefault" -instance Souffle.Fact ReturnValue where factName = const "returnvalue" -instance Souffle.Fact FirstInst where factName = const "firstinst" -instance Souffle.Fact NextInst where factName = const "nextinst" -instance Souffle.Fact FunctionParameter where factName = const "functionparameter" -instance Souffle.Fact AltParameter where factName = const "altparameter" - - -gtagToDtag :: Grin.Tag -> Tag -gtagToDtag (Grin.Tag tt name) = (renderTagType tt) <> Grin.nameText name - where - renderTagType :: Grin.TagType -> Text - renderTagType Grin.C = "C" - renderTagType Grin.F = "F" - renderTagType (Grin.P m) = "P-" <> Text.pack (show m) <> "-" +instance Souffle.Fact EntryPoint where factName = const "EntryPoint" +instance Souffle.Fact External where factName = const "External" +instance Souffle.Fact ExternalParam where factName = const "ExternalParam" +instance Souffle.Fact Move where factName = const "Move" +instance Souffle.Fact LitAssign where factName = const "LitAssign" +instance Souffle.Fact Node where factName = const "Node" +instance Souffle.Fact NodeArgument where factName = const "NodeArgument" +instance Souffle.Fact Fetch where factName = const "Fetch" +instance Souffle.Fact Store where factName = const "Store" +instance Souffle.Fact Update where factName = const "Update" +instance Souffle.Fact Call where factName = const "Call" +instance Souffle.Fact CallArgument where factName = const "CallArgument" +instance Souffle.Fact NodePattern where factName = const "NodePattern" +instance Souffle.Fact NodeParameter where factName = const "NodeParameter" +instance Souffle.Fact Case where factName = const "Case" +instance Souffle.Fact Alt where factName = const "Alt" +instance Souffle.Fact AltLiteral where factName = const "AltLiteral" +instance Souffle.Fact AltDefault where factName = const "AltDefault" +instance Souffle.Fact ReturnValue where factName = const "ReturnValue" +instance Souffle.Fact FirstInst where factName = const "FirstInst" +instance Souffle.Fact NextInst where factName = const "NextInst" +instance Souffle.Fact FunctionParameter where factName = const "FunctionParameter" +instance Souffle.Fact AltParameter where factName = const "AltParameter" --- type Souffle a = ReaderT (Handle HPT) SouffleM a +data HPTResult = HPTResult -convertExternals :: [Grin.External] -> SouffleM () -convertExternals = undefined +renderDatalog :: Grin.Exp -> IO (Maybe HPTResult) +renderDatalog exp = do + let cfg = Souffle.Config "./datalog/hpt/" (Just "souffle") + Souffle.runSouffleWith cfg $ do + mprog <- Souffle.init HPT + forM mprog $ \prog -> do + Souffle.addFact prog $ EntryPoint "grinMain" + para (structure prog) exp + calcReturnValues prog exp + nextInst prog exp + Souffle.run prog + pure Nothing -emitAlg :: Handle HPT -> Grin.ExpF (Grin.Exp, SouffleM ()) -> SouffleM () -emitAlg prog = \case +structure :: Handle HPT -> Grin.ExpF (Grin.Exp, SouffleM ()) -> SouffleM () +structure prog = \case Grin.ProgramF externals defs -> do - convertExternals externals + convertExternals prog externals mapM_ snd defs -- f param0 param1 = ... @@ -164,7 +190,7 @@ emitAlg prog = \case -- .decl LitAssign(result:Variable, l:Literal) Grin.EBindF (Grin.SReturn (Grin.Lit l), lhs) (Grin.VarPat res) (_, rhs) -> do lhs - Souffle.addFact prog $ litAssignFact res l + Souffle.addFact prog $ uncurry (LitAssign (Grin.nameText res)) $ literalParams l rhs -- result_node <- pure (Ctag item0 item1) @@ -242,26 +268,125 @@ emitAlg prog = \case Souffle.addFact prog $ Alt (Grin.nameText cs_res) (Grin.nameText n) (gtagToDtag tag) Souffle.addFacts prog $ zipWith - (\j a -> AltParameter (Grin.nameText cs_res) (gtagToDtag tag) j {-(Grin.nameText a)-}) + (\j a -> AltParameter (Grin.nameText cs_res) (gtagToDtag tag) j (Grin.nameText a)) [0..] args -- TODO: Handle literals better - -- Grin.Alt (Grin.LitPat (G.SInt64 i)) n _ -> - -- [ AltLiteral - -- { case_result = Variable cs_res - -- , alt_value = Variable n - -- , l = Literal (show i) - -- } - -- ] + Grin.Alt (Grin.LitPat l) n _ -> do + let (st, lt) = literalParams l + Souffle.addFact prog $ AltLiteral (Grin.nameText cs_res) (Grin.nameText n) st lt Grin.Alt Grin.DefaultPat n _ -> do Souffle.addFact prog $ AltDefault (Grin.nameText cs_res) (Grin.nameText n) - rhs -litAssignFact :: Grin.Name -> Grin.Lit -> LitAssign -litAssignFact v sv = (\(ty, value) -> LitAssign (Grin.nameText v) ty value) $ case sv of + other -> void $ traverse snd other + +-- * Return values + +-- TODO: Make this monadic +calcReturnValues :: Handle HPT -> Grin.Exp -> SouffleM () +calcReturnValues prog = snd . histo (returnValueAlg prog) + +returnValueAlg + :: Handle HPT + -> Grin.ExpF (Cofree Grin.ExpF (Maybe Grin.Name, SouffleM ())) + -> (Maybe Grin.Name, SouffleM ()) +returnValueAlg prog = \case + Grin.SReturnF (Grin.Var name) -> (Just name, pure ()) + Grin.SReturnF val -> (Nothing, pure ()) + Grin.EBindF ((_, lhs) :< Grin.ECaseF _ alts) (Grin.VarPat v) (extract -> (returnValue, rhs)) + -> let altReturnValues = mapMaybe (fst . extract) alts + in ( returnValue + , do lhs + Souffle.addFacts prog + $ map (\r -> NextInst (Grin.nameText r) (Grin.nameText v)) altReturnValues + rhs + ) + Grin.EBindF (extract -> (_, lhs)) _ (extract -> (returnValue, rhs)) + -> (returnValue, lhs >> rhs) + Grin.AltF _ codeName (extract -> (Just returnValue, body)) -> + ( Just returnValue + , do Souffle.addFact prog $ ReturnValue (Grin.nameText codeName) (Grin.nameText returnValue) + body + ) + Grin.DefF codeName _ (extract -> (Just returnValue, body)) -> + ( Nothing + , do Souffle.addFact prog $ ReturnValue (Grin.nameText codeName) (Grin.nameText returnValue) + body + ) + rest -> + ( Nothing + , void $ traverse (snd . extract) rest + ) + +nextInst :: Handle HPT -> Grin.Exp -> SouffleM () +nextInst prog = void . para (nextInstAlg prog) + +-- | The next instrument makes a chain of variable associations, between binds +nextInstAlg :: Handle HPT -> Grin.ExpF (Grin.Exp, SouffleM (Maybe Grin.Name)) -> SouffleM (Maybe Grin.Name) +nextInstAlg prog = \case + Grin.DefF codeName _ (Grin.EBind _ (Grin.VarPat v) _, body) -> do + Souffle.addFact prog $ FirstInst (Grin.nameText codeName) (Grin.nameText v) + void body + pure Nothing + Grin.AltF _ n (Grin.EBind _ (Grin.VarPat v) _, body) -> do + Souffle.addFact prog $ NextInst (Grin.nameText n) (Grin.nameText v) + void body + pure $ Just n + Grin.ECaseF v alts -> do + nis <- catMaybes <$> mapM snd alts + Souffle.addFacts prog $ + map (\ni -> NextInst (Grin.nameText v) (Grin.nameText ni)) nis + pure Nothing + Grin.EBindF (elhs, lhs) (Grin.VarPat v) (_, rhs) -> do + void lhs + mni <- rhs + forM_ mni $ \ni -> do + Souffle.addFact prog $ NextInst (Grin.nameText v) (Grin.nameText ni) + pure $ case elhs of + Grin.ECase{} -> Nothing + _ -> Just v + rest -> do + mapM_ snd rest + pure Nothing + +-- * Externals + +convertExternals :: Handle HPT -> [Grin.External] -> SouffleM () +convertExternals prog externals = forM_ externals $ + \(Grin.External n rt pts e k) -> do + Souffle.addFact prog $ + External (Grin.nameText n) (mkBoolean e) (asDatalogSimpleType rt) (externalKind k) + Souffle.addFacts prog $ + zipWith + (\j t -> ExternalParam (Grin.nameText n) j (asDatalogSimpleType t)) + [0..] + pts + where + asDatalogSimpleType :: Grin.Ty -> SimpleType + asDatalogSimpleType = \case + Grin.TySimple st -> stToDatalogST st + _ -> error "asDatalogSimpleType: None handled" + +externalKind :: Grin.ExternalKind -> ExternalKind +externalKind = \case + Grin.PrimOp -> "primop" + Grin.FFI -> "ffi" + +-- * Helpers + +gtagToDtag :: Grin.Tag -> Tag +gtagToDtag (Grin.Tag tt name) = (renderTagType tt) <> Grin.nameText name + where + renderTagType :: Grin.TagType -> Text + renderTagType Grin.C = "C" + renderTagType Grin.F = "F" + renderTagType (Grin.P m) = "P-" <> Text.pack (show m) <> "-" + +literalParams :: Grin.Lit -> (SimpleType, Literal) +literalParams sv = case sv of Grin.LInt64 i -> (stToDatalogST Grin.T_Int64, Text.pack $ show i) Grin.LWord64 w -> (stToDatalogST Grin.T_Word64, Text.pack $ show w) Grin.LFloat f -> (stToDatalogST Grin.T_Float, Text.pack $ show f) diff --git a/grin/src/Pipeline/Pipeline.hs b/grin/src/Pipeline/Pipeline.hs index aab604b5..836ee3fe 100644 --- a/grin/src/Pipeline/Pipeline.hs +++ b/grin/src/Pipeline/Pipeline.hs @@ -100,7 +100,7 @@ import Control.Monad.Trans.State.Strict hiding (gets) import Control.Monad.IO.Class import Lens.Micro.TH import Lens.Micro.Mtl -import System.FilePath +import System.FilePath hiding (normalise) import System.Exit import Control.DeepSeq import Debug.Trace @@ -122,6 +122,13 @@ import qualified Data.ByteString.Lazy as LBS import Reducer.PrimOps (evalPrimOp) import Reducer.Pure (EvalPlugin(..)) +import qualified Grin.ExtendedSyntax.Syntax as SyntaxV2 +import qualified Transformations.ExtendedSyntax.Conversion as SyntaxV2 (convertToNew) +import qualified Grin.ExtendedSyntax.Pretty as SyntaxV2 +import qualified Grin.ExtendedSyntax.Datalog as Datalog +import Transformations.ExtendedSyntax.Normalisation (normalise) + + data Transformation -- Simplifying = RegisterIntroduction @@ -215,6 +222,7 @@ data PipelineStep | ConfluenceTest | PrintErrors | DebugPipelineState + | DatalogHPT deriving (Eq, Show) pattern DeadCodeElimination :: PipelineStep @@ -480,6 +488,7 @@ pipelineStep p = do DebugPipelineState -> debugPipelineState PureEval showStatistics -> pureEval (EvalPlugin evalPrimOp) showStatistics PureEvalPlugin evalPlugin showStatistics -> pureEval evalPlugin showStatistics + DatalogHPT -> datalogHPT after <- use psExp let eff = if before == after then None else ExpChanged showMS :: Rational -> String @@ -785,6 +794,14 @@ lintGrin mPhaseName = do liftIO $ die "illegal code" pure () +datalogHPT :: PipelineM () +datalogHPT = do + exp <- use psExp + let expV2 = normalise $ SyntaxV2.convertToNew exp + liftIO $ SyntaxV2.printGrin expV2 + liftIO $ Datalog.renderDatalog expV2 + pure () + -- confluence testing randomPipeline :: StdGen -> PipelineOpts -> Exp -> IO Exp diff --git a/grin/src/Transformations/ExtendedSyntax/Normalisation.hs b/grin/src/Transformations/ExtendedSyntax/Normalisation.hs new file mode 100644 index 00000000..988ae667 --- /dev/null +++ b/grin/src/Transformations/ExtendedSyntax/Normalisation.hs @@ -0,0 +1,64 @@ +--A normalised AST is +-- * Bind normalised +-- * The last statement of the function is pure v +-- * Node patterns only appear only when the lhs of the bind +-- is pure. + +{-# LANGUAGE LambdaCase #-} +module Transformations.ExtendedSyntax.Normalisation where + +import Data.Functor.Foldable +import Transformations.Util +import Grin.ExtendedSyntax.Syntax +import Transformations.ExtendedSyntax.BindNormalisation +import Transformations.ExtendedSyntax.Names + + + +normalise :: Exp -> Exp +normalise e = fst $ evalNameM e $ do + e1 <- restoreNodePattern $ bindNormalisation e + restorePureAsLast e1 + +restorePureAsLast :: Exp -> NameM Exp +restorePureAsLast = apoM $ \case + -- v <- lhs + -- pure v + EBind lhs pat (SReturn (Var v)) -> + pure $ EBindF (Right lhs) pat (Left (SReturn (Var v))) + + -- v1 <- lhs1 + -- v2 <- ... + EBind lhs pat rhs@(EBind{}) -> + pure $ EBindF (Right lhs) pat (Right rhs) + + -- v <- lhs + -- pure val / case / store / update / fetch / call + EBind lhs pat rhs -> do + x <- deriveNewName "rapl" + -- v <- lhs + -- x <- other + -- pure x + pure $ EBindF (Right lhs) pat (Left (EBind rhs (VarPat x) (SReturn (Var x)))) + + -- rrogram / def + other -> pure $ fmap Right $ project other + +restoreNodePattern :: Exp -> NameM Exp +restoreNodePattern = apoM $ \case + -- x @ (tag ps) <- pure y + -- rhs + EBind (SReturn y) x@(AsPat{}) rhs -> do + pure $ EBindF (Left (SReturn y)) x (Right rhs) + + -- v @ (tag ps) <- case / store / update / fetch / call + -- rhs + EBind lhs v@(AsPat{}) rhs -> do + x <- deriveNewName "rnp" + -- x <- case / store / update / fetch / call + -- v @ (tag ps) <- pure x + -- rhs + pure $ EBindF (Right lhs) (VarPat x) $ Right + $ EBind (SReturn (Var x)) v rhs + + other -> pure $ fmap Right $ project other diff --git a/grin/test/Transformations/ExtendedSyntax/NormalisationSpec.hs b/grin/test/Transformations/ExtendedSyntax/NormalisationSpec.hs new file mode 100644 index 00000000..1dc6b108 --- /dev/null +++ b/grin/test/Transformations/ExtendedSyntax/NormalisationSpec.hs @@ -0,0 +1,37 @@ +module Transformations.ExtendedSyntax.NormalisationSpec where + +import Test.Hspec +import Grin.ExtendedSyntax.TH +import Test.ExtendedSyntax.Assertions + + +test :: IO () +test = hspec spec + +spec :: Spec +spec = describe "Normalisation" $ do + it "works for an example" $ do + let before = [prog| + pureLast1 x = pure x + + pureLast2 x = + a <- fun1 x + store a + + pureLast3 x = + case x of + (CCons a b) -> pure a + + pureLast4 x = + y <- pure x + case y of + (CCons a b) -> pure a + + pureLast5 x = + y <- pure (CInt x) + pure y + |] + + printGrin $ normalise before + 42 `shouldBe` 42 + diff --git a/stack.yaml b/stack.yaml index e6fe3df2..9ef729ba 100644 --- a/stack.yaml +++ b/stack.yaml @@ -19,7 +19,7 @@ extra-deps: - llvm-hs - llvm-hs-pure - github: luc-tielen/souffle-haskell - commit: c76bd446c210b32e7a1de55b37a4df051586f108 + commit: bf6e419d65059274f3a32d4e81505ccadd42ff58 flags: llvm-hs: From 7f12b5e333c904675e629f76d148c339ad08f74a Mon Sep 17 00:00:00 2001 From: Andor Penzes Date: Wed, 6 May 2020 23:18:50 +0200 Subject: [PATCH 03/15] Datalog: Create HPTResult from souffle output. --- datalog/hpt/hpt.dl | 32 ++-- grin/src/Grin/ExtendedSyntax/Datalog.hs | 233 +++++++++++++++++++++++- grin/src/Pipeline/Pipeline.hs | 4 +- 3 files changed, 244 insertions(+), 25 deletions(-) diff --git a/datalog/hpt/hpt.dl b/datalog/hpt/hpt.dl index f886e619..50921a3e 100644 --- a/datalog/hpt/hpt.dl +++ b/datalog/hpt/hpt.dl @@ -91,9 +91,9 @@ // Reachability .decl ReachableCode(n:CodeName) -.output ReachableCode(delimiter=",") +// .output ReachableCode .decl CodeNameInst(n:CodeName, v:Variable) -.output CodeNameInst(delimiter=",") +// .output CodeNameInst CodeNameInst(n, v) :- FirstInst(n, v). @@ -115,7 +115,7 @@ ReachableInst(v) :- CodeNameInst(n, v). .decl VarPointsTo(v:Variable, target:Variable) -.output VarPointsTo(delimiter=",") +.output VarPointsTo VarPointsTo(v,t) :- Store(v, t), @@ -138,10 +138,10 @@ VarPointsTo(v,t) :- // Value Computation .decl Value(v:Variable, value:Variable) -.output Value(delimiter=",") +.output Value .decl Heap(orig:Variable, item:Variable) -.output Heap(delimiter=",") +.output Heap Heap(v,i) :- Store(v,i). @@ -258,17 +258,17 @@ Value(case_result, val) :- .decl VariableNodeTag(n:Variable, t:Tag) .decl VariableNodeParamType(n: Variable, t:Tag, i:number, nt:NodeParamType) -.output AbstractLocation(delimiter=",") +.output AbstractLocation AbstractLocation(n) :- Heap(n,_). -.output VariableSimpleType(delimiter=",") +.output VariableSimpleType VariableSimpleType(n,st) :- LitAssign(n,st,_). VariableSimpleType(n,"Unit") :- Update(n,_,_). VariableSimpleType(n,st) :- External(f,_,st), Call(n,f). VariableSimpleType(n,st) :- ExternalParam(f,i,st), Call(r,f), CallArgument(r,i,n). VariableSimpleType(n,st) :- Value(n,r), VariableSimpleType(r,st). -.output VariableNodeParamType(delimiter=",") +.output VariableNodeParamType VariableNodeParamType(n,t,i,al) :- Node(n,t), NodeArgument(n,i,arg), Value(arg,al), AbstractLocation(al). VariableNodeParamType(n,t,i,st) @@ -276,21 +276,21 @@ VariableNodeParamType(n,t,i,st) VariableNodeParamType(n,t,i,ty) :- Value(n,n0), VariableNodeParamType(n0,t,i,ty). -.output VariableNodeTag(delimiter=",") +.output VariableNodeTag VariableNodeTag(n,t) :- Value(n,r), Node(r,t). -.output VariableAbstractLocation(delimiter=",") +.output VariableAbstractLocation VariableAbstractLocation(n,n) :- AbstractLocation(n). VariableAbstractLocation(n,v) :- Value(n,v), AbstractLocation(v). .decl FunName(f: Function) -.output FunName(delimiter=",") +.output FunName .decl FunReturn(f:Function, n:Variable) -.output FunReturn(delimiter=",") +.output FunReturn .decl FunParam(f:Function, i:number, n:Variable) -.output FunParam(delimiter=",") +.output FunParam FunName("main"). FunName(f) :- Call(_,f), ReachableCode(f). @@ -303,7 +303,7 @@ FunParam(f,i,p) :- ExternalParam(f,i,_), Call(r,f), CallArgument(r,i,p). /* If a concrete instance of the abstract location may be subject to a fetch more than once, */ .decl SharedLocation(n:Variable) -.output SharedLocation(delimiter=",") +// .output SharedLocation SharedLocation(l) :- AbstractLocation(l), Value(v,l), NonLinearVar(v). @@ -313,13 +313,13 @@ SharedLocation(l) :- // .decl AfterInst(b:Variable,a:Variable) -.output AfterInst(delimiter=",") +// .output AfterInst AfterInst(b,a) :- NextInst(b,a). AfterInst(b,c) :- AfterInst(b,a), NextInst(a,c). .decl NonLinearVar(v:Variable) -.output NonLinearVar(delimiter=",") +// .output NonLinearVar // Variable used in different use cases. // CA F M NP RV diff --git a/grin/src/Grin/ExtendedSyntax/Datalog.hs b/grin/src/Grin/ExtendedSyntax/Datalog.hs index 96bcce95..63b89540 100644 --- a/grin/src/Grin/ExtendedSyntax/Datalog.hs +++ b/grin/src/Grin/ExtendedSyntax/Datalog.hs @@ -5,7 +5,8 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE TypeApplications #-} -module Grin.ExtendedSyntax.Datalog where +{-# LANGUAGE RecordWildCards #-} +module Grin.ExtendedSyntax.Datalog (calculateHPTResult) where import Control.Monad (forM, forM_, void) import Data.Int @@ -17,16 +18,29 @@ import Data.Text (Text) import Data.Functor.Foldable import Control.Comonad (extract) import Control.Comonad.Cofree -import Data.Maybe (catMaybes, mapMaybe) +import Data.Either (fromRight) +import Data.Maybe (catMaybes, mapMaybe, fromJust) import Data.Proxy - +import Data.Bifunctor +import Data.List (sortBy) +import Data.Function (on) +import Grin.ExtendedSyntax.Pretty +import Debug.Trace + +import qualified Data.Vector as Vector +import qualified Data.Set as Set +import qualified Data.Map.Strict as Map import qualified Grin.ExtendedSyntax.Syntax as Grin import qualified Data.Text as Text +import qualified AbstractInterpretation.ExtendedSyntax.HeapPointsTo.Result as Result + +import AbstractInterpretation.ExtendedSyntax.HeapPointsTo.Pretty () {- TODO: [ ] Handle As patterns [x] Generate code that always have a single return value (In normalisation) +[x] Create HPTResult [ ] Add Datalog program to the resources -} @@ -55,8 +69,17 @@ instance Souffle.Program HPT where , ReturnValue , FirstInst , NextInst + + , Heap , FunctionParameter , AltParameter + , AbstractLocation + , VariableAbstractLocation + , VariableSimpleType + , VariableNodeTag + , VariableNodeParamType + , FunParam + , FunReturn ] programName = const "hpt" @@ -69,6 +92,7 @@ type Literal = Text type Tag = Text type CodeName = Text type ExternalKind = Text +type Loc = Text mkBoolean :: Bool -> Boolean mkBoolean = \case @@ -103,6 +127,15 @@ data AltParameter = AltParameter !Variable !Tag !Number !Variable data External = External !Function !Boolean !SimpleType !ExternalKind deriving (Eq, Show, Generic) data ExternalParam = ExternalParam !Function !Number !SimpleType deriving (Eq, Show, Generic) +data Heap = Heap !Variable !Variable deriving (Eq, Show, Generic) +data AbstractLocation = AbstractLocation !Loc deriving (Eq, Show, Generic) +data VariableSimpleType = VariableSimpleType !Variable !SimpleType deriving (Eq, Show, Generic) +data VariableNodeTag = VariableNodeTag !Variable !Tag deriving (Eq, Show, Generic) +data VariableNodeParamType = VariableNodeParamType !Variable !Tag !Int32 !SimpleType deriving (Eq, Show, Generic) +data VariableAbstractLocation = VariableAbstractLocation !Variable !Loc deriving (Eq, Show, Generic) +data FunParam = FunParam !Function !Int32 !Variable deriving (Eq, Show, Generic) +data FunReturn = FunReturn !Function !Variable deriving (Eq, Show, Generic) + instance Souffle.Marshal EntryPoint instance Souffle.Marshal External instance Souffle.Marshal ExternalParam @@ -127,6 +160,15 @@ instance Souffle.Marshal NextInst instance Souffle.Marshal FunctionParameter instance Souffle.Marshal AltParameter +instance Souffle.Marshal Heap +instance Souffle.Marshal AbstractLocation +instance Souffle.Marshal VariableAbstractLocation +instance Souffle.Marshal VariableSimpleType +instance Souffle.Marshal VariableNodeTag +instance Souffle.Marshal VariableNodeParamType +instance Souffle.Marshal FunParam +instance Souffle.Marshal FunReturn + instance Souffle.Fact EntryPoint where factName = const "EntryPoint" instance Souffle.Fact External where factName = const "External" instance Souffle.Fact ExternalParam where factName = const "ExternalParam" @@ -151,10 +193,19 @@ instance Souffle.Fact NextInst where factName = const "NextInst" instance Souffle.Fact FunctionParameter where factName = const "FunctionParameter" instance Souffle.Fact AltParameter where factName = const "AltParameter" -data HPTResult = HPTResult +instance Souffle.Fact Heap where factName = const "Heap" +instance Souffle.Fact VariableSimpleType where factName = const "VariableSimpleType" +instance Souffle.Fact AbstractLocation where factName = const "AbstractLocation" +instance Souffle.Fact VariableAbstractLocation where factName = const "VariableAbstractLocation" +instance Souffle.Fact VariableNodeTag where factName = const "VariableNodeTag" +instance Souffle.Fact VariableNodeParamType where factName = const "VariableNodeParamType" +instance Souffle.Fact FunParam where factName = const "FunParam" +instance Souffle.Fact FunReturn where factName = const "FunReturn" + + -renderDatalog :: Grin.Exp -> IO (Maybe HPTResult) -renderDatalog exp = do +calculateHPTResult :: Grin.Exp -> IO (Maybe Result.HPTResult) +calculateHPTResult exp = do let cfg = Souffle.Config "./datalog/hpt/" (Just "souffle") Souffle.runSouffleWith cfg $ do mprog <- Souffle.init HPT @@ -164,7 +215,18 @@ renderDatalog exp = do calcReturnValues prog exp nextInst prog exp Souffle.run prog - pure Nothing + r <- ResultData + <$> Souffle.getFacts prog -- abstract location + <*> Souffle.getFacts prog -- value abstract location + <*> Souffle.getFacts prog -- variable simple type + <*> Souffle.getFacts prog -- resultVariableNodeTag + <*> Souffle.getFacts prog -- resultVariableNodeParamType + <*> Souffle.getFacts prog -- resultFunReturn + <*> Souffle.getFacts prog -- resultFunParam + <*> Souffle.getFacts prog -- heap + let res = calcHPTResult r + liftIO $ putStrLn $ showWide $ pretty res + pure res structure :: Handle HPT -> Grin.ExpF (Grin.Exp, SouffleM ()) -> SouffleM () structure prog = \case @@ -375,6 +437,133 @@ externalKind = \case Grin.PrimOp -> "primop" Grin.FFI -> "ffi" +-- * Convert to HPTResult + +data ResultData = ResultData + { resultAbstractLocations :: [AbstractLocation] + , resultValueAbstractLocation :: [VariableAbstractLocation] + , resultVariableSimpleType :: [VariableSimpleType] + , resultVariableNodeTag :: [VariableNodeTag] + , resultVariableNodeParamType :: [VariableNodeParamType] + , resultFunReturn :: [FunReturn] + , resultFunParam :: [FunParam] + , resultHeap :: [Heap] + } deriving (Eq, Show) + +abstractLocationMap :: [AbstractLocation] -> (Map.Map Text Int, Map.Map Int Text) +abstractLocationMap as = (ti, it) + where + (ti,it) = bimap Map.fromList Map.fromList + $ unzip + $ zipWith (\(AbstractLocation l) n -> ((l,n), (n,l))) as [0..] + +variableNodeMap + :: [VariableNodeTag] + -> [VariableNodeParamType] + -> Map.Map Text [(Tag, [Set.Set SimpleType])] +variableNodeMap ns ps = Map.unionsWith (++) + [ Map.singleton n [(t,ts)] + | VariableNodeTag n t <- ns + , let ps0 = Map.unionsWith mappend + $ mapMaybe (\(VariableNodeParamType n0 t0 i s) + -> if n == n0 && t == t0 + then Just $ Map.singleton i (Set.singleton s) + else Nothing) ps + , let ts = case unzip $ Map.toList ps0 of + (as, es) | as == [0 .. fromIntegral (length as - 1)] -> es + _ -> error $ "in positions: " ++ show ps0 + ] + +functionNameMap + :: [FunParam] + -> [FunReturn] + -> Map.Map Grin.Name Result.TypeSet + -> Map.Map Grin.Name (Result.TypeSet, Vector.Vector Result.TypeSet) +functionNameMap ps rs vars = Map.fromList + [ (Grin.mkName fun, (ret, params)) + | FunReturn fun ret0 <- rs + , let ps0 = Map.unionsWith mappend + $ mapMaybe + (\(FunParam f i p) + -> if f == fun + then Map.singleton i <$> Map.lookup (Grin.mkName p) vars + else Nothing) + ps + , let params = case unzip $ Map.toList ps0 of + (as,es) | as == [0 .. fromIntegral (length as - 1)] -> Vector.fromList es + _ -> error $ "functionMap: in positions: " ++ show (fun, ret0, ps0) + , let ret = fromJust $ Map.lookup (Grin.mkName ret0) vars + ] + +heapMap + :: [Heap] + -> Map.Map Text Int + -> Map.Map Grin.Name Result.TypeSet + -> Vector.Vector Result.NodeSet +heapMap hs nameToLoc vars = Vector.generate (Map.size nameToLoc) (fromJust . flip Map.lookup heapVals) + where + heapVals = Map.unionsWith mappend + [ Map.singleton loc nodeSet + | Heap ln t <- hs + , let Just loc = Map.lookup ln nameToLoc + , let Just (Result.TypeSet _ nodeSet) = Map.lookup (Grin.mkName t) vars + ] + +calcHPTResult :: ResultData -> Result.HPTResult +calcHPTResult (ResultData{..}) = Result.HPTResult memory register function + where + (nameToLoc, locToName) = abstractLocationMap resultAbstractLocations + nodeTags = Map.toList $ variableNodeMap resultVariableNodeTag resultVariableNodeParamType + memory = heapMap resultHeap nameToLoc register + register = Map.unionsWith (<>) + ( map (\(VariableSimpleType n t) + -> Map.singleton (Grin.mkName n) + (toTypeSet $ either (error . show) id $ datalogStToSt t)) + resultVariableSimpleType + ++ + map (\(VariableAbstractLocation n l) + -> case Map.lookup n nameToLoc of + Nothing -> mempty + Just l -> Map.singleton + (Grin.mkName n) + (Result.TypeSet + (Set.singleton (Result.T_Location l)) + mempty)) + resultValueAbstractLocation + ++ + concatMap + (\(n, ps) + -> map (\(tag, types) + -> Map.singleton + (Grin.mkName n) + (Result.TypeSet mempty + (Result.NodeSet (Map.singleton + (dtagToGtag tag) + (Vector.fromList $ map + (Set.map + (either + (Result.T_Location . fromJust . flip Map.lookup nameToLoc) + id . datalogStToRSt)) + types)))) + ) ps) + nodeTags + ) + + function = functionNameMap resultFunParam resultFunReturn register + +class ToTypeSet t where + toTypeSet :: t -> Result.TypeSet + +instance ToTypeSet Grin.SimpleType where + toTypeSet = \case + Grin.T_Int64 -> Result.TypeSet (Set.singleton Result.T_Int64) mempty + Grin.T_Word64 -> Result.TypeSet (Set.singleton Result.T_Word64) mempty + Grin.T_Float -> Result.TypeSet (Set.singleton Result.T_Float) mempty + Grin.T_Bool -> Result.TypeSet (Set.singleton Result.T_Bool) mempty + Grin.T_Char -> Result.TypeSet (Set.singleton Result.T_Char) mempty + Grin.T_Unit -> Result.TypeSet (Set.singleton Result.T_Unit) mempty + Grin.T_String -> Result.TypeSet (Set.singleton Result.T_String) mempty + -- * Helpers gtagToDtag :: Grin.Tag -> Tag @@ -385,6 +574,14 @@ gtagToDtag (Grin.Tag tt name) = (renderTagType tt) <> Grin.nameText name renderTagType Grin.F = "F" renderTagType (Grin.P m) = "P-" <> Text.pack (show m) <> "-" +dtagToGtag :: Tag -> Grin.Tag +dtagToGtag tag = case Text.unpack tag of + 'C':name -> Grin.Tag Grin.C (Grin.mkName $ Text.pack name) + 'F':name -> Grin.Tag Grin.F (Grin.mkName $ Text.pack name) + 'P':rest -> case Text.splitOn "-" $ Text.pack rest of + ["P",(read . show) -> m, name] -> Grin.Tag (Grin.P m) (Grin.NM name) + _ -> error $ show tag + literalParams :: Grin.Lit -> (SimpleType, Literal) literalParams sv = case sv of Grin.LInt64 i -> (stToDatalogST Grin.T_Int64, Text.pack $ show i) @@ -404,3 +601,25 @@ stToDatalogST = \case Grin.T_Unit -> "Unit" Grin.T_String -> "String" other -> error $ "stToDatalogST: None handled case: " ++ show other + +datalogStToSt :: SimpleType -> (Either Text Grin.SimpleType) +datalogStToSt = \case + "Int64" -> Right $ Grin.T_Int64 + "Word64" -> Right $ Grin.T_Word64 + "Float" -> Right $ Grin.T_Float + "Bool" -> Right $ Grin.T_Bool + "Char" -> Right $ Grin.T_Char + "Unit" -> Right $ Grin.T_Unit + "String" -> Right $ Grin.T_String + other -> Left other + +datalogStToRSt :: SimpleType -> (Either Text Result.SimpleType) +datalogStToRSt = \case + "Int64" -> Right $ Result.T_Int64 + "Word64" -> Right $ Result.T_Word64 + "Float" -> Right $ Result.T_Float + "Bool" -> Right $ Result.T_Bool + "Char" -> Right $ Result.T_Char + "Unit" -> Right $ Result.T_Unit + "String" -> Right $ Result.T_String + other -> Left other diff --git a/grin/src/Pipeline/Pipeline.hs b/grin/src/Pipeline/Pipeline.hs index 836ee3fe..29633ccd 100644 --- a/grin/src/Pipeline/Pipeline.hs +++ b/grin/src/Pipeline/Pipeline.hs @@ -798,8 +798,8 @@ datalogHPT :: PipelineM () datalogHPT = do exp <- use psExp let expV2 = normalise $ SyntaxV2.convertToNew exp - liftIO $ SyntaxV2.printGrin expV2 - liftIO $ Datalog.renderDatalog expV2 + -- liftIO $ SyntaxV2.printGrin expV2 + liftIO $ Datalog.calculateHPTResult expV2 pure () -- confluence testing From 1dc783df463fd5f971233f7dd5cfbd03732bf327 Mon Sep 17 00:00:00 2001 From: Andor Penzes Date: Sun, 10 May 2020 21:01:19 +0200 Subject: [PATCH 04/15] Datalog: Move datalog files around, use data-files. --- grin/app/CLI/Lib.hs | 2 +- grin/datalog/hpt/hpt.dl | 358 ++++++++++++++++++ grin/grin.cabal | 5 + grin/src/Grin/ExtendedSyntax/Datalog.hs | 49 ++- grin/src/Pipeline/Pipeline.hs | 41 +- .../ExtendedSyntax/Conversion.hs | 53 ++- 6 files changed, 473 insertions(+), 35 deletions(-) create mode 100644 grin/datalog/hpt/hpt.dl diff --git a/grin/app/CLI/Lib.hs b/grin/app/CLI/Lib.hs index 929adebb..78fa7e0c 100644 --- a/grin/app/CLI/Lib.hs +++ b/grin/app/CLI/Lib.hs @@ -229,7 +229,7 @@ mainWithArgs args = do let opts = defaultOpts { _poOutputDir = outputDir , _poFailOnLint = not continueOnLint - , _poLogging = not quiet + , _poLogConfig = if quiet then NoLog else StdoutLog , _poSaveBinary = saveBinary , _poCFiles = cFiles } diff --git a/grin/datalog/hpt/hpt.dl b/grin/datalog/hpt/hpt.dl new file mode 100644 index 00000000..9d566638 --- /dev/null +++ b/grin/datalog/hpt/hpt.dl @@ -0,0 +1,358 @@ +.type Function +.type Variable +.type Tag +.type Literal +.type SimpleType +.type CodeName = Variable | Function + +// External function (name, effectful) +.decl External(f:Function, effectful:number, ret:SimpleType) +.decl ExternalParam(f:Function, i:number, st:SimpleType) + +// variable +// example: result <- pure value +.decl Move(result:Variable, value:Variable) + +// literal value +// example: result <- pure 1 +.decl LitAssign(result:Variable, st:SimpleType, l:Literal) + +// node value +// example: result_node <- pure (Ctag item0 item1) +.decl Node(result_node:Variable, t:Tag) +.decl NodeArgument(result_node:Variable, i:number, item:Variable) + +// store/fetch/update +// example: result <- fetch value +.decl Fetch(result:Variable, value:Variable) +// example: result <- store value +.decl Store(result:Variable, value:Variable) +// example: result <- update target value +.decl Update(result:Variable, target:Variable, value:Variable) + + +// app a.k.a. call +// example: call_result <- f value0 value1 +.decl Call(call_result:Variable, f:Function) +.decl CallArgument(call_result:Variable, i:number, value:Variable) + +// bind pattern +// example: node@(Ctag param0 param1) <- pure input_value +.decl NodePattern(node:Variable, t:Tag, input_value:Variable) +.decl NodeParameter(node:Variable, i:number, parameter:Variable) + +// function +// example: f param0 param1 = ... +.decl FunctionParameter(f:Function, i:number, parameter:Variable) + +// case + alt +// example: +// case_result <- case scrut of +// alt_name@(Ctag param0 param1) -> basic_block_name arg0 arg1 +.decl Case(case_result:Variable, scrutinee:Variable) +.decl Alt(case_result:Variable, alt_name:Variable, t:Tag) +// NOTE: first could be just alt_name since it's unique +// QUESTION: why the tag here again? Maybe just store it here, and let case_result be alt_name +.decl AltParameter(case_result:Variable, t:Tag, i:number, parameter:Variable) +.decl AltLiteral(case_result:Variable, alt_name:Variable, st:SimpleType, l:Literal) +.decl AltDefault(case_result:Variable, alt_name:Variable) + +// pure a.k.a. return value +// example: pure value +.decl ReturnValue(n:CodeName, value:Variable) + +// instruction ordering +/* QUESTION: What about f x = pure x +What is the first instruction? +*/ +.decl FirstInst(n:CodeName, result:Variable) +.decl NextInst(prev:Variable, next:Variable) + +.decl EntryPoint(n:CodeName) + + +.input External +.input ExternalParam +.input Move +.input LitAssign +.input Node +.input NodeArgument +.input Fetch +.input Store +.input Update +.input Call +.input CallArgument +.input NodePattern +.input NodeParameter +.input FunctionParameter +.input Case +.input Alt +.input AltParameter +.input AltLiteral +.input AltDefault +.input ReturnValue +.input FirstInst +.input NextInst +.input EntryPoint + +// Reachability +.decl ReachableCode(n:CodeName) +// .output ReachableCode +.decl CodeNameInst(n:CodeName, v:Variable) +// .output CodeNameInst + +CodeNameInst(n, v) :- + FirstInst(n, v). +CodeNameInst(n, v) :- + CodeNameInst(n, v0), + NextInst(v0, v). + +ReachableCode(n) :- + EntryPoint(n). +ReachableCode(n) :- + ReachableCode(n0), + CodeNameInst(n0, v), + Call(v, n). + +.decl ReachableInst(v:Variable) + +ReachableInst(v) :- + ReachableCode(n), + CodeNameInst(n, v). + +// NOTE: For a given pointer, it shows which variable it points to. (Store origin?) +.decl VarPointsTo(v:Variable, target:Variable) +// .output VarPointsTo + +VarPointsTo(v,t) :- + Store(v, t), + ReachableInst(v). + +VarPointsTo(v,t) :- + Move(v, v0), + ReachableInst(v), + VarPointsTo(v0, t). + +VarPointsTo(v,t) :- + Update(r, v, t), + ReachableInst(r). + +VarPointsTo(v,t) :- + FunctionParameter(_, i, v), + CallArgument(r, i, v0), + VarPointsTo(v0, t), + ReachableInst(r). + +// CreatedBy Computation +.decl CreatedBy(v:Variable, value:Variable) +// .output CreatedBy + +.decl Heap(orig:Variable, item:Variable) +.output Heap + +Heap(v,i) :- Store(v,i). + +// HPT: update +Heap(heap_orig, sv) :- + Update(_, heap, sv), + CreatedBy(heap, heap_orig), + Heap(heap_orig, _), + SharedLocation(heap). + +// QUESTION: don't we need this as well? +// ANSWER: probably not, if we are not concerned with aliases (we need only the unique locations) +// Heap(heap, sv) :- +// Update(_, heap, sv), +// SharedLocation(heap). + +CreatedBy(n,n) :- + LitAssign(n,_,_). + +CreatedBy(n, n) :- + Node(n, _). + +CreatedBy(v, v) :- + Store(v, _). + +CreatedBy(v,v) :- + Update(v,_,_). + +CreatedBy(v,v) :- + External(f,_,_), + Call(v,f). + +CreatedBy(v, n_og) :- + CreatedBy(n, n_og), + Move(v, n). + +CreatedBy(v1,v2) :- + FunctionParameter(_,_,p), + CreatedBy(v1,p), + CreatedBy(p,v2). + +// HPT: fetch +CreatedBy(v, item_origin) :- + Fetch(v, heap), + CreatedBy(heap, heap_orig), + Heap(heap_orig, item), + CreatedBy(item, item_origin). + +// fun param +CreatedBy(p, val) :- + CallArgument(r, i, a), + Call(r, f), + FunctionParameter(f, i, p), + CreatedBy(a, val). + +// fun return +CreatedBy(r, val) :- + Call(r, f), + ReturnValue(f, v), + CreatedBy(v, val). + +// Node parameter matching node value created somewhere +CreatedBy(param, argval) :- + NodePattern(v, tag, n), + NodeParameter(v, i, param), + CreatedBy(n, nval), + Node(nval, tag), + NodeArgument(nval, i, arg), + CreatedBy(arg, argval). + +CreatedBy(v, n_og) :- + NodePattern(v, _tag, n), + CreatedBy(n, n_og). + +// Alt value when matched on literal. +CreatedBy(alt_name, scrut_val) :- + Case(case_result, scrut), + AltLiteral(case_result, alt_name, _, _), + CreatedBy(scrut, scrut_val). + +// Alt value when matched on tag +CreatedBy(alt_name, scrut_val) :- + Case(case_result, scrut), + Alt(case_result, alt_name, tag), + CreatedBy(scrut, scrut_val), + // NOTE: this just checks whether the alternative is possible + Node(scrut_val, tag). + +// CreatedBy of alt parameter when matched on tag +CreatedBy(parameter, val) :- + Case(case_res, scrut), + Alt(case_res, _alt_name, tag), + AltParameter(case_res, tag, i, parameter), + CreatedBy(scrut, scrut_val), + Node(scrut_val,tag), + NodeArgument(scrut_val,i,val). + +// NOTE: every alternative should be related to its return value (via ReturnValue) +// Result of case/alt when matched on a node. +CreatedBy(case_result, val) :- + Case(case_result, scrut), + Alt(case_result, alt_name, alt_tag), + CreatedBy(scrut, scrut_og), + Node(scrut_og, alt_tag), + ReturnValue(alt_name, v), + CreatedBy(v, val). + +// Result of case/alt when matched on a literal. +CreatedBy(case_result, val) :- + Case(case_result, _), + AltLiteral(case_result, alt_name, _, _), + ReturnValue(alt_name, v), + CreatedBy(v, val). + +// QUESTION: could implement liveness check here as well? (ignore alt when impossible) +// ANSWER: would have to collect all tags of all possible origins of the scrutinee, then check whether all are covered +// Result of case/alt when matched on the default alternative. +CreatedBy(case_result, val) :- + Case(case_result, _), + AltDefault(case_result, alt_name), + ReturnValue(alt_name, v), + CreatedBy(v, val). + +// Type Env + +.type NodeParamType = Variable | SimpleType +.decl AbstractLocation(n: Variable) +.decl VariableSimpleType(n: Variable, st:SimpleType) +.decl VariableAbstractLocation(n:Variable, loc:Variable) +.decl VariableNodeTag(n:Variable, t:Tag) +.decl VariableNodeParamType(n: Variable, t:Tag, i:number, nt:NodeParamType) + +.output AbstractLocation +AbstractLocation(n) :- Heap(n,_). + +.output VariableSimpleType +VariableSimpleType(n,st) :- LitAssign(n,st,_). +VariableSimpleType(n,"Unit") :- Update(n,_,_). +VariableSimpleType(n,st) :- External(f,_,st), Call(n,f). +VariableSimpleType(n,st) :- ExternalParam(f,i,st), Call(r,f), CallArgument(r,i,n). +// NOTE: that's nice! +VariableSimpleType(n,st) :- CreatedBy(n,r), VariableSimpleType(r,st). + +.output VariableNodeParamType +VariableNodeParamType(n,t,i,al) + :- Node(n,t), NodeArgument(n,i,arg), CreatedBy(arg,al), AbstractLocation(al). +VariableNodeParamType(n,t,i,st) + :- Node(n,t), NodeArgument(n,i,arg), CreatedBy(arg,v), VariableSimpleType(v,st). +VariableNodeParamType(n,t,i,ty) + :- CreatedBy(n,n0), VariableNodeParamType(n0,t,i,ty). + +.output VariableNodeTag +VariableNodeTag(n,t) :- CreatedBy(n,r), Node(r,t). + +// QUESTION: is this basically CreatedBy constrained by AbstractLocation? (i.e. all variables who have pointer producers?) +.output VariableAbstractLocation +VariableAbstractLocation(n,n) :- AbstractLocation(n). +VariableAbstractLocation(n,v) :- CreatedBy(n,v), AbstractLocation(v). + +.decl FunName(f: Function) +// .output FunName + +.decl FunReturn(f:Function, n:Variable) +.output FunReturn + +.decl FunParam(f:Function, i:number, n:Variable) +.output FunParam + +FunName("main"). +FunName(f) :- Call(_,f), ReachableCode(f). + +FunReturn(f,n) :- FunName(f), ReturnValue(f,n). +FunReturn(f,n) :- External(f,_,_), Call(n,f). + +FunParam(f,i,p) :- FunctionParameter(f,i,p). +FunParam(f,i,p) :- ExternalParam(f,i,_), Call(r,f), CallArgument(r,i,p). + +/* If a concrete instance of the abstract location may be subject to a fetch more than once, */ +.decl SharedLocation(n:Variable) +// .output SharedLocation + +SharedLocation(l) :- + AbstractLocation(l), CreatedBy(v,l), NonLinearVar(v). + +// For non-linear variables +// A location may only become shared if it is a possible value of a nonlinear variable. +// NOTE: linear => not shared ~ nonlinear <= shared (agrees with the above statement) + +.decl NonLinearVar(v:Variable) +// .output NonLinearVar + +// Variable used in different use cases. +// CA F M NP RV +// CallArgument CA -- - x xx xx +// Move M -- - - xx xx +// NodeParameter NP -- - - -- xx +// ReturnValue RV -- - - -- -- + +NonLinearVar(n) :- CallArgument(f,_,n), CallArgument(g,_,n), !(f=g). +NonLinearVar(n) :- CallArgument(_,i,n), CallArgument(_,j,n), !(i=j). +NonLinearVar(n) :- CallArgument(_,_,n), Move(_,n). +NonLinearVar(n) :- CallArgument(_,_,n), NodeArgument(_,_,n). +NonLinearVar(n) :- CallArgument(_,_,n), ReturnValue(_,n). +NonLinearVar(n) :- Fetch(r,n), Fetch(q,n), !(r=q). +NonLinearVar(n) :- Move(_,n), NodeArgument(_,_,n). +NonLinearVar(n) :- Move(_,n), ReturnValue(_,n). +NonLinearVar(n) :- NodeParameter(_,_,n), ReturnValue(_,n). diff --git a/grin/grin.cabal b/grin/grin.cabal index 5b082013..8c3e315d 100644 --- a/grin/grin.cabal +++ b/grin/grin.cabal @@ -13,9 +13,14 @@ build-type: Simple --extra-source-files: README.md cabal-version: >=1.10 +data-files: + datalog/hpt/hpt.dl + library hs-source-dirs: src default-extensions: OverloadedStrings + other-modules: + Paths_grin exposed-modules: AbstractInterpretation.ExtendedSyntax.IR AbstractInterpretation.ExtendedSyntax.PrettyIR diff --git a/grin/src/Grin/ExtendedSyntax/Datalog.hs b/grin/src/Grin/ExtendedSyntax/Datalog.hs index 63b89540..c4c7c871 100644 --- a/grin/src/Grin/ExtendedSyntax/Datalog.hs +++ b/grin/src/Grin/ExtendedSyntax/Datalog.hs @@ -19,13 +19,14 @@ import Data.Functor.Foldable import Control.Comonad (extract) import Control.Comonad.Cofree import Data.Either (fromRight) -import Data.Maybe (catMaybes, mapMaybe, fromJust) +import Data.Maybe (catMaybes, mapMaybe, fromMaybe, fromJust) import Data.Proxy import Data.Bifunctor import Data.List (sortBy) import Data.Function (on) import Grin.ExtendedSyntax.Pretty import Debug.Trace +import System.FilePath (takeDirectory) import qualified Data.Vector as Vector import qualified Data.Set as Set @@ -35,13 +36,14 @@ import qualified Data.Text as Text import qualified AbstractInterpretation.ExtendedSyntax.HeapPointsTo.Result as Result import AbstractInterpretation.ExtendedSyntax.HeapPointsTo.Pretty () +import Paths_grin {- TODO: -[ ] Handle As patterns +[x] Handle As patterns [x] Generate code that always have a single return value (In normalisation) [x] Create HPTResult -[ ] Add Datalog program to the resources +[x] Add Datalog program to the resources -} data HPT = HPT @@ -99,10 +101,6 @@ mkBoolean = \case False -> 0 True -> 1 ---instance Souffle.Marshal Grin.Name where --- push (Grin.NM n) = push n --- pop = Grin.NM <$> pop - data EntryPoint = EntryPoint !CodeName deriving (Eq, Show, Generic) data Move = Move !Variable !Variable deriving (Eq, Show, Generic) data LitAssign = LitAssign !Variable !SimpleType !Literal deriving (Eq, Show, Generic) @@ -206,7 +204,14 @@ instance Souffle.Fact FunReturn where factName = const "FunRetur calculateHPTResult :: Grin.Exp -> IO (Maybe Result.HPTResult) calculateHPTResult exp = do - let cfg = Souffle.Config "./datalog/hpt/" (Just "souffle") + + -- The datalog program needs to be registered in the cabal file as data-file + -- but the souffle-haskell library needs a directory to look for the program + -- file. In the instance of the Program HPT the name must concide the one + -- which is registered in the data-file part of the cabal file. + hptProgramDirPath <- takeDirectory <$> getDataFileName "datalog/hpt/hpt.dl" + + let cfg = Souffle.Config hptProgramDirPath (Just "souffle") Souffle.runSouffleWith cfg $ do mprog <- Souffle.init HPT forM mprog $ \prog -> do @@ -224,9 +229,7 @@ calculateHPTResult exp = do <*> Souffle.getFacts prog -- resultFunReturn <*> Souffle.getFacts prog -- resultFunParam <*> Souffle.getFacts prog -- heap - let res = calcHPTResult r - liftIO $ putStrLn $ showWide $ pretty res - pure res + pure $ calcHPTResult r structure :: Handle HPT -> Grin.ExpF (Grin.Exp, SouffleM ()) -> SouffleM () structure prog = \case @@ -471,7 +474,7 @@ variableNodeMap ns ps = Map.unionsWith (++) else Nothing) ps , let ts = case unzip $ Map.toList ps0 of (as, es) | as == [0 .. fromIntegral (length as - 1)] -> es - _ -> error $ "in positions: " ++ show ps0 + (_, es) -> error $ "in positions: " ++ show ps0 -- TODO ] functionNameMap @@ -491,8 +494,9 @@ functionNameMap ps rs vars = Map.fromList ps , let params = case unzip $ Map.toList ps0 of (as,es) | as == [0 .. fromIntegral (length as - 1)] -> Vector.fromList es - _ -> error $ "functionMap: in positions: " ++ show (fun, ret0, ps0) - , let ret = fromJust $ Map.lookup (Grin.mkName ret0) vars + (_, es) -> error $ "functionMap: in positions: " ++ show (fun, ret0, ps0) -- TODO + , let ret = fromMaybe (error $ "functionMap:" ++ show (ret0, vars)) + $ Map.lookup (Grin.mkName ret0) vars ] heapMap @@ -500,13 +504,20 @@ heapMap -> Map.Map Text Int -> Map.Map Grin.Name Result.TypeSet -> Vector.Vector Result.NodeSet -heapMap hs nameToLoc vars = Vector.generate (Map.size nameToLoc) (fromJust . flip Map.lookup heapVals) +heapMap hs nameToLoc vars + = Vector.generate + (Map.size nameToLoc) + (\l -> fromMaybe (error $ "heapMap #0: " ++ show (l, heapVals)) $ Map.lookup l heapVals) -- TODO: mempty where heapVals = Map.unionsWith mappend [ Map.singleton loc nodeSet | Heap ln t <- hs - , let Just loc = Map.lookup ln nameToLoc - , let Just (Result.TypeSet _ nodeSet) = Map.lookup (Grin.mkName t) vars + -- TODO: Fix below, we shouldn't avoid use pattern match errors. + , let loc = fromMaybe (error $ "heapMap #1: " ++ show (ln, nameToLoc)) + $ Map.lookup ln nameToLoc + , let (Result.TypeSet _ nodeSet) + = fromMaybe (error $ "heapMap #2: " ++ show (t,vars)) + $ Map.lookup (Grin.mkName t) vars ] calcHPTResult :: ResultData -> Result.HPTResult @@ -542,7 +553,7 @@ calcHPTResult (ResultData{..}) = Result.HPTResult memory register function (Vector.fromList $ map (Set.map (either - (Result.T_Location . fromJust . flip Map.lookup nameToLoc) + (Result.T_Location . fromJust . flip Map.lookup nameToLoc) -- TODO: mempty id . datalogStToRSt)) types)))) ) ps) @@ -589,7 +600,7 @@ literalParams sv = case sv of Grin.LFloat f -> (stToDatalogST Grin.T_Float, Text.pack $ show f) Grin.LBool b -> (stToDatalogST Grin.T_Bool, Text.pack $ show b) Grin.LChar c -> (stToDatalogST Grin.T_Char, Text.pack $ show c) - Grin.LString s -> (stToDatalogST Grin.T_String, s) -- TODO + Grin.LString s -> (stToDatalogST Grin.T_String, Text.pack $ show s) -- TODO stToDatalogST :: Grin.SimpleType -> SimpleType stToDatalogST = \case diff --git a/grin/src/Pipeline/Pipeline.hs b/grin/src/Pipeline/Pipeline.hs index 29633ccd..5304f841 100644 --- a/grin/src/Pipeline/Pipeline.hs +++ b/grin/src/Pipeline/Pipeline.hs @@ -1,6 +1,7 @@ {-# LANGUAGE LambdaCase, RecordWildCards, RankNTypes, PatternSynonyms, TemplateHaskell #-} module Pipeline.Pipeline - ( PipelineOpts(..) + ( PipelineLogCfg(..) + , PipelineOpts(..) , defaultOpts , PipelineStep(..) , AbstractComputationStep(..) @@ -106,6 +107,7 @@ import Control.DeepSeq import Debug.Trace import Lens.Micro import Data.List +import System.IO import Data.Algorithm.Diff import Data.Algorithm.DiffOutput @@ -123,7 +125,7 @@ import Reducer.PrimOps (evalPrimOp) import Reducer.Pure (EvalPlugin(..)) import qualified Grin.ExtendedSyntax.Syntax as SyntaxV2 -import qualified Transformations.ExtendedSyntax.Conversion as SyntaxV2 (convertToNew) +import qualified Transformations.ExtendedSyntax.Conversion as SyntaxV2 (convertToNew, convert) import qualified Grin.ExtendedSyntax.Pretty as SyntaxV2 import qualified Grin.ExtendedSyntax.Datalog as Datalog import Transformations.ExtendedSyntax.Normalisation (normalise) @@ -264,10 +266,15 @@ pattern PureEvalPlugin :: EvalPlugin -> Bool -> PipelineStep pattern PureEvalPlugin t b <- PureEvalPluginH (H t) b where PureEvalPlugin t b = PureEvalPluginH (H t) b +data PipelineLogCfg + = NoLog + | StdoutLog + | HandleLog Handle + data PipelineOpts = PipelineOpts { _poOutputDir :: FilePath , _poFailOnLint :: Bool - , _poLogging :: Bool + , _poLogConfig :: PipelineLogCfg , _poSaveTypeEnv :: Bool , _poStatistics :: Bool , _poLintOnChange :: Bool @@ -280,7 +287,7 @@ defaultOpts :: PipelineOpts defaultOpts = PipelineOpts { _poOutputDir = ".grin-output" , _poFailOnLint = True - , _poLogging = True + , _poLogConfig = StdoutLog , _poSaveTypeEnv = False , _poStatistics = False , _poLintOnChange = True @@ -574,7 +581,6 @@ runHPTPure = use psHPTProgram >>= \case liftIO $ printf "type-env error: %s" err psTypeEnv .= Nothing - runCByPureWith :: (CBy.CByMapping -> ComputerState -> CBy.CByResult) -> PipelineM () runCByPureWith toCByResult = use psCByProgram >>= \case Nothing -> psCByResult .= Nothing @@ -794,13 +800,15 @@ lintGrin mPhaseName = do liftIO $ die "illegal code" pure () +-- This is a proof of concept implementation of the Datalog implementation of the HPT. +-- After the new version of the AST got introduced to the pipeline. This HPT will be wired in +-- as a default HPT. Meanwhile it simply calculates the HPTResult and prints it on the pipeline. datalogHPT :: PipelineM () datalogHPT = do exp <- use psExp let expV2 = normalise $ SyntaxV2.convertToNew exp - -- liftIO $ SyntaxV2.printGrin expV2 - liftIO $ Datalog.calculateHPTResult expV2 - pure () + res <- liftIO $ Datalog.calculateHPTResult expV2 + pipelineLog $ show $ plain $ pretty res -- confluence testing @@ -941,6 +949,7 @@ runPipeline :: PipelineOpts -> TypeEnv -> Exp -> PipelineM a -> IO (a, Exp) runPipeline o ta e m = do createDirectoryIfMissing True $ _poOutputDir o fmap (second _psExp) $ flip runStateT start $ runReaderT m o where + start = PState { _psExp = e , _psTransStep = 0 @@ -1157,15 +1166,23 @@ decreateIntendation = psIntendation %= pred pipelineLog :: String -> PipelineM () pipelineLog str = do - shouldLog <- view poLogging ident <- use psIntendation - when shouldLog $ liftIO $ putStrLn $ replicate ident ' ' ++ str + view poLogConfig >>= \case + NoLog -> pure () + StdoutLog -> liftIO $ putStrLn $ replicate ident ' ' ++ str + HandleLog h -> liftIO $ do + hPutStrLn h $ replicate ident ' ' ++ str + hFlush h pipelineLogNoLn :: String -> PipelineM () pipelineLogNoLn str = do - shouldLog <- view poLogging ident <- use psIntendation - when shouldLog $ liftIO $ putStr $ replicate ident ' ' ++ str + view poLogConfig >>= \case + NoLog -> pure () + StdoutLog -> liftIO $ putStr $ replicate ident ' ' ++ str + HandleLog h -> liftIO $ do + hPutStr h $ replicate ident ' ' ++ str + hFlush h pipelineLogIterations :: Int -> PipelineM () pipelineLogIterations n = pipelineLogNoLn $ "iterations: " ++ show n ++ " " diff --git a/grin/src/Transformations/ExtendedSyntax/Conversion.hs b/grin/src/Transformations/ExtendedSyntax/Conversion.hs index ba6358bc..4e2f8d02 100644 --- a/grin/src/Transformations/ExtendedSyntax/Conversion.hs +++ b/grin/src/Transformations/ExtendedSyntax/Conversion.hs @@ -9,6 +9,7 @@ import Data.Functor.Foldable as Foldable import qualified Data.Map as M import qualified Data.Vector as V +import qualified Data.Set as S import Control.Monad import Control.Monad.Identity @@ -26,14 +27,16 @@ import qualified Grin.ExtendedSyntax.Grin as New import qualified Grin.ExtendedSyntax.Syntax as New import qualified Grin.ExtendedSyntax.SyntaxDefs as New import qualified Grin.ExtendedSyntax.TypeEnvDefs as New +import qualified AbstractInterpretation.ExtendedSyntax.HeapPointsTo.Result as NewHPTResult +import qualified AbstractInterpretation.HeapPointsTo.Result as HPTResult -import Transformations.Util -import Transformations.Names import Transformations.BindNormalisation +import Transformations.Names import Transformations.Optimising.CopyPropagation import Transformations.Optimising.SimpleDeadVariableElimination -import Transformations.Simplifying.ProducerNameIntroduction import Transformations.Simplifying.BindingPatternSimplification +import Transformations.Simplifying.ProducerNameIntroduction +import Transformations.Util class Convertible a b where @@ -281,6 +284,50 @@ instance Convertible New.Ty Ty where New.TyVar name -> TyVar (convert name) New.TySimple st -> TySimple (convert st) +instance Convertible NewHPTResult.HPTLocal HPTResult.HPTLocal where + convert NewHPTResult.UndefinedProducer = HPTResult.UndefinedProducer + +instance Convertible NewHPTResult.SimpleType HPTResult.SimpleType where + convert = \case + NewHPTResult.T_Int64 -> HPTResult.T_Int64 + NewHPTResult.T_Word64 -> HPTResult.T_Word64 + NewHPTResult.T_Float -> HPTResult.T_Float + NewHPTResult.T_Bool -> HPTResult.T_Bool + NewHPTResult.T_Unit -> HPTResult.T_Unit + NewHPTResult.T_Location l -> HPTResult.T_Location l + NewHPTResult.T_String -> HPTResult.T_String + NewHPTResult.T_Char -> HPTResult.T_Char + NewHPTResult.T_UnspecifiedLocation -> HPTResult.T_UnspecifiedLocation + NewHPTResult.Local l -> HPTResult.Local $ convert l + +instance (Convertible a a') => Convertible (Maybe a) (Maybe a') where + convert = fmap convert + +instance (Convertible a b) => Convertible (V.Vector a) (V.Vector b) where + convert = V.map convert + +instance (Convertible a a', Convertible b b', Ord a') => Convertible (M.Map a b) (M.Map a' b') where + convert = M.mapKeys convert . M.map convert + +instance (Convertible a a', Convertible b b') => Convertible (a,b) (a',b') where + convert (a,b) = (convert a, convert b) + +instance (Convertible a a', Ord a') => Convertible (S.Set a) (S.Set a') where + convert = S.map convert + +instance Convertible NewHPTResult.NodeSet HPTResult.NodeSet where + convert (NewHPTResult.NodeSet ns) = HPTResult.NodeSet $ convert ns + +instance Convertible NewHPTResult.TypeSet HPTResult.TypeSet where + convert (NewHPTResult.TypeSet st ns) = HPTResult.TypeSet (convert st) (convert ns) + +instance Convertible NewHPTResult.HPTResult HPTResult.HPTResult where + convert (NewHPTResult.HPTResult memory register function) + = HPTResult.HPTResult + (convert memory) + (convert register) + (convert function) + instance Convertible New.ExternalKind ExternalKind where convert = \case New.PrimOp -> PrimOp From ce39913b268bb8b6e78f1c5d58c2568e3918cb49 Mon Sep 17 00:00:00 2001 From: Andor Penzes Date: Sun, 10 May 2020 21:03:14 +0200 Subject: [PATCH 05/15] Datalog: Remove previous locations. --- datalog/hpt/hpt.dl | 340 --------------------------------------------- 1 file changed, 340 deletions(-) delete mode 100644 datalog/hpt/hpt.dl diff --git a/datalog/hpt/hpt.dl b/datalog/hpt/hpt.dl deleted file mode 100644 index 50921a3e..00000000 --- a/datalog/hpt/hpt.dl +++ /dev/null @@ -1,340 +0,0 @@ -.type Function -.type Variable -.type Tag -.type Literal -.type SimpleType -.type CodeName = Variable | Function - -// External function (name, effectful) -.decl External(f:Function,effectful:number,ret:SimpleType) -.decl ExternalParam(f:Function, i:number, st:SimpleType) - -// variable -// example: result <- pure value -.decl Move(result:Variable, value:Variable) - -// literal value -// example: result <- pure 1 -.decl LitAssign(result:Variable, st:SimpleType, l:Literal) - -// node value -// example: result_node <- pure (Ctag item0 item1) -.decl Node(result_node:Variable, t:Tag) -.decl NodeArgument(result_node:Variable, i:number, item:Variable) - -// store/fetch/update -// example: result <- fetch value -.decl Fetch(result:Variable, value:Variable) -// example: result <- store value -.decl Store(result:Variable, value:Variable) -// example: result <- update target value -.decl Update(result:Variable, target:Variable, value:Variable) - - -// app a.k.a. call -// example: call_result <- f value0 value1 -.decl Call(call_result:Variable, f:Function) -.decl CallArgument(call_result:Variable, i:number, value:Variable) - -// bind pattern -// example: node@(Ctag param0 param1) <- pure input_value -.decl NodePattern(node:Variable, t:Tag, input_value:Variable) -.decl NodeParameter(node:Variable, i:number, parameter:Variable) - -// function -// example: f param0 param1 = ... -.decl FunctionParameter(f:Function, i:number, parameter:Variable) - -// case + alt -// example: -// case_result <- case scrut of -// alt_value@(Ctag param0 param1) -> basic_block_name arg0 arg1 -.decl Case(case_result:Variable, scrutinee:Variable) -.decl Alt(case_result:Variable, alt_value:Variable, t:Tag) -.decl AltParameter(case_result:Variable, t:Tag, i:number, parameter:Variable) -.decl AltLiteral(case_result:Variable, alt_value:Variable, st:SimpleType, l:Literal) -.decl AltDefault(case_result:Variable, alt_value:Variable) - -// pure a.k.a. return value -// example: pure value -.decl ReturnValue(n:CodeName, value:Variable) - -// instruction ordering -.decl FirstInst(n:CodeName, result:Variable) -.decl NextInst(prev:Variable, next:Variable) - -.decl EntryPoint(n:CodeName) - -.input External -.input ExternalParam -.input Move -.input LitAssign -.input Node -.input NodeArgument -.input Fetch -.input Store -.input Update -.input Call -.input CallArgument -.input NodePattern -.input NodeParameter -.input FunctionParameter -.input Case -.input Alt -.input AltParameter -.input AltLiteral -.input AltDefault -.input ReturnValue -.input FirstInst -.input NextInst -.input EntryPoint - -// Reachability -.decl ReachableCode(n:CodeName) -// .output ReachableCode -.decl CodeNameInst(n:CodeName, v:Variable) -// .output CodeNameInst - -CodeNameInst(n, v) :- - FirstInst(n, v). -CodeNameInst(n, v) :- - CodeNameInst(n, v0), - NextInst(v0, v). - -ReachableCode(n) :- - EntryPoint(n). -ReachableCode(n) :- - ReachableCode(n0), - CodeNameInst(n0, v), - Call(v, n). - -.decl ReachableInst(v:Variable) - -ReachableInst(v) :- - ReachableCode(n), - CodeNameInst(n, v). - -.decl VarPointsTo(v:Variable, target:Variable) -.output VarPointsTo - -VarPointsTo(v,t) :- - Store(v, t), - ReachableInst(v). - -VarPointsTo(v,t) :- - Move(v, v0), - ReachableInst(v), - VarPointsTo(v0, t). - -VarPointsTo(v,t) :- - Update(r, v, t), - ReachableInst(r). - -VarPointsTo(v,t) :- - FunctionParameter(_, i, v), - CallArgument(r, i, v0), - VarPointsTo(v0, t), - ReachableInst(r). - -// Value Computation -.decl Value(v:Variable, value:Variable) -.output Value - -.decl Heap(orig:Variable, item:Variable) -.output Heap - -Heap(v,i) :- Store(v,i). - -// HPT: update -Heap(heap_orig, sv) :- - Update(_, heap, sv), - Value(heap, heap_orig), - Heap(heap_orig, _), - SharedLocation(heap). - -Value(n,n) :- - LitAssign(n,_,_). - -Value(n, n) :- - Node(n, _). - -Value(v, v) :- - Store(v, _). - -Value(v,v) :- - Update(v,_,_). - -Value(v,v) :- - External(f,_,_), - Call(v,f). - -Value(v, n) :- - Node(n, _), - Move(v, n). - -Value(v1,v2) :- - FunctionParameter(_,_,p), - Value(v1,p), - Value(p,v2). - -// HPT: fetch -Value(v, item_origin) :- - Fetch(v, heap), - Value(heap, heap_orig), - Heap(heap_orig, item), - Value(item, item_origin). - -// fun param -Value(p, val) :- - CallArgument(r, i, a), - Call(r, f), - FunctionParameter(f, i, p), - Value(a, val). - -// fun return -Value(r, val) :- - Call(r, f), - ReturnValue(f, v), - Value(v, val). - -// Node parameter matching node value created somewhere -Value(param, argval) :- - NodePattern(v, tag, n), - NodeParameter(v, i, param), - Value(n, nval), - Node(nval, tag), - NodeArgument(nval, i, arg), - Value(arg, argval). - -// Alt value when matched on tag. -Value(alt_val, scrut_val) :- - Case(case_result, scrut), - AltLiteral(case_result, alt_val, _, _), - Value(scrut, scrut_val). - -// Alt value when matched on tag -Value(alt_val, scrut_val) :- - Case(case_result, scrut), - Alt(case_result, alt_val, tag), - Value(scrut, scrut_val), - Node(scrut_val, tag). - -// Value of alt parameter when matched on tag -Value(parameter, val) :- - Case(case_res, scrut), - Alt(case_res, _alt_value, tag), - AltParameter(case_res, tag, i, parameter), - Value(scrut, scrut_val), - Node(scrut_val,tag), - NodeArgument(scrut_val,i,val). - -// Result of case/alt when matched on a node. -Value(case_result, val) :- - Case(case_result, _), - Alt(case_result, alt_value, _), - ReturnValue(alt_value, v), - Value(v, val). - -// Result of case/alt when matched on a literal. -Value(case_result, val) :- - Case(case_result, _), - AltLiteral(case_result, alt_value, _, _), - ReturnValue(alt_value, v), - Value(v, val). - -// Result of case/alt when matched on the default alternative. -Value(case_result, val) :- - Case(case_result, _), - AltDefault(case_result, alt_value), - ReturnValue(alt_value, v), - Value(v, val). - -// Type Env - -.type NodeParamType = Variable | SimpleType -.decl AbstractLocation(n: Variable) -.decl VariableSimpleType(n: Variable, st:SimpleType) -.decl VariableAbstractLocation(n:Variable, loc:Variable) -.decl VariableNodeTag(n:Variable, t:Tag) -.decl VariableNodeParamType(n: Variable, t:Tag, i:number, nt:NodeParamType) - -.output AbstractLocation -AbstractLocation(n) :- Heap(n,_). - -.output VariableSimpleType -VariableSimpleType(n,st) :- LitAssign(n,st,_). -VariableSimpleType(n,"Unit") :- Update(n,_,_). -VariableSimpleType(n,st) :- External(f,_,st), Call(n,f). -VariableSimpleType(n,st) :- ExternalParam(f,i,st), Call(r,f), CallArgument(r,i,n). -VariableSimpleType(n,st) :- Value(n,r), VariableSimpleType(r,st). - -.output VariableNodeParamType -VariableNodeParamType(n,t,i,al) - :- Node(n,t), NodeArgument(n,i,arg), Value(arg,al), AbstractLocation(al). -VariableNodeParamType(n,t,i,st) - :- Node(n,t), NodeArgument(n,i,arg), Value(arg,v), VariableSimpleType(v,st). -VariableNodeParamType(n,t,i,ty) - :- Value(n,n0), VariableNodeParamType(n0,t,i,ty). - -.output VariableNodeTag -VariableNodeTag(n,t) :- Value(n,r), Node(r,t). - -.output VariableAbstractLocation -VariableAbstractLocation(n,n) :- AbstractLocation(n). -VariableAbstractLocation(n,v) :- Value(n,v), AbstractLocation(v). - -.decl FunName(f: Function) -.output FunName - -.decl FunReturn(f:Function, n:Variable) -.output FunReturn - -.decl FunParam(f:Function, i:number, n:Variable) -.output FunParam - -FunName("main"). -FunName(f) :- Call(_,f), ReachableCode(f). - -FunReturn(f,n) :- FunName(f), ReturnValue(f,n). -FunReturn(f,n) :- External(f,_,_), Call(n,f). - -FunParam(f,i,p) :- FunctionParameter(f,i,p). -FunParam(f,i,p) :- ExternalParam(f,i,_), Call(r,f), CallArgument(r,i,p). - -/* If a concrete instance of the abstract location may be subject to a fetch more than once, */ -.decl SharedLocation(n:Variable) -// .output SharedLocation - -SharedLocation(l) :- - AbstractLocation(l), Value(v,l), NonLinearVar(v). - -// For non-linear variables -// A location may only become shared if it is a possible value of a nonlinear variable. -// - -.decl AfterInst(b:Variable,a:Variable) -// .output AfterInst - -AfterInst(b,a) :- NextInst(b,a). -AfterInst(b,c) :- AfterInst(b,a), NextInst(a,c). - -.decl NonLinearVar(v:Variable) -// .output NonLinearVar - -// Variable used in different use cases. -// CA F M NP RV -// CallArgument CA -- - x xx xx -// Move M -- - - xx xx -// NodeParameter NP -- - - -- xx -// ReturnValue RV -- - - -- -- - -NonLinearVar(n) :- CallArgument(f,_,n), CallArgument(g,_,n), !(f=g). -NonLinearVar(n) :- CallArgument(_,i,n), CallArgument(_,j,n), !(i=j). -NonLinearVar(n) :- CallArgument(_,_,n), Move(_,n). -NonLinearVar(n) :- CallArgument(_,_,n), NodeArgument(_,_,n). -NonLinearVar(n) :- CallArgument(_,_,n), ReturnValue(_,n). -NonLinearVar(n) :- Fetch(r,n), Fetch(q,n), !(r=q). -NonLinearVar(n) :- Update(_,v0,n), Fetch(_,v1), AfterInst(v0,v1). -NonLinearVar(n) :- Move(_,n), NodeArgument(_,_,n). -NonLinearVar(n) :- Move(_,n), ReturnValue(_,n). -NonLinearVar(n) :- NodeParameter(_,_,n), ReturnValue(_,n). From f57ca415297e19900079d5f3b943be70ae345101 Mon Sep 17 00:00:00 2001 From: Andor Penzes Date: Mon, 11 May 2020 20:06:01 +0200 Subject: [PATCH 06/15] Fix test suite after PipelineConfig change. --- grin/test/Test/Hspec/PipelineExample.hs | 2 +- grin/test/Transformations/ConfluenceSpec.hs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/grin/test/Test/Hspec/PipelineExample.hs b/grin/test/Test/Hspec/PipelineExample.hs index 48eedd28..30340466 100644 --- a/grin/test/Test/Hspec/PipelineExample.hs +++ b/grin/test/Test/Hspec/PipelineExample.hs @@ -68,7 +68,7 @@ instance Example Pipeline where let opts = PipelineOpts { _poOutputDir = ".output" -- TODO: Random test dir , _poFailOnLint = False - , _poLogging = False + , _poLogConfig = NoLog , _poSaveTypeEnv = False , _poStatistics = False , _poLintOnChange = False diff --git a/grin/test/Transformations/ConfluenceSpec.hs b/grin/test/Transformations/ConfluenceSpec.hs index 1c0df6ae..340f4165 100644 --- a/grin/test/Transformations/ConfluenceSpec.hs +++ b/grin/test/Transformations/ConfluenceSpec.hs @@ -73,7 +73,7 @@ spec = do it "Random pipeline" $ do -- NOTE: This is a random test. This could make fail the build non-related to code changes. - let opts = defaultOpts { _poLogging = False, _poOutputDir = "/tmp", _poFailOnLint = False } + let opts = defaultOpts { _poLogConfig = NoLog, _poOutputDir = "/tmp", _poFailOnLint = False } forAll arbitrary $ \(seed1, seed2) -> monadicIO $ run $ do transformed1 <- randomPipeline (mkStdGen seed1) opts exp transformed2 <- randomPipeline (mkStdGen seed2) opts exp @@ -82,7 +82,7 @@ spec = do -- Needs better code generation. xit "Random pipeline, random expression" $ property $ forAll (PP <$> genProg) $ \(PP prog) -> monadicIO $ run $ do - let opts = defaultOpts { _poLogging = False, _poOutputDir = "/tmp" } + let opts = defaultOpts { _poLogConfig = NoLog, _poOutputDir = "/tmp" } transformed1 <- randomPipeline (mkStdGen 0xffaa419371) opts exp transformed2 <- randomPipeline (mkStdGen 0x51437291fb) opts exp mangleNames transformed1 `sameAs` mangleNames transformed2 From b79b3a714d67c8d7501e7c6c05d17979faee9406 Mon Sep 17 00:00:00 2001 From: Andor Penzes Date: Mon, 11 May 2020 20:07:09 +0200 Subject: [PATCH 07/15] Fix normalisation on short programs. --- .../ExtendedSyntax/Normalisation.hs | 11 ++++ .../ExtendedSyntax/NormalisationSpec.hs | 62 ++++++++++++++----- 2 files changed, 56 insertions(+), 17 deletions(-) diff --git a/grin/src/Transformations/ExtendedSyntax/Normalisation.hs b/grin/src/Transformations/ExtendedSyntax/Normalisation.hs index 988ae667..a56b3bd0 100644 --- a/grin/src/Transformations/ExtendedSyntax/Normalisation.hs +++ b/grin/src/Transformations/ExtendedSyntax/Normalisation.hs @@ -41,6 +41,17 @@ restorePureAsLast = apoM $ \case -- pure x pure $ EBindF (Right lhs) pat (Left (EBind rhs (VarPat x) (SReturn (Var x)))) + -- fun params = + -- v <- lhs + -- rhs + Def f ps body@(EBind{}) -> + pure $ DefF f ps $ Right body + + -- fun params = pure / store / fetch / update / case + Def f ps body -> do + x <- deriveNewName "rapl" + pure $ DefF f ps $ Right $ EBind body (VarPat x) (SReturn (Var x)) + -- rrogram / def other -> pure $ fmap Right $ project other diff --git a/grin/test/Transformations/ExtendedSyntax/NormalisationSpec.hs b/grin/test/Transformations/ExtendedSyntax/NormalisationSpec.hs index 1dc6b108..7d2a1c17 100644 --- a/grin/test/Transformations/ExtendedSyntax/NormalisationSpec.hs +++ b/grin/test/Transformations/ExtendedSyntax/NormalisationSpec.hs @@ -1,8 +1,11 @@ +{-# LANGUAGE LambdaCase, QuasiQuotes #-} module Transformations.ExtendedSyntax.NormalisationSpec where import Test.Hspec import Grin.ExtendedSyntax.TH +import Grin.ExtendedSyntax.Pretty import Test.ExtendedSyntax.Assertions +import Transformations.ExtendedSyntax.Normalisation test :: IO () @@ -12,26 +15,51 @@ spec :: Spec spec = describe "Normalisation" $ do it "works for an example" $ do let before = [prog| - pureLast1 x = pure x + pureLast1 x = pure x - pureLast2 x = - a <- fun1 x - store a + pureLast2 x = + a <- fun1 x + store a - pureLast3 x = - case x of - (CCons a b) -> pure a + pureLast3 x = + case x of + (CCons a b) @ a1 -> pure a - pureLast4 x = - y <- pure x - case y of - (CCons a b) -> pure a + pureLast4 x = + y <- pure x + case y of + (CCons a b) @ a2 -> pure a - pureLast5 x = - y <- pure (CInt x) - pure y - |] + pureLast5 x = + y <- pure (CInt x) + pure y + |] - printGrin $ normalise before - 42 `shouldBe` 42 + let after = [prog| + pureLast1 x = + rapl.0 <- pure x + pure rapl.0 + pureLast2 x = + a <- fun1 $ x + rapl.1 <- store a + pure rapl.1 + + pureLast3 x = + rapl.2 <- case x of + (CCons a b) @ a1 -> + pure a + pure rapl.2 + + pureLast4 x = + y <- pure x + rapl.3 <- case y of + (CCons a b) @ a2 -> + pure a + pure rapl.3 + + pureLast5 x = + y <- pure (CInt x) + pure y + |] + (normalise before) `sameAs` after From 072886c55b7a32aeda0112bb4a9f00dc197ed2ae Mon Sep 17 00:00:00 2001 From: Andor Penzes Date: Mon, 11 May 2020 20:37:25 +0200 Subject: [PATCH 08/15] Datalog HPT Fix variable abstract location lookup. --- grin/src/Grin/ExtendedSyntax/Datalog.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/grin/src/Grin/ExtendedSyntax/Datalog.hs b/grin/src/Grin/ExtendedSyntax/Datalog.hs index c4c7c871..1a421c1e 100644 --- a/grin/src/Grin/ExtendedSyntax/Datalog.hs +++ b/grin/src/Grin/ExtendedSyntax/Datalog.hs @@ -533,7 +533,7 @@ calcHPTResult (ResultData{..}) = Result.HPTResult memory register function resultVariableSimpleType ++ map (\(VariableAbstractLocation n l) - -> case Map.lookup n nameToLoc of + -> case Map.lookup l nameToLoc of Nothing -> mempty Just l -> Map.singleton (Grin.mkName n) From 85d54d1114b60df2be04a350426c21d050e8d136 Mon Sep 17 00:00:00 2001 From: Andor Penzes Date: Mon, 11 May 2020 21:24:47 +0200 Subject: [PATCH 09/15] Some comments. --- grin/src/Grin/ExtendedSyntax/Datalog.hs | 14 +++++++------- grin/src/Pipeline/Pipeline.hs | 2 ++ 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/grin/src/Grin/ExtendedSyntax/Datalog.hs b/grin/src/Grin/ExtendedSyntax/Datalog.hs index 1a421c1e..9068a5ee 100644 --- a/grin/src/Grin/ExtendedSyntax/Datalog.hs +++ b/grin/src/Grin/ExtendedSyntax/Datalog.hs @@ -8,6 +8,13 @@ {-# LANGUAGE RecordWildCards #-} module Grin.ExtendedSyntax.Datalog (calculateHPTResult) where +{- +This is a proof of concept for souffle based implementation of static analyses. + +After merging the new expression syntax tree into the pipeline we need to separate the +dataflow and control flow fact generation from the implementation of the specific analysis. +-} + import Control.Monad (forM, forM_, void) import Data.Int import Language.Souffle.Interpreted as Souffle @@ -38,13 +45,6 @@ import qualified AbstractInterpretation.ExtendedSyntax.HeapPointsTo.Result as Re import AbstractInterpretation.ExtendedSyntax.HeapPointsTo.Pretty () import Paths_grin -{- -TODO: -[x] Handle As patterns -[x] Generate code that always have a single return value (In normalisation) -[x] Create HPTResult -[x] Add Datalog program to the resources --} data HPT = HPT diff --git a/grin/src/Pipeline/Pipeline.hs b/grin/src/Pipeline/Pipeline.hs index 44f63d7a..f3ae8d17 100644 --- a/grin/src/Pipeline/Pipeline.hs +++ b/grin/src/Pipeline/Pipeline.hs @@ -587,6 +587,8 @@ runHPTPure = use psHPTProgram >>= \case psErrors %= (err :) liftIO $ printf "type-env error: %s" err psTypeEnv .= Nothing + -- NOTE: This is for testing only + -- void $ pipelineStep DatalogHPT runCByPureWith :: (CBy.CByMapping -> ComputerState -> CBy.CByResult) -> PipelineM () runCByPureWith toCByResult = use psCByProgram >>= \case From bde39ac5d6f8f5168e9f600e117f1ead213f0270 Mon Sep 17 00:00:00 2001 From: Andor Penzes Date: Mon, 11 May 2020 23:51:47 +0200 Subject: [PATCH 10/15] Rename Datalog.hs to SouffleHPT.hs --- grin/app/CLI/Lib.hs | 2 +- grin/grin.cabal | 3 +- .../{Datalog.hs => SouffleHPT.hs} | 2 +- grin/src/Pipeline/Pipeline.hs | 16 +- .../ExtendedSyntax/SouffleHPTSpec.hs | 202 ++++++++++++++++++ 5 files changed, 214 insertions(+), 11 deletions(-) rename grin/src/Grin/ExtendedSyntax/{Datalog.hs => SouffleHPT.hs} (99%) create mode 100644 grin/test/AbstractInterpretation/ExtendedSyntax/SouffleHPTSpec.hs diff --git a/grin/app/CLI/Lib.hs b/grin/app/CLI/Lib.hs index 78fa7e0c..4c153db9 100644 --- a/grin/app/CLI/Lib.hs +++ b/grin/app/CLI/Lib.hs @@ -134,7 +134,7 @@ pipelineOpts = <|> (T <$> transformOpts) <|> flg ConfluenceTest "confluence-test" "Checks transformation confluence by generating random two pipelines which reaches the fix points." <|> flg PrintErrors "print-errors" "Prints the error log" - <|> flg DatalogHPT "datalog-hpt" "Run HPT in souffle" + <|> flg SouffleHPT "souffle-hpt" "Run HPT in souffle" maybeRenderingOpt :: String -> Maybe RenderingOption diff --git a/grin/grin.cabal b/grin/grin.cabal index 2121c06e..cdc5677d 100644 --- a/grin/grin.cabal +++ b/grin/grin.cabal @@ -120,7 +120,7 @@ library Grin.ExtendedSyntax.TypeEnv Grin.ExtendedSyntax.TypeEnvDefs Grin.ExtendedSyntax.GADT - Grin.ExtendedSyntax.Datalog + Grin.ExtendedSyntax.SouffleHPT Pipeline.Eval Pipeline.Optimizations Pipeline.Pipeline @@ -380,6 +380,7 @@ test-suite grin-test AbstractInterpretation.ExtendedSyntax.LiveVariableSpec AbstractInterpretation.ExtendedSyntax.OptimiseAbstractProgramSpec AbstractInterpretation.ExtendedSyntax.SharingSpec + AbstractInterpretation.ExtendedSyntax.SouffleHPTSpec ExtendedSyntax.LintSpec ExtendedSyntax.NametableSpec ExtendedSyntax.ParserSpec diff --git a/grin/src/Grin/ExtendedSyntax/Datalog.hs b/grin/src/Grin/ExtendedSyntax/SouffleHPT.hs similarity index 99% rename from grin/src/Grin/ExtendedSyntax/Datalog.hs rename to grin/src/Grin/ExtendedSyntax/SouffleHPT.hs index 9068a5ee..ca9b5443 100644 --- a/grin/src/Grin/ExtendedSyntax/Datalog.hs +++ b/grin/src/Grin/ExtendedSyntax/SouffleHPT.hs @@ -6,7 +6,7 @@ {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE RecordWildCards #-} -module Grin.ExtendedSyntax.Datalog (calculateHPTResult) where +module Grin.ExtendedSyntax.SouffleHPT (calculateHPTResult) where {- This is a proof of concept for souffle based implementation of static analyses. diff --git a/grin/src/Pipeline/Pipeline.hs b/grin/src/Pipeline/Pipeline.hs index f3ae8d17..507bce4d 100644 --- a/grin/src/Pipeline/Pipeline.hs +++ b/grin/src/Pipeline/Pipeline.hs @@ -128,7 +128,7 @@ import Reducer.Pure (EvalPlugin(..)) import qualified Grin.ExtendedSyntax.Syntax as SyntaxV2 import qualified Transformations.ExtendedSyntax.Conversion as SyntaxV2 (convertToNew, convert) import qualified Grin.ExtendedSyntax.Pretty as SyntaxV2 -import qualified Grin.ExtendedSyntax.Datalog as Datalog +import qualified Grin.ExtendedSyntax.SouffleHPT as SouffleHPT import Transformations.ExtendedSyntax.Normalisation (normalise) @@ -226,7 +226,7 @@ data PipelineStep | ConfluenceTest | PrintErrors | DebugPipelineState - | DatalogHPT + | SouffleHPT deriving (Eq, Show) pattern DeadCodeElimination :: PipelineStep @@ -502,7 +502,7 @@ pipelineStep p = do PureEval showStatistics -> pureEval (EvalPlugin evalPrimOp) showStatistics PureEvalPlugin evalPlugin showStatistics -> pureEval evalPlugin showStatistics DefinitionalInterpreter evalPlugin showStatistics -> definionalInterpreterEval evalPlugin showStatistics - DatalogHPT -> datalogHPT + SouffleHPT -> souffleHPT after <- use psExp let eff = if before == after then None else ExpChanged showMS :: Rational -> String @@ -588,7 +588,7 @@ runHPTPure = use psHPTProgram >>= \case liftIO $ printf "type-env error: %s" err psTypeEnv .= Nothing -- NOTE: This is for testing only - -- void $ pipelineStep DatalogHPT + -- void $ pipelineStep SouffleHPT runCByPureWith :: (CBy.CByMapping -> ComputerState -> CBy.CByResult) -> PipelineM () runCByPureWith toCByResult = use psCByProgram >>= \case @@ -818,14 +818,14 @@ lintGrin mPhaseName = do liftIO $ die "illegal code" pure () --- This is a proof of concept implementation of the Datalog implementation of the HPT. +-- This is a proof of concept implementation of the Souffle implementation of the HPT. -- After the new version of the AST got introduced to the pipeline. This HPT will be wired in -- as a default HPT. Meanwhile it simply calculates the HPTResult and prints it on the pipeline. -datalogHPT :: PipelineM () -datalogHPT = do +souffleHPT :: PipelineM () +souffleHPT = do exp <- use psExp let expV2 = normalise $ SyntaxV2.convertToNew exp - res <- liftIO $ Datalog.calculateHPTResult expV2 + res <- liftIO $ SouffleHPT.calculateHPTResult expV2 pipelineLog $ show $ plain $ pretty res -- confluence testing diff --git a/grin/test/AbstractInterpretation/ExtendedSyntax/SouffleHPTSpec.hs b/grin/test/AbstractInterpretation/ExtendedSyntax/SouffleHPTSpec.hs new file mode 100644 index 00000000..abc2b6e2 --- /dev/null +++ b/grin/test/AbstractInterpretation/ExtendedSyntax/SouffleHPTSpec.hs @@ -0,0 +1,202 @@ +{-# LANGUAGE LambdaCase, QuasiQuotes, OverloadedStrings #-} +module AbstractInterpretation.ExtendedSyntax.SouffleHPTSpec where + +import Test.Hspec +import Test.ExtendedSyntax.Util +import Grin.ExtendedSyntax.Grin +import Grin.ExtendedSyntax.TH +import Grin.ExtendedSyntax.Lint +import Grin.ExtendedSyntax.TypeEnv as TypeEnv +import Grin.ExtendedSyntax.TypeCheck +import Grin.ExtendedSyntax.PrimOpsPrelude +import Test.ExtendedSyntax.Assertions + +import qualified Data.Map as Map +import qualified Data.Set as Set +import qualified Data.Vector as V + +import AbstractInterpretation.ExtendedSyntax.HeapPointsTo.Result as HPT +import Grin.ExtendedSyntax.SouffleHPT + + +runTests :: IO () +runTests = hspec spec + +spec :: Spec +spec = do + + let loc = tySetFromTypes . pure . HPT.T_Location + mkNode = V.fromList . map Set.fromList + mkNodeSet = NodeSet . Map.fromList . map (\(t,v) -> (t,mkNode v)) + tySetFromNodes = TypeSet mempty + mkTySet = tySetFromNodes . mkNodeSet + tySetFromTypes = flip TypeSet mempty . Set.fromList + mkSimpleMain t = (tySetFromTypes [t], mempty) + + describe "HPT Result" $ do + xit "undefined" $ do + let exp = [prog| + grinMain = + nil <- pure (CNil) + p0 <- store nil + k0 <- pure 0 + cons <- pure (CCons k0 p0) + p1 <- store cons + x0 <- pure (#undefined :: T_Int64) + n0 <- pure (#undefined :: {CCons[T_Int64,{0,1}]}) + p2 <- store n0 + n1 <- pure (#undefined :: {CNil[],CCons[T_Int64,{2}]}) + x1 <- pure (#undefined :: T_Int64) + n2 <- pure (CCons x1 p0) + pure 5 + |] + let expected = HPTResult + { HPT._memory = undefinedExpectedHeap + , HPT._register = undefinedExpectedRegisters + , HPT._function = Map.singleton "grinMain" (mkSimpleMain HPT.T_Int64) + } + nodeSetN0 = mkNodeSet [(cCons, [[HPT.T_Int64], [HPT.T_Location 0, HPT.T_Location 1]])] + undefinedExpectedHeap = V.fromList + [ nilTy + , consTy + , nodeSetN0 + ] + undefinedExpectedRegisters = Map.fromList + [ ("p0", loc 0) + , ("p1", loc 1) + , ("p2", loc 2) + , ("nil", tySetFromNodes nilTy) + , ("cons", tySetFromNodes consTy) + , ("x0", tySetFromTypes [HPT.T_Int64]) + , ("x1", tySetFromTypes [HPT.T_Int64]) + , ("n0", TypeSet mempty nodeSetN0) + , ("n1", typeN1) + , ("n2", typeN2) + , ("k0", tySetFromTypes [HPT.T_Int64]) + ] + typeN1 = mkTySet [ (cCons, [[HPT.T_Int64], [HPT.T_Location 2]]) , (cNil, []) ] + typeN2 = mkTySet [ (cCons, [[HPT.T_Int64], [HPT.T_Location 0]]) ] + nilTy = mkNodeSet [(cNil, [])] + consTy = mkNodeSet [(cCons, [[HPT.T_Int64], [HPT.T_Location 0]])] + + Just res <- calculateHPTResult exp + res `sameAs` expected + + xit "unspec_loc" $ do + let exp = [prog| + grinMain = + k0 <- pure 0 + p0 <- case k0 of + 0 @ _1 -> + nil <- pure (CNil) + store nil + 1 @ _2 -> + pure (#undefined :: #ptr) + n0 <- fetch p0 + n1 <- pure (#undefined :: {CNode[#ptr]}) + (CNode p1)@_v <- pure n1 + x0 <- fetch p1 + update p0 x0 + |] + let expected = HPTResult + { HPT._memory = V.fromList [ nodeSetN0 ] + , HPT._register = unspecLocExpectedRegisters + , HPT._function = Map.singleton "grinMain" (mkSimpleMain HPT.T_Unit) + } + nodeSetN0 = mkNodeSet [(cNil, [])] + nodeSetN1 = mkNodeSet [(cNode, [[HPT.T_UnspecifiedLocation]])] + + unspecLocExpectedRegisters = Map.fromList + [ ("k0", tySetFromTypes [HPT.T_Int64]) + , ("p0", tySetFromTypes [HPT.T_Location 0, HPT.T_UnspecifiedLocation]) + , ("p1", tySetFromTypes [HPT.T_UnspecifiedLocation]) + , ("n0", tySetFromNodes nodeSetN0) + , ("n1", tySetFromNodes nodeSetN1) + , ("_v", tySetFromNodes nodeSetN1) + , ("x0", tySetFromTypes []) + , ("nil", tySetFromNodes nodeSetN0) + + , ("_1", tySetFromTypes [HPT.T_Int64]) + , ("_2", tySetFromTypes [HPT.T_Int64]) + ] + Just res <- calculateHPTResult exp + res `sameAs` expected + + it "simple_case_node" $ do + let exp = [prog| + grinMain = + k0 <- pure 0 + p0 <- case k0 of + 0 @ _1 -> + one <- pure (COne) + a1 <- store one + pure a1 + 1 @ _2 -> + two <- pure (CTwo) + a2 <- store two + pure a2 + n0 <- fetch p0 + g1 <- case n0 of + (COne) @ _3 -> + a3 <- pure 1 + pure a3 + (CTwo) @ _4 -> + a4 <- pure 2 + pure a4 + pure g1 + |] + let expected = HPTResult + { HPT._memory = V.fromList [ nodeSetOne, nodeSetTwo ] + , HPT._register = unspecLocExpectedRegisters + , HPT._function = mempty + } + nodeSetOne = mkNodeSet [(cOne, [])] + nodeSetTwo = mkNodeSet [(cTwo, [])] + + unspecLocExpectedRegisters = Map.fromList + [ ("k0", tySetFromTypes [HPT.T_Int64]) + , ("p0", tySetFromTypes [HPT.T_Location 0, HPT.T_Location 1]) + , ("n0", tySetFromNodes (nodeSetOne <> nodeSetTwo)) + , ("a1", tySetFromTypes [HPT.T_Location 0]) + , ("a2", tySetFromTypes [HPT.T_Location 1]) + , ("a3", tySetFromTypes [HPT.T_Int64]) + , ("a4", tySetFromTypes [HPT.T_Int64]) + , ("g1", tySetFromTypes [HPT.T_Int64]) + , ("one", tySetFromNodes nodeSetOne) + , ("two", tySetFromNodes nodeSetTwo) + + , ("_1", tySetFromTypes [HPT.T_Int64]) + , ("_2", tySetFromTypes [HPT.T_Int64]) + , ("_3", tySetFromNodes nodeSetOne) + , ("_4", tySetFromNodes nodeSetTwo) + ] + Just res <- calculateHPTResult exp + res `sameAs` expected + + it "handles as-patterns with nodes correctly" $ do + let exp = withPrimPrelude [prog| + grinMain = + k0 <- pure 0 + x0 <- pure (CInt k0) + (CInt k1)@x1 <- pure x0 + k2 <- _prim_int_add k0 k1 + _v <- _prim_int_print k2 + pure _v + |] + let expected = HPTResult + { HPT._memory = mempty + , HPT._register = Map.fromList + [ ("k0", tySetFromTypes [HPT.T_Int64]) + , ("x0", tySetFromNodes (mkNodeSet [(cInt, [[HPT.T_Int64]])])) + , ("x1", tySetFromNodes (mkNodeSet [(cInt, [[HPT.T_Int64]])])) + , ("k1", tySetFromTypes [HPT.T_Int64]) + , ("k2", tySetFromTypes [HPT.T_Int64]) + , ("_v", tySetFromTypes [HPT.T_Unit]) + ] + , HPT._function = Map.fromList + [ ("_prim_int_add", (tySetFromTypes [HPT.T_Int64], V.fromList [tySetFromTypes [HPT.T_Int64], tySetFromTypes [HPT.T_Int64]])) + , ("_prim_int_print", (tySetFromTypes [HPT.T_Unit], V.fromList [tySetFromTypes [HPT.T_Int64]])) + ] + } + Just res <- calculateHPTResult exp + res `sameAs` expected From 00b6cc1e5456b13d0b1225a84c77d65ffa6d4a51 Mon Sep 17 00:00:00 2001 From: Csaba Hruska Date: Thu, 23 Dec 2021 16:58:42 +0100 Subject: [PATCH 11/15] fix grin extended syntax (datalog ready) converter to handle single applications correctly --- .../ExtendedSyntax/Normalisation.hs | 15 ++++++++++++++- .../ExtendedSyntax/NormalisationSpec.hs | 14 ++++++++++++++ 2 files changed, 28 insertions(+), 1 deletion(-) diff --git a/grin/src/Transformations/ExtendedSyntax/Normalisation.hs b/grin/src/Transformations/ExtendedSyntax/Normalisation.hs index a56b3bd0..bc3c517b 100644 --- a/grin/src/Transformations/ExtendedSyntax/Normalisation.hs +++ b/grin/src/Transformations/ExtendedSyntax/Normalisation.hs @@ -39,7 +39,7 @@ restorePureAsLast = apoM $ \case -- v <- lhs -- x <- other -- pure x - pure $ EBindF (Right lhs) pat (Left (EBind rhs (VarPat x) (SReturn (Var x)))) + pure $ EBindF (Right lhs) pat (Right (EBind rhs (VarPat x) (SReturn (Var x)))) -- fun params = -- v <- lhs @@ -52,9 +52,22 @@ restorePureAsLast = apoM $ \case x <- deriveNewName "rapl" pure $ DefF f ps $ Right $ EBind body (VarPat x) (SReturn (Var x)) + -- every alt that has a single simple expression that is a program point + Alt pat altName body | isNamedProgramPoint body -> do + x <- deriveNewName "rapl" + pure $ AltF pat altName $ Left $ EBind body (VarPat x) (SReturn (Var x)) + -- rrogram / def other -> pure $ fmap Right $ project other +isNamedProgramPoint :: Exp -> Bool +isNamedProgramPoint = \case + SApp{} -> True + SStore{} -> True + SFetch{} -> True + SUpdate{} -> True + _ -> False + restoreNodePattern :: Exp -> NameM Exp restoreNodePattern = apoM $ \case -- x @ (tag ps) <- pure y diff --git a/grin/test/Transformations/ExtendedSyntax/NormalisationSpec.hs b/grin/test/Transformations/ExtendedSyntax/NormalisationSpec.hs index 7d2a1c17..81d99047 100644 --- a/grin/test/Transformations/ExtendedSyntax/NormalisationSpec.hs +++ b/grin/test/Transformations/ExtendedSyntax/NormalisationSpec.hs @@ -33,6 +33,12 @@ spec = describe "Normalisation" $ do pureLast5 x = y <- pure (CInt x) pure y + + pureLast6 x = + r <- case y of + (CCons a b) @ a2 -> + fun1 x + fun2 x |] let after = [prog| @@ -61,5 +67,13 @@ spec = describe "Normalisation" $ do pureLast5 x = y <- pure (CInt x) pure y + + pureLast6 x = + r <- case y of + (CCons a b) @ a2 -> + rapl.5 <- fun1 x + pure rapl.5 + rapl.4 <- fun2 x + pure rapl.4 |] (normalise before) `sameAs` after From d5561cbf144b9e2b1da8f8483de618b422207d80 Mon Sep 17 00:00:00 2001 From: Csaba Hruska Date: Thu, 23 Dec 2021 17:00:41 +0100 Subject: [PATCH 12/15] port to souffle-haskell 2.1.0 --- grin/src/Grin/ExtendedSyntax/SouffleHPT.hs | 185 ++++++++++++++++----- 1 file changed, 141 insertions(+), 44 deletions(-) diff --git a/grin/src/Grin/ExtendedSyntax/SouffleHPT.hs b/grin/src/Grin/ExtendedSyntax/SouffleHPT.hs index ca9b5443..545c9d11 100644 --- a/grin/src/Grin/ExtendedSyntax/SouffleHPT.hs +++ b/grin/src/Grin/ExtendedSyntax/SouffleHPT.hs @@ -33,7 +33,9 @@ import Data.List (sortBy) import Data.Function (on) import Grin.ExtendedSyntax.Pretty import Debug.Trace +import Text.Read import System.FilePath (takeDirectory) +import qualified Text.Show.Pretty as PP import qualified Data.Vector as Vector import qualified Data.Set as Set @@ -104,7 +106,7 @@ mkBoolean = \case data EntryPoint = EntryPoint !CodeName deriving (Eq, Show, Generic) data Move = Move !Variable !Variable deriving (Eq, Show, Generic) data LitAssign = LitAssign !Variable !SimpleType !Literal deriving (Eq, Show, Generic) -data Node = Node !Variable !Tag deriving (Eq, Show, Generic) +data Node = Node !Variable !Tag !Int32 deriving (Eq, Show, Generic) data NodeArgument = NodeArgument !Variable !Number !Variable deriving (Eq, Show, Generic) data Fetch = Fetch !Variable !Variable deriving (Eq, Show, Generic) data Store = Store !Variable !Variable deriving (Eq, Show, Generic) @@ -128,7 +130,7 @@ data ExternalParam = ExternalParam !Function !Number !SimpleType data Heap = Heap !Variable !Variable deriving (Eq, Show, Generic) data AbstractLocation = AbstractLocation !Loc deriving (Eq, Show, Generic) data VariableSimpleType = VariableSimpleType !Variable !SimpleType deriving (Eq, Show, Generic) -data VariableNodeTag = VariableNodeTag !Variable !Tag deriving (Eq, Show, Generic) +data VariableNodeTag = VariableNodeTag !Variable !Tag !Int32 deriving (Eq, Show, Generic) data VariableNodeParamType = VariableNodeParamType !Variable !Tag !Int32 !SimpleType deriving (Eq, Show, Generic) data VariableAbstractLocation = VariableAbstractLocation !Variable !Loc deriving (Eq, Show, Generic) data FunParam = FunParam !Function !Int32 !Variable deriving (Eq, Show, Generic) @@ -167,39 +169,129 @@ instance Souffle.Marshal VariableNodeParamType instance Souffle.Marshal FunParam instance Souffle.Marshal FunReturn -instance Souffle.Fact EntryPoint where factName = const "EntryPoint" -instance Souffle.Fact External where factName = const "External" -instance Souffle.Fact ExternalParam where factName = const "ExternalParam" -instance Souffle.Fact Move where factName = const "Move" -instance Souffle.Fact LitAssign where factName = const "LitAssign" -instance Souffle.Fact Node where factName = const "Node" -instance Souffle.Fact NodeArgument where factName = const "NodeArgument" -instance Souffle.Fact Fetch where factName = const "Fetch" -instance Souffle.Fact Store where factName = const "Store" -instance Souffle.Fact Update where factName = const "Update" -instance Souffle.Fact Call where factName = const "Call" -instance Souffle.Fact CallArgument where factName = const "CallArgument" -instance Souffle.Fact NodePattern where factName = const "NodePattern" -instance Souffle.Fact NodeParameter where factName = const "NodeParameter" -instance Souffle.Fact Case where factName = const "Case" -instance Souffle.Fact Alt where factName = const "Alt" -instance Souffle.Fact AltLiteral where factName = const "AltLiteral" -instance Souffle.Fact AltDefault where factName = const "AltDefault" -instance Souffle.Fact ReturnValue where factName = const "ReturnValue" -instance Souffle.Fact FirstInst where factName = const "FirstInst" -instance Souffle.Fact NextInst where factName = const "NextInst" -instance Souffle.Fact FunctionParameter where factName = const "FunctionParameter" -instance Souffle.Fact AltParameter where factName = const "AltParameter" - -instance Souffle.Fact Heap where factName = const "Heap" -instance Souffle.Fact VariableSimpleType where factName = const "VariableSimpleType" -instance Souffle.Fact AbstractLocation where factName = const "AbstractLocation" -instance Souffle.Fact VariableAbstractLocation where factName = const "VariableAbstractLocation" -instance Souffle.Fact VariableNodeTag where factName = const "VariableNodeTag" -instance Souffle.Fact VariableNodeParamType where factName = const "VariableNodeParamType" -instance Souffle.Fact FunParam where factName = const "FunParam" -instance Souffle.Fact FunReturn where factName = const "FunReturn" +instance Souffle.Fact EntryPoint where + type FactDirection EntryPoint = 'Souffle.Input + factName = const "EntryPoint" +instance Souffle.Fact External where + type FactDirection External = 'Souffle.Input + factName = const "External" + +instance Souffle.Fact ExternalParam where + type FactDirection ExternalParam = 'Souffle.Input + factName = const "ExternalParam" + +instance Souffle.Fact Move where + type FactDirection Move = 'Souffle.Input + factName = const "Move" + +instance Souffle.Fact LitAssign where + type FactDirection LitAssign = 'Souffle.Input + factName = const "LitAssign" + +instance Souffle.Fact Node where + type FactDirection Node = 'Souffle.Input + factName = const "Node" + +instance Souffle.Fact NodeArgument where + type FactDirection NodeArgument = 'Souffle.Input + factName = const "NodeArgument" + +instance Souffle.Fact Fetch where + type FactDirection Fetch = 'Souffle.Input + factName = const "Fetch" + +instance Souffle.Fact Store where + type FactDirection Store = 'Souffle.Input + factName = const "Store" + +instance Souffle.Fact Update where + type FactDirection Update = 'Souffle.Input + factName = const "Update" + +instance Souffle.Fact Call where + type FactDirection Call = 'Souffle.Input + factName = const "Call" + +instance Souffle.Fact CallArgument where + type FactDirection CallArgument = 'Souffle.Input + factName = const "CallArgument" + +instance Souffle.Fact NodePattern where + type FactDirection NodePattern = 'Souffle.Input + factName = const "NodePattern" + +instance Souffle.Fact NodeParameter where + type FactDirection NodeParameter = 'Souffle.Input + factName = const "NodeParameter" + +instance Souffle.Fact Case where + type FactDirection Case = 'Souffle.Input + factName = const "Case" + +instance Souffle.Fact Alt where + type FactDirection Alt = 'Souffle.Input + factName = const "Alt" + +instance Souffle.Fact AltLiteral where + type FactDirection AltLiteral = 'Souffle.Input + factName = const "AltLiteral" + +instance Souffle.Fact AltDefault where + type FactDirection AltDefault = 'Souffle.Input + factName = const "AltDefault" + +instance Souffle.Fact ReturnValue where + type FactDirection ReturnValue = 'Souffle.Input + factName = const "ReturnValue" + +instance Souffle.Fact FirstInst where + type FactDirection FirstInst = 'Souffle.Input + factName = const "FirstInst" + +instance Souffle.Fact NextInst where + type FactDirection NextInst = 'Souffle.Input + factName = const "NextInst" + +instance Souffle.Fact FunctionParameter where + type FactDirection FunctionParameter = 'Souffle.Input + factName = const "FunctionParameter" + +instance Souffle.Fact AltParameter where + type FactDirection AltParameter = 'Souffle.Input + factName = const "AltParameter" + +instance Souffle.Fact Heap where + type FactDirection Heap = 'Souffle.Output + factName = const "Heap" + +instance Souffle.Fact VariableSimpleType where + type FactDirection VariableSimpleType = 'Souffle.Output + factName = const "VariableSimpleType" + +instance Souffle.Fact AbstractLocation where + type FactDirection AbstractLocation = 'Souffle.Output + factName = const "AbstractLocation" + +instance Souffle.Fact VariableAbstractLocation where + type FactDirection VariableAbstractLocation = 'Souffle.Output + factName = const "VariableAbstractLocation" + +instance Souffle.Fact VariableNodeTag where + type FactDirection VariableNodeTag = 'Souffle.Output + factName = const "VariableNodeTag" + +instance Souffle.Fact VariableNodeParamType where + type FactDirection VariableNodeParamType = 'Souffle.Output + factName = const "VariableNodeParamType" + +instance Souffle.Fact FunParam where + type FactDirection FunParam = 'Souffle.Output + factName = const "FunParam" + +instance Souffle.Fact FunReturn where + type FactDirection FunReturn = 'Souffle.Output + factName = const "FunReturn" calculateHPTResult :: Grin.Exp -> IO (Maybe Result.HPTResult) @@ -211,9 +303,13 @@ calculateHPTResult exp = do -- which is registered in the data-file part of the cabal file. hptProgramDirPath <- takeDirectory <$> getDataFileName "datalog/hpt/hpt.dl" - let cfg = Souffle.Config hptProgramDirPath (Just "souffle") - Souffle.runSouffleWith cfg $ do - mprog <- Souffle.init HPT + let cfg = Souffle.Config + { cfgDatalogDir = hptProgramDirPath + , cfgSouffleBin = Just "souffle" + , cfgFactDir = Nothing -- Just "." + , cfgOutputDir = Nothing -- Just "." + } + Souffle.runSouffleWith cfg HPT $ \mprog -> do forM mprog $ \prog -> do Souffle.addFact prog $ EntryPoint "grinMain" para (structure prog) exp @@ -229,6 +325,7 @@ calculateHPTResult exp = do <*> Souffle.getFacts prog -- resultFunReturn <*> Souffle.getFacts prog -- resultFunParam <*> Souffle.getFacts prog -- heap + --liftIO $ PP.pPrint r pure $ calcHPTResult r structure :: Handle HPT -> Grin.ExpF (Grin.Exp, SouffleM ()) -> SouffleM () @@ -263,7 +360,7 @@ structure prog = \case -- .decl NodeArgument(result_node:Variable, i:number, item:Variable) Grin.EBindF ((Grin.SReturn (Grin.ConstTagNode tag items)), lhs) (Grin.VarPat res) (_, rhs) -> do lhs - Souffle.addFact prog $ Node (Grin.nameText res) (gtagToDtag tag) + Souffle.addFact prog $ Node (Grin.nameText res) (gtagToDtag tag) (fromIntegral $ length items) Souffle.addFacts prog $ zipWith (\n v -> NodeArgument (Grin.nameText res) n (Grin.nameText v)) [0..] items rhs @@ -466,15 +563,15 @@ variableNodeMap -> Map.Map Text [(Tag, [Set.Set SimpleType])] variableNodeMap ns ps = Map.unionsWith (++) [ Map.singleton n [(t,ts)] - | VariableNodeTag n t <- ns - , let ps0 = Map.unionsWith mappend - $ mapMaybe (\(VariableNodeParamType n0 t0 i s) + | VariableNodeTag n t arity <- ns + , let ps0 = Map.unionsWith mappend $ [Map.singleton i Set.empty | i <- [0 .. fromIntegral (arity - 1)]] + ++ mapMaybe (\(VariableNodeParamType n0 t0 i s) -> if n == n0 && t == t0 then Just $ Map.singleton i (Set.singleton s) else Nothing) ps , let ts = case unzip $ Map.toList ps0 of (as, es) | as == [0 .. fromIntegral (length as - 1)] -> es - (_, es) -> error $ "in positions: " ++ show ps0 -- TODO + (_, es) -> error $ "in positions: " ++ show (ps0, n, t) -- TODO ] functionNameMap @@ -590,8 +687,8 @@ dtagToGtag tag = case Text.unpack tag of 'C':name -> Grin.Tag Grin.C (Grin.mkName $ Text.pack name) 'F':name -> Grin.Tag Grin.F (Grin.mkName $ Text.pack name) 'P':rest -> case Text.splitOn "-" $ Text.pack rest of - ["P",(read . show) -> m, name] -> Grin.Tag (Grin.P m) (Grin.NM name) - _ -> error $ show tag + ["", (readMaybe . Text.unpack) -> Just m, name] -> Grin.Tag (Grin.P m) (Grin.NM name) + l -> error $ "cannot decode tag: " ++ show tag ++ " " ++ show l literalParams :: Grin.Lit -> (SimpleType, Literal) literalParams sv = case sv of From 2a8c57c8d5cbadf532b08136c55ff6c8cd3b1c88 Mon Sep 17 00:00:00 2001 From: Csaba Hruska Date: Thu, 23 Dec 2021 17:01:37 +0100 Subject: [PATCH 13/15] use souffle-haskell-2.1.0 --- stack.yaml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/stack.yaml b/stack.yaml index 9ef729ba..d68daa41 100644 --- a/stack.yaml +++ b/stack.yaml @@ -18,8 +18,7 @@ extra-deps: subdirs: - llvm-hs - llvm-hs-pure - - github: luc-tielen/souffle-haskell - commit: bf6e419d65059274f3a32d4e81505ccadd42ff58 + - souffle-haskell-2.1.0 flags: llvm-hs: From fdd915832267151657b71d1469d626d326dd5078 Mon Sep 17 00:00:00 2001 From: Csaba Hruska Date: Thu, 23 Dec 2021 22:12:17 +0100 Subject: [PATCH 14/15] write out datalog facts ; track node arity --- grin/datalog/hpt/hpt.dl | 25 +++++++++++----------- grin/src/Grin/ExtendedSyntax/SouffleHPT.hs | 4 ++-- 2 files changed, 15 insertions(+), 14 deletions(-) diff --git a/grin/datalog/hpt/hpt.dl b/grin/datalog/hpt/hpt.dl index 9d566638..619812d7 100644 --- a/grin/datalog/hpt/hpt.dl +++ b/grin/datalog/hpt/hpt.dl @@ -19,7 +19,7 @@ // node value // example: result_node <- pure (Ctag item0 item1) -.decl Node(result_node:Variable, t:Tag) +.decl Node(result_node:Variable, t:Tag, arity:number) .decl NodeArgument(result_node:Variable, i:number, item:Variable) // store/fetch/update @@ -97,7 +97,7 @@ What is the first instruction? // Reachability .decl ReachableCode(n:CodeName) -// .output ReachableCode +.output ReachableCode .decl CodeNameInst(n:CodeName, v:Variable) // .output CodeNameInst @@ -115,6 +115,7 @@ ReachableCode(n) :- Call(v, n). .decl ReachableInst(v:Variable) +.output ReachableInst ReachableInst(v) :- ReachableCode(n), @@ -169,7 +170,7 @@ CreatedBy(n,n) :- LitAssign(n,_,_). CreatedBy(n, n) :- - Node(n, _). + Node(n, _, _). CreatedBy(v, v) :- Store(v, _). @@ -215,7 +216,7 @@ CreatedBy(param, argval) :- NodePattern(v, tag, n), NodeParameter(v, i, param), CreatedBy(n, nval), - Node(nval, tag), + Node(nval, tag, _), NodeArgument(nval, i, arg), CreatedBy(arg, argval). @@ -235,15 +236,15 @@ CreatedBy(alt_name, scrut_val) :- Alt(case_result, alt_name, tag), CreatedBy(scrut, scrut_val), // NOTE: this just checks whether the alternative is possible - Node(scrut_val, tag). + Node(scrut_val, tag, _). // CreatedBy of alt parameter when matched on tag CreatedBy(parameter, val) :- Case(case_res, scrut), - Alt(case_res, _alt_name, tag), + Alt(case_res, alt_name, tag), AltParameter(case_res, tag, i, parameter), CreatedBy(scrut, scrut_val), - Node(scrut_val,tag), + Node(scrut_val,tag, _), NodeArgument(scrut_val,i,val). // NOTE: every alternative should be related to its return value (via ReturnValue) @@ -252,7 +253,7 @@ CreatedBy(case_result, val) :- Case(case_result, scrut), Alt(case_result, alt_name, alt_tag), CreatedBy(scrut, scrut_og), - Node(scrut_og, alt_tag), + Node(scrut_og, alt_tag, _), ReturnValue(alt_name, v), CreatedBy(v, val). @@ -278,7 +279,7 @@ CreatedBy(case_result, val) :- .decl AbstractLocation(n: Variable) .decl VariableSimpleType(n: Variable, st:SimpleType) .decl VariableAbstractLocation(n:Variable, loc:Variable) -.decl VariableNodeTag(n:Variable, t:Tag) +.decl VariableNodeTag(n:Variable, t:Tag, arity:number) .decl VariableNodeParamType(n: Variable, t:Tag, i:number, nt:NodeParamType) .output AbstractLocation @@ -294,14 +295,14 @@ VariableSimpleType(n,st) :- CreatedBy(n,r), VariableSimpleType(r,st). .output VariableNodeParamType VariableNodeParamType(n,t,i,al) - :- Node(n,t), NodeArgument(n,i,arg), CreatedBy(arg,al), AbstractLocation(al). + :- Node(n,t,_), NodeArgument(n,i,arg), CreatedBy(arg,al), AbstractLocation(al). VariableNodeParamType(n,t,i,st) - :- Node(n,t), NodeArgument(n,i,arg), CreatedBy(arg,v), VariableSimpleType(v,st). + :- Node(n,t,_), NodeArgument(n,i,arg), CreatedBy(arg,v), VariableSimpleType(v,st). VariableNodeParamType(n,t,i,ty) :- CreatedBy(n,n0), VariableNodeParamType(n0,t,i,ty). .output VariableNodeTag -VariableNodeTag(n,t) :- CreatedBy(n,r), Node(r,t). +VariableNodeTag(n,t,arity) :- CreatedBy(n,r), Node(r,t,arity). // QUESTION: is this basically CreatedBy constrained by AbstractLocation? (i.e. all variables who have pointer producers?) .output VariableAbstractLocation diff --git a/grin/src/Grin/ExtendedSyntax/SouffleHPT.hs b/grin/src/Grin/ExtendedSyntax/SouffleHPT.hs index 545c9d11..e4329bbd 100644 --- a/grin/src/Grin/ExtendedSyntax/SouffleHPT.hs +++ b/grin/src/Grin/ExtendedSyntax/SouffleHPT.hs @@ -306,8 +306,8 @@ calculateHPTResult exp = do let cfg = Souffle.Config { cfgDatalogDir = hptProgramDirPath , cfgSouffleBin = Just "souffle" - , cfgFactDir = Nothing -- Just "." - , cfgOutputDir = Nothing -- Just "." + , cfgFactDir = Just "." + , cfgOutputDir = Just "." } Souffle.runSouffleWith cfg HPT $ \mprog -> do forM mprog $ \prog -> do From dbb1c3569557f03f317c724e71b65b33b5bb5083 Mon Sep 17 00:00:00 2001 From: Csaba Hruska Date: Thu, 23 Dec 2021 22:13:01 +0100 Subject: [PATCH 15/15] write out souffle-hpt result to file along with the input program in the new syntax --- grin/src/Pipeline/Pipeline.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/grin/src/Pipeline/Pipeline.hs b/grin/src/Pipeline/Pipeline.hs index 507bce4d..faa8aba0 100644 --- a/grin/src/Pipeline/Pipeline.hs +++ b/grin/src/Pipeline/Pipeline.hs @@ -825,8 +825,10 @@ souffleHPT :: PipelineM () souffleHPT = do exp <- use psExp let expV2 = normalise $ SyntaxV2.convertToNew exp + liftIO $ writeFile "syntax2_program.grin" $ show $ SyntaxV2.WPP expV2 res <- liftIO $ SouffleHPT.calculateHPTResult expV2 - pipelineLog $ show $ plain $ pretty res + --pipelineLog $ show $ plain $ pretty res + liftIO $ writeFile "souffle-hpt-result.out" $ show $ plain $ pretty res -- confluence testing