cpsa-4.4.1: src/CPSA/GenRules.hs
-- Generates rules when loading protocols from S-Expressions.
-- Copyright (c) 2009 The MITRE Corporation
--
-- This program is free software: you can redistribute it and/or
-- modify it under the terms of the BSD License as published by the
-- University of California.
module CPSA.GenRules where
import qualified Data.List as L
-- import CPSA.Lib.SExpr
import CPSA.Signature (Sig)
import CPSA.Algebra
import CPSA.Channel
import CPSA.Protocol
import CPSA.LoadFormulas
{--
import System.IO.Unsafe
z :: Show a => a -> b -> b
z x y = unsafePerformIO (print x >> return y)
zz :: Show a => a -> a
zz x = z x x
zb :: Show a => a -> Bool -> Bool
zb a False = z a False
zb _ b = b
zn :: Show a => a -> Maybe b -> Maybe b
zn x Nothing = z x Nothing
zn _ y = y
zf :: Show a => a -> Bool -> Bool
zf x False = z x False
zf _ y = y
zt :: Show a => a -> Bool -> Bool
zt x True = z x True
zt _ y = y
zl :: Show a => [a] -> [a]
zl a = z (length a) a
--}
-- Protocol Rules
type Conjunction = [AForm]
conjunctionOfConj :: Conj -> Conjunction
conjunctionOfConj = map snd
type Conjunctor = [Term] -> Conjunction -- Function which, given new
-- free variables, plugs them
-- in to yield a conjunction
-- [Term] ->
type Existor = Conjunctor
-- Used to say: -- Function which, given new
-- variables to bind
-- existentially, plugs them
-- in to yield a conjunctor
ruleOfClauses :: Sig -> Gen -> String ->
VarListSpec -> Conjunctor ->
[([Term],Existor)] -> (Gen,Rule)
ruleOfClauses sig g rn sortedVarLists antecedent evarDisjuncts =
let (g',uvars) = sortedVarsOfStrings sig g sortedVarLists in
let disjuncts =
map
(\(evars,existor) ->
(evars,(existor -- evars
-- use only the members
-- of uvars that avoid names in evars
(avoidByName evars uvars))))
evarDisjuncts in
(g',
(Rule { rlname = rn,
rlgoal =
(Goal
{ uvars = uvars,
antec = antecedent uvars,
consq = disjuncts,
concl = map snd disjuncts}),
rlcomment = [] }))
where
varOfName _ [] = Nothing
varOfName name (v : rest) =
if (name == varName v)
then Just v
else varOfName name rest
avoidByName evars uvars =
map (\uv ->
case varOfName (varName uv) evars of
Nothing -> uv
Just ev -> ev)
uvars
applyToSoleEntry :: (a -> b) -> String -> [a] -> b
applyToSoleEntry f _ [a] = f a
applyToSoleEntry _ s _ = error s
applyToThreeEntries :: (a -> a -> a -> b) -> String -> [a] -> b
applyToThreeEntries f _ [a1,a2,a3] = f a1 a2 a3
applyToThreeEntries _ s _ = error s
applyToStrandVarAndParams :: (a -> [a] -> b) -> [a] -> String -> b
applyToStrandVarAndParams _ [] s = error s
applyToStrandVarAndParams f (a : rest) _ = f a rest
-- foldM :: (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b
neqRules :: Sig -> Gen -> (Gen, [Rule])
neqRules sig g =
foldr
(\sortName (g,rs) ->
let (g', r) =
(ruleOfClauses sig g ("neqRl_" ++ sortName)
[(sortName,["x"])]
(applyToSoleEntry
(\x -> [(AFact "neq" [x,x])])
"neqrules: Impossible var list.")
[]) -- false conclusion
in
(g', r : rs))
(g,[])
["indx", "strd", "mesg"]
transRls :: Sig -> Gen -> Role -> [(Int,Int)] -> (Gen, [Rule])
transRls sig g rl =
L.foldl
(\(g, rs) pair ->
let (g', r) = f g pair in
(g', r : rs))
(g, [])
where
f g (i,j) =
ruleOfClauses sig g ("trRl_" ++ (rname rl) ++ "-at-" ++ (show i))
[("strd",["z"])]
(applyToSoleEntry
(\z -> [(Length rl z (indxOfInt (j+1)))])
"transRules: Impossible var list.")
[([], -- no existentially bound vars
(applyToSoleEntry
(\z -> [(Trans (z, (indxOfInt i)))])
"transRules: Impossible var list."))]
lastRecvInCS :: Role -> Int -> Int -> Int
lastRecvInCS rl start end =
loop start $ drop (start+1) $ rtrace rl
-- i is always the index before the index of the first entry still
-- in c.
where
loop i ((In (ChMsg ch _)) : c)
| i < end && isLocn ch = loop (i+1) c
| otherwise = i
loop i _ = i
csRules :: Sig -> Gen -> Role -> [(Int,Int)] -> (Gen, [Rule])
csRules sig g rl =
L.foldl
(\(g, rs) (start,end) ->
(let (g', csRules) = f g start end in
(g', csRules ++ rs)))
(g,[])
where
f g start end =
let lastRecv = lastRecvInCS rl start end in
let (g',rs) = foldr (\ind (g,soFar) ->
let (g',r) = causeRule g rl start ind in
(g', (r : soFar)))
(g,[])
[start+1..lastRecv] in
foldr (\ind (g,soFar) ->
let (g',r) = effectRule g rl end ind in
(g', (r : soFar)))
(g',rs)
[lastRecv+1..end-1]
causeRule g rl start ind =
ruleOfClauses sig g
("cau-" ++ (rname rl) ++ "-" ++ (show ind))
[("strd",["z", "z1"]), ("indx", ["i"])]
(applyToThreeEntries
(\z z1 i -> [(Length rl z (indxOfInt (ind+1))),
(Prec -- LeadsTo
(z1,i) (z,(indxOfInt ind)))])
"csRules: Impossible var list.")
[([],
(applyToThreeEntries
(\z z1 _ -> [Equals z z1])
"csRules: Impossible var list.")),
([],
(applyToThreeEntries
(\z z1 i -> [(Prec (z1,i) (z,(indxOfInt start)))])
"csRules: Impossible var list."))]
effectRule g rl end ind =
ruleOfClauses sig g
("eff-" ++ (rname rl) ++ "-" ++ (show ind))
[("strd",["z", "z1"]), ("indx", ["i"])]
(applyToThreeEntries
(\z z1 i -> [(Length rl z (indxOfInt (ind+1))),
(Prec --LeadsTo
(z, (indxOfInt ind)) (z1,i))])
"csRules: Impossible var list.")
[([],
(applyToThreeEntries
(\z z1 _ -> [Equals z z1])
"csRules: Impossible var list.")),
([],
(applyToThreeEntries
(\z z1 i -> [(Length rl z (indxOfInt (end+1))),
(Prec (z, (indxOfInt end)) (z1,i))])
"csRules: Impossible var list."))]
data FoundAt = FoundAt Int
| Missing Term
-- Return the smallest height in the trace of rl at which all of the
-- vars are found to have occurred, if found, or a missing var if no
-- such height.
varsUsedHeight :: Role -> [Term] -> FoundAt
varsUsedHeight rl vars =
loop 0 vars
where
occ = flip firstOccurs rl -- return *index*
loop i [] = FoundAt (1+i) -- convert to height
loop i (v : rest) =
case occ v of
Nothing -> Missing v
Just j -> loop (max i j) rest
boundVarNamesOfVarListSpec :: VarListSpec -> [String]
boundVarNamesOfVarListSpec [] = []
boundVarNamesOfVarListSpec ((_,names) : rest) =
L.nub $ names ++ boundVarNamesOfVarListSpec rest
freeVarsInExistential :: ([Term],Existor) -> [Term]
freeVarsInExistential (vars,c) =
let bvns = map varName vars in
concatMap
(\a -> filter (not . (flip elem bvns) . varName)
(aFreeVars [] a))
(c [])
freeVarsInDisjunction :: [([Term],Existor)] -> [Term]
freeVarsInDisjunction vcs =
L.nub
(foldr (\vc acc -> (freeVarsInExistential vc) ++ acc)
[]
vcs)
freeVarsInConjLists :: [([Term], Conj)] -> [Term]
freeVarsInConjLists [] = []
freeVarsInConjLists ((vars,conj) : rest) =
((foldr (\(_,aForm) soFar -> aFreeVars soFar aForm)
[]
conj)
L.\\ vars)
++ (freeVarsInConjLists rest)
-- Take the subset of fvars that have a name shared with some member
-- of pvars
freeVarsSubsetByName :: [Term] -> [Term] -> [Term]
freeVarsSubsetByName fvars pvars =
loop fvars []
where
pvarNames = map varName pvars
loop [] soFar = reverse soFar
loop (fv : rest) soFar
| (varName fv) `elem` pvarNames =
loop rest (fv : soFar)
| otherwise =
loop rest soFar
-- freeVarsNamedIn [] pvars = []
-- freeVarsNamedIn (fv : rest) pvars =
-- if (varName fv) `elem` (map varName pvars)
-- then fv : freeVarsNamedIn rest pvars
-- else freeVarsNamedIn rest pvars
conclHeight :: Role -> [([Term], Conj)] -> FoundAt
conclHeight _ [] = FoundAt 1
conclHeight rl (disj : rest) =
case conclHeight rl rest of
Missing v -> Missing v
FoundAt j ->
case varsUsedHeight rl $ freeVarsInConjLists [disj] of
Missing v -> Missing v
FoundAt i -> FoundAt (max i j)
renameApart :: String -> [Term] -> String
renameApart prefix vars =
if not (prefix `elem` vns) then prefix
else
loop 0
where
vns = map varName vars
loop :: Int -> String
loop i =
let candidate = prefix ++ "-" ++ (show i) in
if not (candidate `elem` vns) then candidate
else
loop (i+1)
ruleOfDisjAtHeight :: Sig -> Gen -> Role -> String -> [([Term],Existor)] -> Int -> (Gen, Rule)
ruleOfDisjAtHeight sig g rl rulename disj ht =
let fvs = freeVarsInDisjunction disj in
ruleOfClauses
sig g rulename
(("strd", [renameApart "z" (concatMap fst disj)])
: varListSpecOfVars (freeVarsSubsetByName fvs (rvars rl)))
(\vars ->
applyToStrandVarAndParams
(\z pvars ->
(Length rl z (indxOfInt ht))
: (map
(\v ->
case paramOfName (varName v) rl of
Nothing -> errorWithMsg v " not found."
Just p ->
case firstOccurs p rl of
Nothing -> errorWithMsg v " not found."
Just i ->
if i < ht then (Param rl p (i+1) z v)
else errorWithMsg v
(" introduced for " ++ (varName p) ++ " too high in role " ++ (rname rl) ++": " ++ (show i) ++
" not below " ++ (show ht) ++ "in " ++ rulename ++ "."))
pvars))
vars
"ruleOfDisjAtHeight: vars not strand+prams?")
disj
where
errorWithMsg v tail =
error ("ruleOfDisjAtHeight: Parameter " ++
(varName v) ++ tail)
genOneAssumeRl :: Sig -> Gen -> Role -> Int -> [([Term], Conj)] -> (Gen, Rule)
genOneAssumeRl sig g rl n disjuncts =
case conclHeight rl disjuncts of
Missing v -> error ("genOneAssumeRl: Variable not in role " ++ (rname rl)
++ ": " ++ (show (varName v)))
FoundAt ht ->
ruleOfDisjAtHeight
sig g rl ("assume-" ++ (rname rl) ++ "-" ++ (show n))
(map (\(evars,conj) ->
(evars,
(\pvars ->
case envsRoleParams rl g pvars of
(_,e) : _ -> (map snd $ instantiateConj e conj)
_ -> error ("genOneAssumeRl: Parameter matching failed "
++ (show pvars) ++ (rname rl)))))
disjuncts)
ht
--
-- where
-- freeVars bndList conjunct = (aFreeVars [] conjunct) L.\\ bndList
--
-- vars = L.nub (concatMap (\(vars,conj) ->
-- concatMap (freeVars vars) (map snd conj))
-- disjuncts)
genAssumeRls :: Sig -> Gen -> Role -> [[([Term], Conj)]] -> (Gen, [Rule])
genAssumeRls sig g rl disjunctLists =
(g',rls)
where
(g',rls,_) =
foldr (\ds (g, rs, n) ->
(let (g', new_rule) = genOneAssumeRl sig g rl n ds in
(g', new_rule : rs, n+1)))
(g, [], (0 :: Int))
disjunctLists
genOneRelyGuarRl :: Sig -> Gen -> Role -> Int -> String -> [([Term], Conj)] -> (Gen, Rule)
genOneRelyGuarRl sig g rl ht kind disjuncts =
case conclHeight rl disjuncts of
Missing v -> error ("genOneRelyGuarRl: Variable not in role " ++ (rname rl)
++ ": " ++ (show (varName v)))
FoundAt fndHt | fndHt <= ht ->
ruleOfDisjAtHeight
sig g rl (kind ++ "-" ++ (rname rl) ++ "-" ++ (show ht))
(map (\(evars,conj) ->
(evars,
(\pvars ->
case envsRoleParams rl g pvars of
(_,e) : _ -> (map snd $ instantiateConj e conj)
_ -> error ("genOneAssumeRl: Parameter matching failed "
++ (show pvars) ++ (rname rl)))))
disjuncts)
ht
| otherwise -> error ("genOneRelyGuarRl: Variable found above ht " ++ (show ht) ++
" in " ++ (rname rl))
genStateRls :: Sig -> Gen -> Role -> [Term] -> (Gen, [Rule])
genStateRls sig g rl ts =
(g',rls)
where
(g',rls,_) =
foldr (\t (g, rs, n) ->
(let (g', new_rule) = f g t n in
(g', new_rule : rs, n+1)))
(g, [], (0 :: Int))
ts
-- vSpec t = ("strd", ["z"]) : varListSpecOfVars (varsInTerm t)
f g t n =
case varsUsedHeight rl (varsInTerm t) of
Missing v ->
error ("genStateRls: In gen-st of "
++ (rname rl) ++ ": no occurrence of "
++ (show (displayTerm (addToContext emptyContext [t]) v)))
FoundAt ht ->
(ruleOfDisjAtHeight
sig g rl ("gen-st-" ++ (rname rl) ++ "-" ++ (show n))
[ -- One disjunct, no existentially bound variables
([],
-- One conjunctor:
(\pvars ->
case envsRoleParams rl g pvars of
(_,e) : _ -> [GenStV (instantiate e t)]
[] -> error ("genStateRls: Parameter matching failed "
++ (show pvars) ++ (show t))))]
ht)
genFactRls :: Sig -> Gen -> Role -> [(String,[Term])] -> (Gen, [Rule])
genFactRls sig g rl predarglists =
(g',rls)
where
(g',rls,_) =
foldr (\(pred,args) (g, rs, n) ->
(let (g', new_rule) = f g pred args n in
(g', new_rule : rs, n+1)))
(g, [], (0 :: Int))
predarglists
-- vSpec t = ("strd", ["z"]) : varListSpecOfVars (varsInTerm t)
f g pred args n =
case varsUsedHeight rl (concatMap varsInTerm args) of
Missing v ->
error ("genFactRls: In fact of "
++ (rname rl) ++ ": no occurrence of "
++ (show $ varName v))
FoundAt ht ->
(ruleOfDisjAtHeight
sig g rl ("fact-" ++ (rname rl) ++ "-" ++ pred ++ (show n))
[ -- One disjunct, no existentially bound variables
([],
-- One conjunctor:
(\pvars ->
case envsRoleParams rl g pvars of
(_,e) : _ -> [AFact pred (map (instantiate e) args)]
_ -> error ("genFactRls: Parameter matching failed "
++ (show pvars) ++ (concatMap show args))))]
ht)
{--
(g',rls)
where
(g',rls,_) =
foldr (\(pred,args) (g, rs, n) ->
(let (g', new_rule) = f g pred args n in
(g', new_rule : rs, n+1)))
(g, [], (0 :: Integer))
predarglists
vSpec args = ("strd", ["z"]) : varListSpecOfVars (varsInArgs args)
varsInArgs = concatMap varsInTerm
f g pred args n =
case varsUsedHeight rl (varsInArgs args) of
Missing v -> error ("genFactRls: Unbound variable " ++ (show v)
++ " in fact of " ++ (rname rl) ++ ": "
++ pred ++ (show args))
FoundAt ht ->
ruleOfClauses sig g
("fact-" ++ (rname rl) ++ "-" ++ pred ++ (show n))
(vSpec args)
(\vars ->
applyToStrandVarAndParams
(\z pvars ->
(Length rl z (indxOfInt ht))
: (map
(\v ->
case paramOfName (varName v) rl of
Nothing -> error ("genFactRls: Parameter " ++
(varName v) ++ " not found.")
Just p ->
case firstOccurs p rl of
Nothing -> error ("genFactRls: Parameter " ++
(varName v) ++ " not found.")
Just i -> (Param rl p (i+1) z v))
pvars))
vars
"genFactRls: vars not strand+params?")
[([],
(\_ vars ->
applyToStrandVarAndParams
(\_ pvars ->
case envsRoleParams rl g [] pvars of
[(_,e)] -> [AFact pred (map (instantiate e) args)]
_ -> error "genFactRls: Non-unary matching not implemented")
vars
"genFactRls: vars not strand+params?"))]
--}
theVacuousRule :: Rule
theVacuousRule =
(Rule { rlname = "vacuity",
rlgoal = Goal {uvars = [],
antec = [],
consq = [([], [])], -- no bvs, no conjuncts
concl = [[]]},
rlcomment = [] })
scissorsRule :: Sig -> Gen -> (Gen, Rule)
scissorsRule sig g =
case sortedVarsOfNames sig g "strd" ["z0","z1","z2"] of
(g, [z0,z1,z2]) ->
case sortedVarsOfNames sig g "indx" ["i0","i1","i2"] of
(g, [i0,i1,i2]) ->
(g, (Rule { rlname = "scissorsRule",
rlgoal =
Goal
{uvars = [z0,z1,z2,i0,i1,i2],
antec = [ -- useful for debugging:
-- (AFact "no-state-split" []),
(Trans (z0,i0)), (Trans (z1,i1)), (Trans (z2,i2)),
(LeadsTo (z0,i0) (z1,i1)), (LeadsTo (z0,i0) (z2,i2)) ],
consq = [([], -- no bvs
[(Equals z1 z2), -- two eqns
(Equals i1 i2)])],
concl = [[(Equals z1 z2), -- two eqns
(Equals i1 i2)]]},
rlcomment = [] }))
(g, _) -> (g, theVacuousRule)
(g, _) -> (g, theVacuousRule)
shearsRule :: Sig -> Gen -> (Gen, Rule)
shearsRule sig g =
case sortedVarsOfNames sig g "strd" ["z0","z1","z2"] of
(g, [z0,z1,z2]) ->
case sortedVarsOfNames sig g "indx" ["i0","i1","i2"] of
(g, [i0,i1,i2]) ->
(g, (Rule { rlname = "shearsRule",
rlgoal =
Goal
{uvars = [z0,z1,z2,i0,i1,i2],
antec = [ -- useful for debugging:
-- (AFact "no-state-split" []),
(Trans (z0,i0)), (Trans (z1,i1)), (Trans (z2,i2)),
(LeadsTo (z0,i0) (z1,i1)), (SameLocn (z0,i0) (z2,i2)),
(Prec (z0,i0) (z2,i2)) ],
consq = [([], -- no bvs
[(Equals z1 z2), -- two eqns
(Equals i1 i2)]),
([], -- no bvs
-- (z1,i1) precedes (z2,i2)
[(Prec (z1, i1) (z2, i2))])],
concl = [[(Equals z1 z2), -- two eqns
(Equals i1 i2)],
-- (z1,i1) precedes (z2,i2)
[(Prec (z1, i1) (z2, i2))]]},
rlcomment = [] }))
(g, _) -> (g, theVacuousRule)
(g, _) -> (g, theVacuousRule)
invShearsRule :: Sig -> Gen -> (Gen, Rule)
invShearsRule sig g =
case sortedVarsOfNames sig g "strd" ["z0","z1","z2"] of
(g, [z0,z1,z2]) ->
case sortedVarsOfNames sig g "indx" ["i0","i1","i2"] of
(g, [i0,i1,i2]) ->
(g, (Rule { rlname = "invShearsRule",
rlgoal =
Goal
{uvars = [z0,z1,z2,i0,i1,i2],
antec = [ -- useful for debugging:
-- (AFact "no-state-split" []),
(Trans (z0,i0)), (Trans (z1,i1)),
(SameLocn (z0,i0) (z1,i1)),
(LeadsTo (z1,i1) (z2,i2)), (Prec (z0,i0) (z2,i2)) ],
consq = [([], -- no bvs
[(Equals z0 z1), -- two eqns
(Equals i0 i1)]),
([], -- no bvs
-- (z0, i0) precedes (z1,i1)
[(Prec (z0, i0) (z1, i1))])],
concl = [[(Equals z0 z1), -- two eqns
(Equals i0 i1)],
-- (z0, i0) precedes (z1,i1)
[(Prec (z0, i0) (z1, i1))]]},
rlcomment = [] }))
(g, _) -> (g, theVacuousRule)
(g, _) -> (g, theVacuousRule)
uninterruptibleRule :: Sig -> Gen -> (Gen, Rule)
uninterruptibleRule sig g =
case sortedVarsOfNames sig g "strd" ["z0","z1","z2"] of
(g, [z0,z1,z2]) ->
case sortedVarsOfNames sig g "indx" ["i0","i1","i2"] of
(g, [i0,i1,i2]) ->
(g,
(Rule { rlname = "no-interruption",
rlgoal =
Goal
{uvars = [z0,z1,z2,i0,i1,i2],
antec = [ (LeadsTo (z0,i0) (z2,i2)), (Trans (z1,i1)),
(SameLocn (z0,i0) (z1,i1)), (Prec (z0,i0) (z1,i1)),
(Prec (z1,i1) (z2,i2)) ],
consq = [], -- implies False
concl = []},
rlcomment = [] }))
(g, _) -> (g, theVacuousRule)
(g, _) -> (g, theVacuousRule)
cakeRule :: Sig -> Gen -> (Gen, Rule)
cakeRule sig g =
case sortedVarsOfNames sig g "strd" ["z0","z1","z2"] of
(g, [z0,z1,z2]) ->
case sortedVarsOfNames sig g "indx" ["i0","i1","i2"] of
(g, [i0,i1,i2]) ->
(g,
(Rule { rlname = "cakeRule",
rlgoal =
Goal
{uvars = [z0,z1,z2,i0,i1,i2],
antec = [ (Trans (z0,i0)), (Trans (z1,i1)),
(LeadsTo (z0,i0) (z1,i1)), (LeadsTo (z0,i0) (z2,i2)),
(Prec (z1,i1) (z2,i2)) ],
consq = [], -- implies False
concl = []},
rlcomment = [] }))
(g, _) -> (g, theVacuousRule)
(g, _) -> (g, theVacuousRule)