-
-
Notifications
You must be signed in to change notification settings - Fork 36
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
5 changed files
with
365 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
141 changes: 141 additions & 0 deletions
141
grin/src/AbstractInterpretation/ExtendedSyntax/Sharing/CodeGen.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,141 @@ | ||
{-# LANGUAGE LambdaCase, RecordWildCards, TemplateHaskell, OverloadedStrings #-} | ||
module AbstractInterpretation.ExtendedSyntax.Sharing.CodeGen where | ||
|
||
import Control.Monad.State | ||
|
||
import Data.Set (Set) | ||
import Data.Map (Map) | ||
import Data.Vector (Vector) | ||
import qualified Data.Set as Set | ||
import qualified Data.Map as Map | ||
import qualified Data.Vector as Vec | ||
|
||
import qualified Data.Set.Extra as Set | ||
|
||
import Data.Maybe | ||
import Data.Foldable | ||
import Data.Functor.Foldable | ||
|
||
import Lens.Micro.Platform | ||
|
||
import Grin.ExtendedSyntax.Syntax | ||
import Grin.ExtendedSyntax.TypeEnvDefs | ||
import AbstractInterpretation.ExtendedSyntax.Util (converge) | ||
import AbstractInterpretation.ExtendedSyntax.IR (Instruction(..), Reg, AbstractProgram) | ||
import qualified AbstractInterpretation.ExtendedSyntax.IR as IR | ||
|
||
import AbstractInterpretation.ExtendedSyntax.HeapPointsTo.CodeGenBase | ||
import qualified AbstractInterpretation.ExtendedSyntax.HeapPointsTo.CodeGen as HPT | ||
|
||
{- | ||
[x] Calc non-linear variables, optionally ignoring updates. | ||
[x] Assumption: all the non-linear variables have registers already. | ||
[x] For all non-linear variables set the locations as shared. | ||
[x] For all the shared locations, look up the pointed locations and set to shared them. | ||
[x] Create a register to maintain sharing information | ||
[x] Add Sharing register as parameter to HPT | ||
[x] Add Sharing register as parameter to Sharing | ||
[x] Remove _shared field from Reduce | ||
[-] Add 'In' to the Condition | ||
[x] Remove GetShared from IR | ||
[x] Remove SetShared from IR | ||
[x] CodeGenMain: depend on optimisation phase, before InLineAfter inline | ||
[x] CodeGenMain: add an extra parameter | ||
[x] Pipeline: Set a variable if the codegen is after or before | ||
[-] Add mode as parameter for the eval'' and typecheck | ||
[x] Remove Mode for calcNonLinearVars | ||
-} | ||
|
||
data SharingMapping = SharingMapping | ||
{ _shRegName :: Reg | ||
, _hptMapping :: HPTMapping | ||
} deriving (Show) | ||
|
||
concat <$> mapM makeLenses [''SharingMapping] | ||
|
||
-- | Calc non linear variables, ignores variables that are used in update locations | ||
-- This is an important difference, if a variable would become non-linear due to | ||
-- being subject to an update, that would make the sharing analysis incorrect. | ||
-- One possible improvement is to count the updates in a different set and make a variable | ||
-- linear if it is subject to an update more than once. But that could not happen, thus the only | ||
-- introdcution of new updates comes from inlining eval. | ||
calcNonLinearNonUpdateLocVariables :: Exp -> Set Name | ||
calcNonLinearNonUpdateLocVariables exp = Set.fromList $ Map.keys $ Map.filter (>1) $ cata collect exp | ||
where | ||
union = Map.unionsWith (+) | ||
|
||
collect :: ExpF (Map Name Int) -> Map Name Int | ||
collect = \case | ||
ECaseF scrut alts -> union (seen scrut : alts) | ||
SStoreF var -> seen var | ||
SFetchF var -> seen var | ||
SUpdateF p var -> seen var | ||
SReturnF val -> case val of | ||
Var v -> seen v | ||
ConstTagNode _ args -> union $ map seen args | ||
_ -> mempty | ||
SAppF _ ps -> union $ fmap seen ps | ||
rest -> Data.Foldable.foldr (Map.unionWith (+)) mempty rest | ||
|
||
seen :: Name -> Map Name Int | ||
seen v = Map.singleton v 1 | ||
|
||
calcSharedLocationsPure :: TypeEnv -> Exp -> Set Loc | ||
calcSharedLocationsPure TypeEnv{..} e = converge (==) (Set.concatMap fetchLocs) origShVarLocs where | ||
nonLinearVars = calcNonLinearNonUpdateLocVariables e | ||
shVarTypes = Set.mapMaybe (`Map.lookup` _variable) $ nonLinearVars | ||
origShVarLocs = onlyLocations . onlySimpleTys $ shVarTypes | ||
|
||
onlySimpleTys :: Set Type -> Set SimpleType | ||
onlySimpleTys tys = Set.fromList [ sty | T_SimpleType sty <- Set.toList tys ] | ||
|
||
onlyLocations :: Set SimpleType -> Set Loc | ||
onlyLocations stys = Set.fromList $ concat [ ls | T_Location ls <- Set.toList stys ] | ||
|
||
fetchLocs :: Loc -> Set Loc | ||
fetchLocs l = onlyLocations . fieldsFromNodeSet . fromMaybe (error msg) . (Vec.!?) _location $ l | ||
where msg = "Sharing: Invalid heap index: " ++ show l | ||
|
||
fieldsFromNodeSet :: NodeSet -> Set SimpleType | ||
fieldsFromNodeSet = Set.fromList . concatMap Vec.toList . Map.elems | ||
|
||
|
||
sharingCodeGen :: Reg -> Exp -> CG () | ||
sharingCodeGen shReg e = do | ||
forM_ nonLinearVars $ \name -> do | ||
-- For all non-linear variables set the locations as shared. | ||
nonLinearVarReg <- getReg name | ||
-- this will copy node field info as well, but we will only use "simpleType" info | ||
emit $ copyStructureWithPtrInfo nonLinearVarReg shReg | ||
|
||
mergedFields <- newReg | ||
pointsToNodeReg <- newReg | ||
emit IR.Fetch | ||
{ addressReg = shReg | ||
, dstReg = pointsToNodeReg | ||
} | ||
emit IR.Project | ||
{ srcReg = pointsToNodeReg | ||
, srcSelector = IR.AllFields | ||
, dstReg = mergedFields | ||
} | ||
emit $ copyStructureWithPtrInfo mergedFields shReg | ||
where | ||
nonLinearVars = calcNonLinearNonUpdateLocVariables e | ||
|
||
codeGenM :: Exp -> CG (AbstractProgram, SharingMapping) | ||
codeGenM e = do | ||
HPT.codeGenM e | ||
shReg <- newReg | ||
sharingCodeGen shReg e | ||
(prg, hptMapping) <- HPT.mkAbstractProgramM | ||
let mapping = SharingMapping | ||
{ _shRegName = shReg | ||
, _hptMapping = hptMapping | ||
} | ||
pure (prg, mapping) | ||
|
||
codeGen :: Program -> (AbstractProgram, SharingMapping) | ||
codeGen prg@(Program{}) = evalState (codeGenM prg) emptyCGState | ||
codeGen _ = error "Program expected" |
33 changes: 33 additions & 0 deletions
33
grin/src/AbstractInterpretation/ExtendedSyntax/Sharing/Pretty.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,33 @@ | ||
{-# LANGUAGE LambdaCase, RecordWildCards #-} | ||
module AbstractInterpretation.ExtendedSyntax.Sharing.Pretty where | ||
|
||
import Text.PrettyPrint.ANSI.Leijen | ||
|
||
import Data.Set (Set) | ||
import Data.Map (Map) | ||
import qualified Data.Set as Set | ||
import qualified Data.Map as Map | ||
|
||
import Data.Vector (Vector) | ||
import qualified Data.Vector as V | ||
|
||
import Grin.ExtendedSyntax.Pretty | ||
import AbstractInterpretation.ExtendedSyntax.HeapPointsTo.Pretty | ||
import AbstractInterpretation.ExtendedSyntax.HeapPointsTo.Result | ||
import AbstractInterpretation.ExtendedSyntax.Sharing.Result | ||
|
||
|
||
instance Pretty SharingResult where | ||
pretty = prettySharingResult | ||
|
||
prettySharingResult :: SharingResult -> Doc | ||
prettySharingResult shResult = vsep | ||
[ yellow (text "Heap (* is shared)") <$$> indent 4 (prettyKeyValue . V.toList . V.imap annotateSharedLoc $ _memory) | ||
, yellow (text "Env") <$$> indent 4 (prettyKeyValue $ Map.toList _register) | ||
, yellow (text "Function") <$$> indent 4 (vsep $ map prettyHPTFunction $ Map.toList _function) | ||
] where | ||
shLocs = _sharedLocs shResult | ||
HPTResult{..} = _hptResult $ shResult | ||
annotateSharedLoc loc ty | ||
| Set.member loc shLocs = (pretty loc <> text "*", ty) | ||
| otherwise = (pretty loc, ty) |
38 changes: 38 additions & 0 deletions
38
grin/src/AbstractInterpretation/ExtendedSyntax/Sharing/Result.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,38 @@ | ||
{-# LANGUAGE TemplateHaskell, GeneralizedNewtypeDeriving, RecordWildCards #-} | ||
|
||
module AbstractInterpretation.ExtendedSyntax.Sharing.Result where | ||
|
||
import Data.Set (Set) | ||
import Data.Map (Map) | ||
import qualified Data.Set as Set | ||
import qualified Data.Map as Map | ||
|
||
import Lens.Micro.Platform | ||
|
||
import Grin.ExtendedSyntax.Grin (Name, Tag) | ||
import AbstractInterpretation.ExtendedSyntax.IR (AbstractProgram) | ||
import AbstractInterpretation.ExtendedSyntax.Sharing.CodeGen | ||
import AbstractInterpretation.ExtendedSyntax.HeapPointsTo.Result | ||
import qualified AbstractInterpretation.ExtendedSyntax.Reduce as R | ||
|
||
|
||
data SharingResult | ||
= SharingResult | ||
{ _hptResult :: HPTResult | ||
, _sharedLocs :: Set Loc | ||
} | ||
deriving (Eq, Show) | ||
|
||
emptySharingResult :: SharingResult | ||
emptySharingResult = SharingResult emptyHPTResult mempty | ||
|
||
concat <$> mapM makeLenses [''SharingResult] | ||
|
||
toSharingResult :: SharingMapping -> R.ComputerState -> SharingResult | ||
toSharingResult SharingMapping{..} comp = SharingResult hptResult sharedLocs where | ||
hptResult = toHPTResult _hptMapping comp | ||
sharedLocs = onlyLocations sty | ||
TypeSet sty _ = convertReg (_hptMapping, comp) _shRegName | ||
|
||
onlyLocations :: Set SimpleType -> Set Loc | ||
onlyLocations stys = Set.fromList [ l | T_Location l <- Set.toList stys ] |
149 changes: 149 additions & 0 deletions
149
grin/test/AbstractInterpretation/ExtendedSyntax/SharingSpec.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,149 @@ | ||
{-# LANGUAGE LambdaCase #-} | ||
{-# LANGUAGE RecordWildCards #-} | ||
{-# LANGUAGE QuasiQuotes #-} | ||
module AbstractInterpretation.ExtendedSyntax.SharingSpec where | ||
|
||
import Data.Set (Set) | ||
import qualified Data.Set as Set | ||
|
||
import qualified Grin.TH as Old | ||
|
||
import Test.Hspec | ||
import Grin.ExtendedSyntax.Grin | ||
import Grin.ExtendedSyntax.TH | ||
import Grin.ExtendedSyntax.Pretty | ||
import Grin.ExtendedSyntax.PrimOpsPrelude | ||
|
||
import AbstractInterpretation.ExtendedSyntax.Reduce | ||
import AbstractInterpretation.ExtendedSyntax.Sharing.CodeGen | ||
import AbstractInterpretation.ExtendedSyntax.Sharing.Result | ||
|
||
import Transformations.ExtendedSyntax.Conversion (convertToNew) | ||
|
||
|
||
|
||
runTests :: IO () | ||
runTests = hspec spec | ||
|
||
spec :: Spec | ||
spec = describe "Sharing analysis" $ do | ||
it "has not changed for sum simple." $ do | ||
let result = calcSharedLocations testProgram | ||
let expected = Set.fromList [0,1,4,5] | ||
result `shouldBe` expected | ||
|
||
it "finds non-transitive shared locations" $ do | ||
-- A sharing is calculated via for non-linear variables | ||
let code = [prog| | ||
main = | ||
one <- pure (COne) | ||
l0 <- store one | ||
l1 <- store one | ||
_1 <- update l0 one | ||
_2 <- fun l0 | ||
v <- fetch l0 | ||
pure () | ||
|] | ||
let result = calcSharedLocations code | ||
let expected = Set.fromList [0] | ||
result `shouldBe` expected | ||
|
||
it "finds location based transitive shared location" $ do | ||
let code = [prog| | ||
main = | ||
one <- pure (COne) | ||
l0 <- store one | ||
two <- pure (CTwo l0) | ||
l1 <- store two | ||
_1 <- update l0 one | ||
_2 <- fun l1 | ||
v <- fetch l1 | ||
pure () | ||
|] | ||
let result = calcSharedLocations code | ||
let expected = Set.fromList [0,1] | ||
result `shouldBe` expected | ||
|
||
it "finds location based on transitive non-linear var" $ do | ||
let code = [prog| | ||
main = | ||
one <- pure (COne) | ||
l0 <- store one | ||
l1 <- store one | ||
_1 <- update l0 one | ||
l2 <- pure l1 | ||
v <- fetch l2 | ||
_2 <- fun l2 | ||
pure () | ||
|] | ||
let result = calcSharedLocations code | ||
let expected = Set.fromList [1] | ||
result `shouldBe` expected | ||
|
||
it "finds location fetched twice inside a node with as-pattern" $ do | ||
let code = [prog| | ||
main = | ||
one <- pure (COne) | ||
l0 <- store one | ||
two <- pure (CTwo l0) | ||
l1 <- store two | ||
_1@(CTwo l2) <- fetch l1 | ||
_2 <- fetch l2 | ||
_2 <- fetch l2 | ||
pure () | ||
|] | ||
let result = calcSharedLocations code | ||
let expected = Set.fromList [0] | ||
result `shouldBe` expected | ||
|
||
calcSharedLocations :: Exp -> Set Loc | ||
calcSharedLocations = _sharedLocs . calcSharingResult | ||
|
||
calcSharingResult :: Exp -> SharingResult | ||
calcSharingResult prog | ||
| (shProgram, shMapping) <- codeGen prog | ||
, computer <- _airComp . evalAbstractProgram $ shProgram | ||
, shResult <- toSharingResult shMapping computer | ||
= shResult | ||
|
||
testProgram :: Exp | ||
-- The syntax conversion preserves the abstract heap layout | ||
testProgram = withPrimPrelude . convertToNew $ [Old.prog| | ||
grinMain = t1 <- store (CInt 1) | ||
t2 <- store (CInt 10000) | ||
t3 <- store (Fupto t1 t2) | ||
t4 <- store (Fsum t3) | ||
(CInt r') <- eval t4 | ||
_prim_int_print r' | ||
|
||
upto m n = (CInt m') <- eval m | ||
(CInt n') <- eval n | ||
b' <- _prim_int_gt m' n' | ||
if b' then | ||
pure (CNil) | ||
else | ||
m1' <- _prim_int_add m' 1 | ||
m1 <- store (CInt m1') | ||
p <- store (Fupto m1 n) | ||
pure (CCons m p) | ||
|
||
sum l = l2 <- eval l | ||
case l2 of | ||
(CNil) -> pure (CInt 0) | ||
(CCons x xs) -> (CInt x') <- eval x | ||
(CInt s') <- sum xs | ||
ax' <- _prim_int_add x' s' | ||
pure (CInt ax') | ||
|
||
eval q = v <- fetch q | ||
case v of | ||
(CInt x'1) -> pure v | ||
(CNil) -> pure v | ||
(CCons y ys) -> pure v | ||
(Fupto a b) -> w <- upto a b | ||
update q w | ||
pure w | ||
(Fsum c) -> z <- sum c | ||
update q z | ||
pure z | ||
|] |