Permalink
Browse files

Separating a few modules out.

  • Loading branch information...
1 parent 5966679 commit d59a983a5a75403b5186d32faa1c7fe067ee927a @scottgw committed Apr 23, 2012
Showing with 292 additions and 313 deletions.
  1. +15 −4 Domain.hs
  2. +85 −0 DomainGen.hs
  3. +3 −3 GenerateSummaries.hs
  4. +178 −0 Instrument.hs
  5. +11 −306 Main.hs
View
@@ -74,10 +74,8 @@ teToD curr' te = go curr' (contents te)
D.BinOpExpr (dEqOp op) (go' curr e1) (go' curr e2)
go curr (T.Old e) = D.UnOpExpr D.Old (go' curr e)
go curr (T.CurrentVar _) = curr
- go curr (T.Attached _ e _) =
- let ClassType cn _ = texprTyp (contents e)
- structType = D.StructType cn []
- in D.BinOpExpr (D.RelOp D.Neq) (go' curr e) D.LitNull
+ go curr (T.Attached _ e _) =
+ D.BinOpExpr (D.RelOp D.Neq) (go' curr e) D.LitNull
go curr (T.Box _ e) = go' curr e
go curr (T.Unbox _ e) = go' curr e
go curr (T.Cast _ e) = go' curr e
@@ -100,6 +98,19 @@ dEqOp o = D.RelOp (rel o)
rel T.TildeEq = D.Eq
rel T.TildeNeq = D.Neq
+
+replaceExpr :: D.Expr -> D.Expr -> D.Expr -> D.Expr
+replaceExpr new old = go
+ where
+ rep = replaceExpr new old
+ go e | e == old = new
+ go (D.Call name args) = D.Call name (map rep args)
+ go (D.Access trg name) = D.Access (rep trg) name
+ go (D.BinOpExpr op e1 e2) = D.BinOpExpr op (rep e1) (rep e2)
+ go (D.UnOpExpr op e) = D.UnOpExpr op (rep e)
+ go e = e
+
+
-- op1 :: E.UnOp -> D.UnOp
-- op1 E.Not = D.Not
-- op1 E.Neg = D.Neg
View
@@ -0,0 +1,85 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+module DomainGen where
+
+import Data.List (nub)
+
+import qualified Data.Map as Map
+import Data.Map (Map)
+
+import qualified Data.Set as Set
+import Data.Set (Set)
+
+import Language.DemonL.PrettyPrint
+
+import Language.Eiffel.Syntax as E hiding (select)
+import Language.Eiffel.Util
+import Language.Eiffel.Position
+import Language.Eiffel.TypeCheck.TypedExpr as T
+
+import ClassEnv
+import Domain
+import Util
+
+data Indicator = Indicator Typ String deriving (Eq, Ord, Show)
+indicatorTuple (Indicator t name) = (t, name)
+
+data Action =
+ Action { actionType :: Typ
+ , actionName :: String
+ } deriving (Eq, Ord, Show)
+
+actionTuple (Action t name) = (t, name)
+
+domActions :: TInterEnv -> T.TExpr -> Set (Typ, String)
+domActions env e =
+ let eIndicators = exprIndicators e
+ -- Desired interface:
+ domActions' :: Set Indicator -> Set Action
+ domActions' = Set.fold (Set.union . go) Set.empty
+ where
+ go :: Indicator -> Set Action
+ go ind@(Indicator typ _name) =
+ let Just clas = envLookup (classNameType typ) env
+ routs = allRoutines clas
+ indicators = clausesIndicators . featurePost
+ hasIndicator = Set.member ind . indicators
+ modifyIndicators = filter hasIndicator routs
+ in Set.fromList (map (\r -> Action typ (featureName r))
+ modifyIndicators)
+ in (Set.map indicatorTuple eIndicators) `Set.union`
+ (Set.map actionTuple (domActions' eIndicators))
+
+clausesIndicators :: [Clause T.TExpr] -> Set Indicator
+clausesIndicators = Set.unions . map (exprIndicators . clauseExpr)
+
+exprIndicators :: T.TExpr -> Set Indicator
+exprIndicators = go'
+ where go' = go . contents
+ go (T.Call trg name args _t) =
+ let argPairs = Set.unions (map exprIndicators (trg : args))
+ in if isBasic (texpr trg)
+ then argPairs
+ else Set.insert (Indicator (texpr trg) name) argPairs
+ go (T.EqExpr _ e1 e2) = go' e1 `Set.union` go' e2
+ go _ = Set.empty
+
+domain clas flatEnv =
+ let Just rout :: Maybe (AbsRoutine (RoutineBody TExpr) TExpr) =
+ findFeature clas "dequeue"
+ pres = nub $ allPreConditions flatEnv $
+ contents $ routineBody (routineImpl rout)
+ typesAndNames = map (domActions flatEnv) pres
+ typeNameMap = collectNames (Set.unions typesAndNames)
+ domainClasses = Map.mapWithKey (cutDownClass flatEnv) typeNameMap
+ in print (domainDoc untypeExprDoc $ makeDomain $ Map.elems domainClasses)
+
+
+cutDownClass flatEnv typ names =
+ let Just clas = envLookupType typ flatEnv
+ undefineNames = Set.fromList (map featureName (allFeatures clas :: [FeatureEx TExpr])) Set.\\ names
+ in Set.fold undefineName clas undefineNames
+
+collectNames :: Set (Typ, String) -> Map Typ (Set String)
+collectNames = Set.fold go Map.empty
+ where go (t, name) =
+ Map.insertWith (Set.union) t (Set.singleton name)
@@ -25,11 +25,11 @@ localDir = homeDir ++ ["local"]
libraryDir :: [String]
libraryDir = localDir ++ ["Eiffel70","library"]
-names :: [String]
-names = ["base2","base","thread","test"]
+libraryNames :: [String]
+libraryNames = ["base2","base","thread","test"]
searchDirectories :: [(String, FilePath)]
-searchDirectories = zip names $
+searchDirectories = zip libraryNames $
map joinPath
[ srcDir ++ ["eiffelbase2","trunk"]
, libraryDir ++ ["base","elks"]
View
@@ -0,0 +1,178 @@
+module Instrument (instrument) where
+
+import Data.List
+
+import Language.Eiffel.Syntax as E hiding (select)
+import Language.Eiffel.Util
+import Language.Eiffel.Position
+
+import Language.Eiffel.TypeCheck.TypedExpr as T
+
+import qualified Language.DemonL.AST as D
+import Language.DemonL.PrettyPrint
+
+import ClassEnv
+import Domain
+import Util
+
+stmt' :: Typ -> TInterEnv
+ -> [Decl] -> [D.Expr]
+ -> UnPosTStmt -> ([D.Expr], UnPosTStmt)
+stmt' curr env decls ens = go
+ where
+ meld = meldCall curr decls
+
+ go' = stmt curr env decls
+
+ go :: UnPosTStmt -> ([D.Expr], UnPosTStmt)
+ go (Block blkBody) =
+ let (cs, blkBody') = wpList ens blkBody -- mapAccumR (stmt env) ens ss
+ wpList p [] = (p, [])
+ wpList p (s:ss) =
+ let (p', ss') = wpList p ss
+ (p'', s') = go' p' s
+ in (p'', s':ss')
+ in meld cs (Block blkBody')
+
+ go (Assign trg src) =
+ let newEns = replaceClause ens trg src
+ in meld newEns (Assign trg src)
+
+ go (CallStmt e) =
+ let pre = preCond env e
+ posts :: [T.TExpr]
+ posts = texprAssert' featurePost env e -- ignores call chain
+ nonOlds = concatMap nonOldExprs posts
+ ens' = pre ++ ens -- TODO: perform weakest precondition calculation
+ in meld ens' (CallStmt e)
+
+ -- TODO: Deal with until, invariant, and variant as well
+ go (Loop from untl inv body var) =
+ let
+ (bodyCls, body') = go' ens body
+ (fromCls, from') = go' bodyCls from
+ in meld fromCls (Loop from' untl inv body' var)
+ go e = error ("stmt'go: " ++ show e)
+
+instrument :: TInterEnv
+ -> String
+ -> AbsClas (RoutineBody TExpr) TExpr
+ -> AbsClas (RoutineBody TExpr) TExpr
+instrument env routName clas =
+ classMapRoutines (\r -> if featureName r == routName
+ then instrumentRoutine env (classToType clas) r
+ else r) clas
+
+instrumentRoutine :: TInterEnv
+ -> Typ
+ -> AbsRoutine (RoutineBody TExpr) TExpr
+ -> AbsRoutine (RoutineBody TExpr) TExpr
+instrumentRoutine env typ r =
+ let decls = routineDecls r
+ in r {routineImpl = instrumentBody typ env (routineEns r) decls (routineImpl r)}
+
+instrumentBody :: Typ
+ -> TInterEnv
+ -> Contract TExpr
+ -> [Decl]
+ -> RoutineBody TExpr
+ -> RoutineBody TExpr
+instrumentBody currType env ens decls (RoutineBody locals localProc body) =
+ let
+ ensD = map (teToDCurr . clauseExpr) (contractClauses ens)
+ body' = snd $ stmt currType env decls ensD body
+ in RoutineBody locals localProc body'
+instrumentBody _ _ _ _ r = r
+
+stmt :: Typ -> TInterEnv -> [Decl] -> [D.Expr] -> TStmt -> ([D.Expr], TStmt)
+stmt currType env decls ens s =
+ let (cs, s') = stmt' currType env decls ens (contents s)
+ in (cs, attachEmptyPos s')
+
+nonOldExprs :: T.TExpr -> [T.UnPosTExpr]
+nonOldExprs = nub . go'
+ where
+ go' :: T.TExpr -> [T.UnPosTExpr]
+ go' = go . contents
+
+ go e@(T.Call _trg _name args _) = e : concatMap go' args
+ go e@(Var _ _) = [e]
+ go _ = []
+
+
+dNeqNull :: Pos UnPosTExpr -> D.Expr
+dNeqNull e = D.BinOpExpr (D.RelOp D.Neq) (teToDCurr e) D.LitNull
+
+dConj :: [D.Expr] -> D.Expr
+dConj = foldr1 (D.BinOpExpr D.And)
+
+
+preCond :: TInterEnv -> TExpr -> [D.Expr]
+preCond env = go . contents
+ where
+ go' = go . contents
+ go (T.Call trg name args _) =
+ let callPreTExpr = texprAssert featurePre env trg name
+ callPres = map (teToD (teToDCurr trg)) callPreTExpr
+ in dNeqNull trg : concatMap go' (trg : args) ++ callPres
+ go (T.Access trg _ _) = dNeqNull trg : go' trg
+ go (T.Old e) = go' e
+ go (T.CurrentVar _) = []
+ go (T.Attached _ e _) = go' e
+ go (T.Box _ e) = go' e
+ go (T.Unbox _ e) = go' e
+ go (T.Cast _ e) = go' e
+ go (T.Var _ _) = []
+ go (T.ResultVar _) = []
+ go (T.LitInt _) = []
+ go (T.LitBool _) = []
+ go (T.LitVoid _) = []
+ go (T.LitChar _) = error "preCond: unimplemented LitChar"
+ go (T.LitString _) = error "preCond: unimplemented LitString"
+ go (T.LitDouble _) = error "preCond: unimplemented LitDouble"
+ go (T.LitArray _) = error "preCond: unimplemented LitArray"
+ go (T.Tuple _) = error "preCond: unimplemented Tuple"
+ go (T.Agent _ _ _ _) = error "preCond: unimplemented Agent"
+
+meldCall :: Typ -> [Decl] -> [D.Expr] -> UnPosTStmt -> ([D.Expr], UnPosTStmt)
+meldCall currType decls pre s =
+ let
+ tuple x y = p0 $ T.Tuple [x, y]
+ curr = p0 $ T.CurrentVar currType
+
+ string :: String -> T.TExpr
+ string name = p0 $ T.LitString name
+
+ var name t = p0 $ T.Var name t
+
+ array :: [T.TExpr] -> T.TExpr
+ array = p0 . T.LitArray
+
+ rely :: [T.TExpr] -> T.TExpr
+ rely es = p0 $ T.Call curr "rely_call" es NoType
+
+ precondStr = show $ untypeExprDoc $ dConj $ nub pre
+
+ _agent = p0 . T.Agent
+
+ declTup (Decl n t) = tuple (string n) (var n t)
+
+ declArray :: T.TExpr
+ declArray =
+ array (tuple (string "this") curr : map declTup decls)
+
+ args :: [T.TExpr]
+ args = [declArray, string precondStr]
+
+ relyCall :: TStmt
+ relyCall = p0 $ E.CallStmt $ rely args
+ in (pre, Block [relyCall, p0 s])
+
+
+p0 :: a -> Pos a
+p0 = attachEmptyPos
+
+
+replaceClause :: [D.Expr] -> TExpr -> TExpr -> [D.Expr]
+replaceClause clauses old new =
+ map (replaceExpr (teToDCurr old) (teToDCurr new)) clauses
Oops, something went wrong.

0 comments on commit d59a983

Please sign in to comment.