From be95f90d7d2adfaf399a3e79765f67feb265f1be Mon Sep 17 00:00:00 2001 From: swiesner Date: Tue, 23 Aug 2022 21:17:00 +0200 Subject: [PATCH 01/19] Adds support for non-linear restrictions e.g. Neq(x,x) ==> F, where arguments of a fact are literals. Non-linear arguments are linearized e.g. the above restriction becomes Neq(x, y) ==> (x == y) ==> F. --- .../src/isabelleGeneratedCode/Arith.hs | 26 +- .../GenericHelperFunctions.hs | 19 +- .../src/isabelleGeneratedCode/IoSpecs.hs | 11 +- .../src/isabelleGeneratedCode/List.hs | 11 +- .../src/isabelleGeneratedCode/Restrictions.hs | 276 +++++++++++++++--- 5 files changed, 276 insertions(+), 67 deletions(-) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Arith.hs b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Arith.hs index a7eea57..3e42e98 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Arith.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Arith.hs @@ -1,7 +1,7 @@ {-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-} module - Arith(Nat, Num(..), integer_of_nat, plus_nat, one_nat, suc, less_nat, + Arith(Nat, integer_of_nat, less_nat, Num(..), plus_nat, one_nat, suc, zero_nat, nat_of_integer, equal_nat, minus_nat, divide_nat, modulo_nat) where { @@ -15,18 +15,29 @@ import qualified ForeignImports; import qualified Product_Type; import qualified Orderings; +newtype Nat = Nat Integer deriving (Prelude.Read, Prelude.Show); + +integer_of_nat :: Nat -> Integer; +integer_of_nat (Nat x) = x; + +less_eq_nat :: Nat -> Nat -> Bool; +less_eq_nat m n = integer_of_nat m <= integer_of_nat n; + +less_nat :: Nat -> Nat -> Bool; +less_nat m n = integer_of_nat m < integer_of_nat n; + +instance Orderings.Ord Nat where { + less_eq = less_eq_nat; + less = less_nat; +}; + instance Orderings.Ord Integer where { less_eq = (\ a b -> a <= b); less = (\ a b -> a < b); }; -newtype Nat = Nat Integer deriving (Prelude.Read, Prelude.Show); - data Num = One | Bit0 Num | Bit1 Num deriving (Prelude.Read, Prelude.Show); -integer_of_nat :: Nat -> Integer; -integer_of_nat (Nat x) = x; - plus_nat :: Nat -> Nat -> Nat; plus_nat m n = Nat (integer_of_nat m + integer_of_nat n); @@ -36,9 +47,6 @@ one_nat = Nat (1 :: Integer); suc :: Nat -> Nat; suc n = plus_nat n one_nat; -less_nat :: Nat -> Nat -> Bool; -less_nat m n = integer_of_nat m < integer_of_nat n; - zero_nat :: Nat; zero_nat = Nat (0 :: Integer); diff --git a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/GenericHelperFunctions.hs b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/GenericHelperFunctions.hs index 5f79b2b..4a72185 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/GenericHelperFunctions.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/GenericHelperFunctions.hs @@ -1,11 +1,11 @@ {-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-} module - GenericHelperFunctions(anya, nubBy, nub, enum, isSome, fstList, sndList, - zipWith, flipPair, collectThe, stringOfNat, - splitAndGetFst, splitAndGetSnd, prependToString, - sortIntoBucketsOrdered, sortIntoBuckets, - stringOfInteger) + GenericHelperFunctions(anya, nubBy, nub, enum, scanl, isSome, fstList, + sndList, uncurry, zipWith, flipPair, collectThe, + stringOfNat, splitAndGetFst, splitAndGetSnd, + prependToString, sortIntoBucketsOrdered, + sortIntoBuckets, stringOfInteger) where { import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**), @@ -36,6 +36,12 @@ enum :: forall a. Arith.Nat -> [a] -> [(Arith.Nat, a)]; enum uu [] = []; enum i (x : xs) = (i, x) : enum (Arith.plus_nat i Arith.one_nat) xs; +scanl :: forall a b. (a -> b -> a) -> a -> [b] -> [a]; +scanl f s ls = s : (case ls of { + [] -> []; + x : a -> scanl f (f s x) a; + }); + unzip :: forall a b. [(a, b)] -> ([a], [b]); unzip inp = let { splitPair = (\ p ps -> (fst p : fst ps, snd p : snd ps)); @@ -51,6 +57,9 @@ fstList pairList = fst (unzip pairList); sndList :: forall a b. [(a, b)] -> [b]; sndList pairList = snd (unzip pairList); +uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c; +uncurry f p = f (fst p) (snd p); + zipWith :: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]; zipWith uu [] uv = []; zipWith uw (v : va) [] = []; diff --git a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/IoSpecs.hs b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/IoSpecs.hs index a1faeaf..5aff7f4 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/IoSpecs.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/IoSpecs.hs @@ -209,7 +209,7 @@ termUptSt lp rp state = TamiglooDatatypes.IOSTermSetOp TamiglooDatatypes.UpdateSt [lp, rp, state]; predPhiR :: - [(TamiglooDatatypes.Fact, TamiglooDatatypes.RestrFormula)] -> + [TamiglooDatatypes.RestrFormula] -> String -> TamiglooDatatypes.Rule -> TamiglooDatatypes.IOSFormula; predPhiR restrs role rule = let { @@ -364,7 +364,7 @@ isAbsPredPhiR (TamiglooDatatypes.IOSFex v va) = error "undefined"; isAbsPredPhiR (TamiglooDatatypes.IOSFfa v va) = error "undefined"; expandPredPhi :: - [(TamiglooDatatypes.Fact, TamiglooDatatypes.RestrFormula)] -> + [TamiglooDatatypes.RestrFormula] -> (String, (TamiglooDatatypes.Rule, TamiglooDatatypes.IOSFormula)) -> (TamiglooDatatypes.IOSFormula, TamiglooDatatypes.IOSFormula); expandPredPhi restrs t = @@ -379,7 +379,7 @@ expandPredPhi restrs t = else error "undefined"))); getRolesIOSpec :: - [(TamiglooDatatypes.Fact, TamiglooDatatypes.RestrFormula)] -> + [TamiglooDatatypes.RestrFormula] -> (String, ([TamiglooDatatypes.Rule], ([TamiglooDatatypes.Rule], [TamiglooDatatypes.Rule]))) -> @@ -409,9 +409,8 @@ extractIOSpec :: [(TamiglooDatatypes.IOSFormula, TamiglooDatatypes.IOSFormula)])))]; extractIOSpec thy = let { - sepRestrs = - map Restrictions.separateRestr (TamiglooDatatypes.extractRestrs thy); - } in List.foldr (\ a -> (\ b -> getRolesIOSpec sepRestrs a : b)) + restrs = TamiglooDatatypes.extractRestrs thy; + } in List.foldr (\ a -> (\ b -> getRolesIOSpec restrs a : b)) (Decomposition.extractProtoAndIoRules thy) []; getAbsPWithDef :: diff --git a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/List.hs b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/List.hs index 09635a5..6f5e881 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/List.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/List.hs @@ -1,6 +1,8 @@ {-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-} -module List(upt, fold, foldl, foldr, hd, tl, replicate, map_filter, size_list) +module + List(upt, fold, last, foldl, foldr, butlast, hd, tl, replicate, map_filter, + size_list) where { import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**), @@ -20,6 +22,9 @@ fold :: forall a b. (a -> b -> b) -> [a] -> b -> b; fold f (x : xs) s = fold f xs (f x s); fold f [] s = s; +last :: forall a. [a] -> a; +last (x : xs) = (if null xs then x else last xs); + foldl :: forall a b. (a -> b -> a) -> a -> [b] -> a; foldl f a [] = a; foldl f a (x : xs) = foldl f (f a x) xs; @@ -28,6 +33,10 @@ foldr :: forall a b. (a -> b -> b) -> [a] -> b -> b; foldr f [] = id; foldr f (x : xs) = f x . foldr f xs; +butlast :: forall a. [a] -> [a]; +butlast [] = []; +butlast (x : xs) = (if null xs then [] else x : butlast xs); + hd :: forall a. [a] -> a; hd (x21 : x22) = x21; diff --git a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs index d18b492..4157b0c 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs @@ -1,6 +1,6 @@ {-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-} -module Restrictions(ruleRestrs, separateRestr, iosfRestrictions) where { +module Restrictions(ruleRestrs, iosfRestrictions) where { import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**), (>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq, @@ -9,20 +9,14 @@ import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**), String, Bool(True, False), Maybe(Nothing, Just)); import qualified Prelude; import qualified ForeignImports; -import qualified Arith; -import qualified List; +import qualified Option; +import qualified Orderings; import qualified HOL; +import qualified List; +import qualified Arith; import qualified GenericHelperFunctions; import qualified TamiglooDatatypes; -isDbi :: - ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> - Bool; -isDbi (ForeignImports.LIT (ForeignImports.Var (ForeignImports.LVar name lsort i))) - = (if name == "Bound" then True else False); -isDbi (ForeignImports.LIT (ForeignImports.Con va)) = False; -isDbi (ForeignImports.FAPP v va) = False; - getDbiLit :: ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> Integer; @@ -32,11 +26,20 @@ getDbiLit getDbiLit (ForeignImports.LIT (ForeignImports.Con va)) = error "undefined"; getDbiLit (ForeignImports.FAPP v va) = error "undefined"; +isDbiLit :: + ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> + Bool; +isDbiLit + (ForeignImports.LIT (ForeignImports.Var (ForeignImports.LVar name lsort i))) = + (if name == "Bound" then True else False); +isDbiLit (ForeignImports.LIT (ForeignImports.Con va)) = False; +isDbiLit (ForeignImports.FAPP v va) = False; + safeGetDbiLit :: ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> Maybe Integer; safeGetDbiLit lnTerm = - (if isDbi lnTerm then Just (getDbiLit lnTerm) else Nothing); + (if isDbiLit lnTerm then Just (getDbiLit lnTerm) else Nothing); getDbis :: ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> @@ -47,6 +50,13 @@ getDbis lnTerm = TamiglooDatatypes.getVarsVTerm) lnTerm; +restrConj :: + [TamiglooDatatypes.RestrFormula] -> Maybe TamiglooDatatypes.RestrFormula; +restrConj fs = + (if Arith.equal_nat (List.size_list fs) Arith.zero_nat then Nothing + else Just (List.foldr (TamiglooDatatypes.Conn ForeignImports.And) + (List.butlast fs) (List.last fs))); + replaceDbiLNTerm :: Integer -> ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> @@ -55,7 +65,7 @@ replaceDbiLNTerm :: replaceDbiLNTerm i repl original = (case original of { ForeignImports.LIT _ -> - (if isDbi original && i == getDbiLit original then repl else original); + (if isDbiLit original && i == getDbiLit original then repl else original); ForeignImports.FAPP fun ts -> ForeignImports.FAPP fun (map (replaceDbiLNTerm i repl) ts); }); @@ -66,7 +76,9 @@ replaceDbiAtom :: TamiglooDatatypes.Atom -> TamiglooDatatypes.Atom; replaceDbiAtom i t a = (case a of { - TamiglooDatatypes.Atom _ -> a; + TamiglooDatatypes.Atom (TamiglooDatatypes.Fact fg ft ts) -> + TamiglooDatatypes.Atom + (TamiglooDatatypes.Fact fg ft (map (replaceDbiLNTerm i t) ts)); TamiglooDatatypes.EqE t1 t2 -> TamiglooDatatypes.EqE (replaceDbiLNTerm i t t1) (replaceDbiLNTerm i t t2); TamiglooDatatypes.TF _ -> a; @@ -84,41 +96,61 @@ replaceDbi i t f = TamiglooDatatypes.Conn conn (replaceDbi i t l) (replaceDbi i t r); }); -instantiateRestr :: - TamiglooDatatypes.Fact -> - (TamiglooDatatypes.Fact, TamiglooDatatypes.RestrFormula) -> - TamiglooDatatypes.RestrFormula; -instantiateRestr f def = - (if TamiglooDatatypes.eqFactSig f (fst def) - then let { - lnTerms = TamiglooDatatypes.accTermList f; - dbis = - GenericHelperFunctions.nub - (concatMap getDbis (TamiglooDatatypes.accTermList (fst def))); - zipped = zip dbis lnTerms; - } in List.fold (\ p -> replaceDbi (fst p) (snd p)) zipped (snd def) - else error "undefined"); +instantiateWithMapping :: + [(Integer, + ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar))] -> + TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; +instantiateWithMapping instMap restrDef = + List.fold (GenericHelperFunctions.uncurry replaceDbi) instMap restrDef; -instantiateRestrictions :: - [(TamiglooDatatypes.Fact, TamiglooDatatypes.RestrFormula)] -> - TamiglooDatatypes.Fact -> [TamiglooDatatypes.RestrFormula]; -instantiateRestrictions restrs actFact = - List.map_filter - (\ x -> - (if TamiglooDatatypes.eqFactSig actFact (fst x) - then Just (instantiateRestr actFact x) else Nothing)) - restrs; +instantiateDbiLNTerms :: + [(Integer, + ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar))] -> + ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> + ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar); +instantiateDbiLNTerms instMap lnTerm = + List.foldr (GenericHelperFunctions.uncurry replaceDbiLNTerm) instMap lnTerm; -factListRestrs :: - [TamiglooDatatypes.Fact] -> - [(TamiglooDatatypes.Fact, TamiglooDatatypes.RestrFormula)] -> - [TamiglooDatatypes.RestrFormula]; -factListRestrs acts restrs = concatMap (instantiateRestrictions restrs) acts; +dbiToBoundLNTerm :: + Integer -> + ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar); +dbiToBoundLNTerm i = + TamiglooDatatypes.varToVTerm + (ForeignImports.LVar "Bound" ForeignImports.LSortNode i); -ruleRestrs :: - [(TamiglooDatatypes.Fact, TamiglooDatatypes.RestrFormula)] -> - TamiglooDatatypes.Rule -> [TamiglooDatatypes.RestrFormula]; -ruleRestrs restrs r = factListRestrs (TamiglooDatatypes.accAc r) restrs; +getDbiLitsPerFactArg :: TamiglooDatatypes.Fact -> [[Integer]]; +getDbiLitsPerFactArg f = map getDbis (TamiglooDatatypes.accTermList f); + +flipEnumInt :: forall a. Arith.Nat -> [a] -> [(a, Integer)]; +flipEnumInt i ls = + map (\ p -> (snd p, Arith.integer_of_nat (fst p))) + (GenericHelperFunctions.enum i ls); + +perArgMapping :: TamiglooDatatypes.Fact -> [[(Integer, Integer)]]; +perArgMapping f = + let { + lens = map List.size_list (getDbiLitsPerFactArg f); + maxCapturedVars = + Arith.nat_of_integer + ((1 :: Integer) + + List.foldr Orderings.max (concat (getDbiLitsPerFactArg f)) + (0 :: Integer)); + minBounds = + map (Arith.plus_nat maxCapturedVars) + (List.butlast + (GenericHelperFunctions.scanl Arith.plus_nat Arith.zero_nat lens)); + a = zip minBounds (getDbiLitsPerFactArg f); + } in map (\ p -> flipEnumInt (fst p) (snd p)) a; + +factToDistinctDbis :: TamiglooDatatypes.Fact -> TamiglooDatatypes.Fact; +factToDistinctDbis (TamiglooDatatypes.Fact fg ft ts) = + let { + mapToLNTerm = + map (map (\ p -> (fst p, dbiToBoundLNTerm (snd p)))) + (perArgMapping (TamiglooDatatypes.Fact fg ft ts)); + zippedTs = zip mapToLNTerm ts; + a = map (\ p -> instantiateDbiLNTerms (fst p) (snd p)) zippedTs; + } in TamiglooDatatypes.Fact fg ft a; separateRestr :: TamiglooDatatypes.RestrFormula -> @@ -136,6 +168,158 @@ separateRestr (TamiglooDatatypes.Conn ForeignImports.Or va vb) = separateRestr (TamiglooDatatypes.Conn ForeignImports.Iff va vb) = error "undefined"; +combineRestr :: + (TamiglooDatatypes.Fact, TamiglooDatatypes.RestrFormula) -> + TamiglooDatatypes.RestrFormula; +combineRestr p = + TamiglooDatatypes.Conn ForeignImports.Imp + (TamiglooDatatypes.Ato (TamiglooDatatypes.Atom (fst p))) (snd p); + +getVarsAtom :: TamiglooDatatypes.Atom -> [ForeignImports.LVar]; +getVarsAtom (TamiglooDatatypes.Atom f) = + concatMap TamiglooDatatypes.getVarsVTerm (TamiglooDatatypes.accTermList f); +getVarsAtom (TamiglooDatatypes.EqE l r) = + TamiglooDatatypes.getVarsVTerm l ++ TamiglooDatatypes.getVarsVTerm r; +getVarsAtom (TamiglooDatatypes.TF v) = []; + +getVarsRestr :: + [ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar)] -> + TamiglooDatatypes.RestrFormula -> + [ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar)]; +getVarsRestr acc (TamiglooDatatypes.Ato atom) = + acc ++ map TamiglooDatatypes.varToVTerm (getVarsAtom atom); +getVarsRestr acc (TamiglooDatatypes.Not f) = getVarsRestr acc f; +getVarsRestr acc (TamiglooDatatypes.Conn uu l r) = + getVarsRestr (getVarsRestr acc l) r; + +mappingDbis :: TamiglooDatatypes.RestrFormula -> [(Integer, [Integer])]; +mappingDbis restr = + let { + sepRestr = separateRestr restr; + fact = fst sepRestr; + rhs = snd sepRestr; + perArgMap = perArgMapping fact; + catPerArg = concat perArgMap; + maxDbisLhs = + List.foldr (Orderings.max . Arith.nat_of_integer) + (GenericHelperFunctions.sndList catPerArg) Arith.zero_nat; + dbisRhs = + GenericHelperFunctions.collectThe + (map safeGetDbiLit (getVarsRestr [] rhs)); + dbisRhsNotInFact = + GenericHelperFunctions.nub + (List.foldr (\ a -> filter (\ b -> a == b)) + (GenericHelperFunctions.fstList catPerArg) dbisRhs); + _ = map (\ p -> (fst p, [snd p])) + (flipEnumInt (Arith.plus_nat maxDbisLhs Arith.one_nat) + dbisRhsNotInFact); + mergedArgMapping = GenericHelperFunctions.sortIntoBuckets catPerArg; + } in mergedArgMapping; + +restrToDistinctDbis :: + TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; +restrToDistinctDbis restr = + let { + sepRestr = separateRestr restr; + newFact = factToDistinctDbis (fst sepRestr); + newLNTermMap = + map (\ p -> (fst p, dbiToBoundLNTerm (snd p))) + (map (\ p -> (fst p, List.hd (snd p))) (mappingDbis restr)); + newRhs = instantiateWithMapping newLNTermMap (snd sepRestr); + } in combineRestr (newFact, newRhs); + +createEqCheckList :: + [ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar)] -> + [TamiglooDatatypes.RestrFormula]; +createEqCheckList lnTerms = + (case lnTerms of { + [] -> []; + [_] -> []; + x : y : zs -> + TamiglooDatatypes.Ato (TamiglooDatatypes.EqE x y) : + createEqCheckList (y : zs); + }); + +dbisCreateEqChecks :: [Integer] -> Maybe TamiglooDatatypes.RestrFormula; +dbisCreateEqChecks dbis = let { + a = createEqCheckList (map dbiToBoundLNTerm dbis); + } in restrConj a; + +createEqChecks :: + [(Integer, [Integer])] -> Maybe TamiglooDatatypes.RestrFormula; +createEqChecks oldToNewMap = + let { + perArgEqChecks = + GenericHelperFunctions.collectThe + (map dbisCreateEqChecks (GenericHelperFunctions.sndList oldToNewMap)); + } in (if Arith.equal_nat (List.size_list perArgEqChecks) Arith.zero_nat + then Nothing else restrConj perArgEqChecks); + +linearizeRestr :: + TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; +linearizeRestr restr = + let { + eqChecks = createEqChecks (mappingDbis restr); + sepNewRestr = separateRestr (restrToDistinctDbis restr); + rhs = (if GenericHelperFunctions.isSome eqChecks + then TamiglooDatatypes.Conn ForeignImports.Imp (Option.the eqChecks) + (snd sepNewRestr) + else snd sepNewRestr); + } in combineRestr (fst sepNewRestr, rhs); + +instantiationMapLNTerm :: + ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> + ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> + [(Integer, + ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar))]; +instantiationMapLNTerm (ForeignImports.LIT var) appTerm = + [(getDbiLit (ForeignImports.LIT var), appTerm)]; +instantiationMapLNTerm (ForeignImports.FAPP fs ts) uu = error "undefined"; + +instantiationMap :: + TamiglooDatatypes.Fact -> + TamiglooDatatypes.Fact -> + [(Integer, + ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar))]; +instantiationMap dbiFact appFact = + let { + dbiTermList = TamiglooDatatypes.accTermList dbiFact; + appTermList = TamiglooDatatypes.accTermList appFact; + } in concatMap (GenericHelperFunctions.uncurry instantiationMapLNTerm) + (zip dbiTermList appTermList); + +instantiateRestr :: + TamiglooDatatypes.Fact -> + TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; +instantiateRestr f def = let { + sepRestr = separateRestr def; + instMap = instantiationMap (fst sepRestr) f; + } in instantiateWithMapping instMap (snd sepRestr); + +eqFactRestr :: TamiglooDatatypes.Fact -> TamiglooDatatypes.RestrFormula -> Bool; +eqFactRestr f restr = TamiglooDatatypes.eqFactSig f (fst (separateRestr restr)); + +instantiateRestrictions :: + [TamiglooDatatypes.RestrFormula] -> + TamiglooDatatypes.Fact -> [TamiglooDatatypes.RestrFormula]; +instantiateRestrictions restrs actFact = + List.map_filter + (\ x -> + (if eqFactRestr actFact x then Just (instantiateRestr actFact x) + else Nothing)) + restrs; + +factListRestrs :: + [TamiglooDatatypes.Fact] -> + [TamiglooDatatypes.RestrFormula] -> [TamiglooDatatypes.RestrFormula]; +factListRestrs acts restrs = concatMap (instantiateRestrictions restrs) acts; + +ruleRestrs :: + [TamiglooDatatypes.RestrFormula] -> + TamiglooDatatypes.Rule -> [TamiglooDatatypes.RestrFormula]; +ruleRestrs restrs r = + factListRestrs (TamiglooDatatypes.accAc r) (map linearizeRestr restrs); + iosfRestrictions :: [TamiglooDatatypes.RestrFormula] -> TamiglooDatatypes.IOSFormula; iosfRestrictions restrs = From 4281bc279b26bd6468892ee9c91f89cbcdfc8daa Mon Sep 17 00:00:00 2001 From: swiesner Date: Wed, 24 Aug 2022 16:32:54 +0200 Subject: [PATCH 02/19] Adds support for restriction definitions with pattern matching to Gobra backend (error message for verifast). --- .../src/PrettyIOSpecs/Gobra/IOSpecs.hs | 9 ++ .../src/PrettyIOSpecs/Gobra/Utils.hs | 3 +- .../src/PrettyIOSpecs/VeriFast/IOSpecs.hs | 29 ++++- .../src/isabelleGeneratedCode/Restrictions.hs | 100 ++++++++++++++++-- .../TamiglooDatatypes.hs | 2 + 5 files changed, 133 insertions(+), 10 deletions(-) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs index 8dc3a02..919cd9e 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs @@ -128,6 +128,15 @@ prettyRestrForm :: Document d => TID.RestrFormula -> d prettyRestrForm (TID.Ato atom) = prettyAtom atom prettyRestrForm (TID.Not f) = text "!(" <> prettyRestrForm f <> text ")" prettyRestrForm (TID.Conn conn l r) = parens (prettyRestrForm l) <> text (showConn conn) <> parens (prettyRestrForm r) +prettyRestrForm (TID.REX t f) = text "(" <> (connectREX [t] f) <> text ")" + where + connectREX :: Document d => [T.LNTerm] -> TID.RestrFormula -> d + connectREX qs (TID.REX v formula) = connectREX (qs ++ [v]) formula + connectREX qs formula = + exists + (hcat . punctuate (text ", ") $ map (text . prettyGobraLNTermWithType) qs) + (prettyRestrForm formula) + prettyAtom :: Document d => TID.Atom -> d prettyAtom (TID.Atom f) = text (prettyFact True f) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs index eaa4c6e..32710a9 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs @@ -8,6 +8,7 @@ module PrettyIOSpecs.Gobra.Utils ( , gobraHeader , domain + , exists , forallWithTriggerSetting , axiom @@ -320,10 +321,8 @@ forallWithTriggerSetting :: Document d => TriggerSetting -> d -> [d] -> d -> d forallWithTriggerSetting = quantifiedWithTriggerSetting "forall" -{- exists :: Document d => d -> d -> d exists termsWithType body = quantifiedWithTriggerSetting "exists" None termsWithType [] body --} quantifiedWithTriggerSetting :: Document d => String -> TriggerSetting -> d -> [d] -> d -> d quantifiedWithTriggerSetting quant triggerSetting termsWithType triggers body = diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/IOSpecs.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/IOSpecs.hs index 8ed0ca6..6fbd890 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/IOSpecs.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/IOSpecs.hs @@ -14,6 +14,8 @@ import Prelude import qualified Data.Map as Map import Text.PrettyPrint.Class import Data.List(delete) +import Data.List.Split + import qualified Theory as T import qualified Theory.Model.Formula as Form @@ -152,7 +154,7 @@ prettyVFIOSFormula f = -- restrictions -{- +{- only for debugging prettyVFRestrs :: Document d => TID.Theory -> d prettyVFRestrs (TID.Theory _ _ thyItems) = text "==== Restrictions ==========\n" $$ @@ -165,10 +167,33 @@ prettyVFRestrs (TID.Theory _ _ thyItems) = getRestrName :: TID.TheoryItem -> String getRestrName (TID.RestrItem name _) = name -} + + + prettyRestrForm :: Document d => TID.RestrFormula -> d prettyRestrForm (TID.Ato atom) = prettyAtom atom prettyRestrForm (TID.Not f) = text "!(" <> prettyRestrForm f <> text ")" prettyRestrForm (TID.Conn conn l r) = prettyConn conn (parens (prettyRestrForm l)) (parens (prettyRestrForm r)) +prettyRestrForm (TID.REX t f) = error "Patterns in definitions of restrictions not supported in VeriFast." -- text "(" <> (connectREX [t] f) <> text ")" + where + connectREX :: Document d => [T.LNTerm] -> TID.RestrFormula -> d + connectREX qs (TID.REX v formula) = connectREX (qs ++ [v]) formula + connectREX qs formula = exQuantFirst (map (prettyVFLNTerm True) qs) (prettyRestrForm formula) + -- copied from Main.Console + renderDoc :: Doc -> String + renderDoc = renderStyle (defaultStyle) + -- not ideal but have to prepend '?' to first occurence of existentially quanitified vars + exQuantFirst :: Document d => [String] -> Doc -> d + exQuantFirst qs df = text $ foldr (\a b -> auxEQF a b) (renderDoc df) qs + auxEQF :: String -> String -> String + auxEQF q s = + (concat $ auxChangeFirst q $ split (onSublist q) s) + auxChangeFirst :: String -> [String] -> [String] + auxChangeFirst _ [] = [] + auxChangeFirst q (x:xs) = + if x == q + then ("?"++x) : xs + else x : (auxChangeFirst q xs) prettyAtom :: Document d => TID.Atom -> d prettyAtom (TID.Atom f) = text (prettyFact True f) @@ -176,7 +201,7 @@ prettyAtom (TID.EqE t1 t2) = text (prettyVFLNTerm True t1) <> text " == " <> tex prettyAtom (TID.TF b) = if b then text "true" else text "false" prettyConn :: Document d => Form.Connective -> d -> d -> d -prettyConn Form.And l r = l <> text " && " <> r +prettyConn Form.And l r = l <> text " &&" $$ r prettyConn Form.Or l r = l <> text " || " <> r prettyConn Form.Imp l r = l <> text " ? " <> r <> text " : true" prettyConn Form.Iff l r = l <> text " == " <> r diff --git a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs index 4157b0c..a68e53b 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs @@ -12,11 +12,19 @@ import qualified ForeignImports; import qualified Option; import qualified Orderings; import qualified HOL; -import qualified List; import qualified Arith; +import qualified List; import qualified GenericHelperFunctions; import qualified TamiglooDatatypes; +isFAPP :: + ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> + Bool; +isFAPP t = (case t of { + ForeignImports.LIT _ -> False; + ForeignImports.FAPP _ _ -> True; + }); + getDbiLit :: ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> Integer; @@ -50,6 +58,17 @@ getDbis lnTerm = TamiglooDatatypes.getVarsVTerm) lnTerm; +hasFAPP :: TamiglooDatatypes.Fact -> Bool; +hasFAPP f = + List.foldr (\ t -> (\ a -> isFAPP t || a)) (TamiglooDatatypes.accTermList f) + False; + +dbiToREX :: + Integer -> + ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar); +dbiToREX i = + ForeignImports.LIT (ForeignImports.Var (ForeignImports.LVar "rEX" ForeignImports.LSortMsg i)); + restrConj :: [TamiglooDatatypes.RestrFormula] -> Maybe TamiglooDatatypes.RestrFormula; restrConj fs = @@ -57,6 +76,32 @@ restrConj fs = else Just (List.foldr (TamiglooDatatypes.Conn ForeignImports.And) (List.butlast fs) (List.last fs))); +unwrapREX :: TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; +unwrapREX (TamiglooDatatypes.REX uu f) = unwrapREX f; +unwrapREX (TamiglooDatatypes.Ato v) = TamiglooDatatypes.Ato v; +unwrapREX (TamiglooDatatypes.Not v) = TamiglooDatatypes.Not v; +unwrapREX (TamiglooDatatypes.Conn v va vb) = TamiglooDatatypes.Conn v va vb; + +wrapInREX :: + [ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar)] -> + TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; +wrapInREX [] f = f; +wrapInREX (t : ts) f = TamiglooDatatypes.REX t (wrapInREX ts f); + +mappingREX :: + TamiglooDatatypes.Fact -> + [(Integer, + ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar))]; +mappingREX f = + let { + dbis = + GenericHelperFunctions.nub + (concat + (List.map_filter + (\ x -> (if isFAPP x then Just (getDbis x) else Nothing)) + (TamiglooDatatypes.accTermList f))); + } in zip dbis (map dbiToREX dbis); + replaceDbiLNTerm :: Integer -> ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> @@ -167,6 +212,7 @@ separateRestr (TamiglooDatatypes.Conn ForeignImports.Or va vb) = error "undefined"; separateRestr (TamiglooDatatypes.Conn ForeignImports.Iff va vb) = error "undefined"; +separateRestr (TamiglooDatatypes.REX v va) = error "undefined"; combineRestr :: (TamiglooDatatypes.Fact, TamiglooDatatypes.RestrFormula) -> @@ -267,6 +313,20 @@ linearizeRestr restr = else snd sepNewRestr); } in combineRestr (fst sepNewRestr, rhs); +createEqPatternREX :: + TamiglooDatatypes.Fact -> + TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; +createEqPatternREX actFact restrREX = + let { + defFactTerms = + TamiglooDatatypes.accTermList (fst (separateRestr (unwrapREX restrREX))); + actFactTerms = TamiglooDatatypes.accTermList actFact; + zipFAPPActDefTerms = filter (isFAPP . snd) (zip actFactTerms defFactTerms); + eqs = map (\ p -> + TamiglooDatatypes.Ato (TamiglooDatatypes.EqE (fst p) (snd p))) + zipFAPPActDefTerms; + } in Option.the (restrConj eqs); + instantiationMapLNTerm :: ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar) -> @@ -274,7 +334,7 @@ instantiationMapLNTerm :: ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar))]; instantiationMapLNTerm (ForeignImports.LIT var) appTerm = [(getDbiLit (ForeignImports.LIT var), appTerm)]; -instantiationMapLNTerm (ForeignImports.FAPP fs ts) uu = error "undefined"; +instantiationMapLNTerm (ForeignImports.FAPP fs ts) uu = []; instantiationMap :: TamiglooDatatypes.Fact -> @@ -288,13 +348,41 @@ instantiationMap dbiFact appFact = } in concatMap (GenericHelperFunctions.uncurry instantiationMapLNTerm) (zip dbiTermList appTermList); +createRestrREX :: + TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; +createRestrREX restr = + let { + sepRestr = separateRestr restr; + rexMap = mappingREX (fst sepRestr); + a = List.fold (GenericHelperFunctions.uncurry replaceDbi) rexMap restr; + } in wrapInREX (GenericHelperFunctions.sndList rexMap) a; + +instantiateHasFAPP :: + TamiglooDatatypes.Fact -> + TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; +instantiateHasFAPP actFact linRestr = + let { + restrREX = createRestrREX linRestr; + eqsPattern = createEqPatternREX actFact restrREX; + unwrapRestrREX = separateRestr (unwrapREX restrREX); + restrREXwithEq = + TamiglooDatatypes.Conn ForeignImports.Imp eqsPattern (snd unwrapRestrREX); + instMap = instantiationMap (fst (separateRestr linRestr)) actFact; + instRestr = instantiateWithMapping instMap restrREXwithEq; + rexVars = + GenericHelperFunctions.sndList + (mappingREX (fst (separateRestr linRestr))); + } in wrapInREX rexVars instRestr; + instantiateRestr :: TamiglooDatatypes.Fact -> TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; -instantiateRestr f def = let { - sepRestr = separateRestr def; - instMap = instantiationMap (fst sepRestr) f; - } in instantiateWithMapping instMap (snd sepRestr); +instantiateRestr f def = + let { + sepRestr = separateRestr def; + instMap = instantiationMap (fst sepRestr) f; + } in (if hasFAPP (fst sepRestr) then instantiateHasFAPP f def + else instantiateWithMapping instMap (snd sepRestr)); eqFactRestr :: TamiglooDatatypes.Fact -> TamiglooDatatypes.RestrFormula -> Bool; eqFactRestr f restr = TamiglooDatatypes.eqFactSig f (fst (separateRestr restr)); diff --git a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/TamiglooDatatypes.hs b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/TamiglooDatatypes.hs index 396d8d1..9466743 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/TamiglooDatatypes.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/TamiglooDatatypes.hs @@ -163,6 +163,8 @@ data Rule = Rule RuleGroup String [Fact] [Fact] [Fact] data RestrFormula = Ato Atom | Not RestrFormula | Conn ForeignImports.Connective RestrFormula RestrFormula + | REX (ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar)) + RestrFormula deriving (Prelude.Show); data TheoryItem = RuleItem Rule | TextItem (String, String) From 158572a6ba4cd1ae8fcbe473b70b80115d75cfee Mon Sep 17 00:00:00 2001 From: swiesner Date: Wed, 24 Aug 2022 22:06:00 +0200 Subject: [PATCH 03/19] Fixes bug: changes restrExists to restrForALl. --- .../src/PrettyIOSpecs/Gobra/IOSpecs.hs | 13 ++-- .../src/PrettyIOSpecs/VeriFast/IOSpecs.hs | 10 +-- .../src/isabelleGeneratedCode/Restrictions.hs | 64 +++++++++---------- .../TamiglooDatatypes.hs | 2 +- 4 files changed, 46 insertions(+), 43 deletions(-) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs index 919cd9e..74b102b 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs @@ -128,13 +128,14 @@ prettyRestrForm :: Document d => TID.RestrFormula -> d prettyRestrForm (TID.Ato atom) = prettyAtom atom prettyRestrForm (TID.Not f) = text "!(" <> prettyRestrForm f <> text ")" prettyRestrForm (TID.Conn conn l r) = parens (prettyRestrForm l) <> text (showConn conn) <> parens (prettyRestrForm r) -prettyRestrForm (TID.REX t f) = text "(" <> (connectREX [t] f) <> text ")" +prettyRestrForm (TID.RFA t f) = text "(" <> (connectRFA [t] f) <> text ")" where - connectREX :: Document d => [T.LNTerm] -> TID.RestrFormula -> d - connectREX qs (TID.REX v formula) = connectREX (qs ++ [v]) formula - connectREX qs formula = - exists - (hcat . punctuate (text ", ") $ map (text . prettyGobraLNTermWithType) qs) + connectRFA :: Document d => [T.LNTerm] -> TID.RestrFormula -> d + connectRFA qs (TID.RFA v formula) = connectRFA (qs ++ [v]) formula + connectRFA qs formula = + forallWithTriggerSetting None + (hcat . punctuate (text ", ") $ map (text . prettyGobraLNTermWithType) qs) + [] (prettyRestrForm formula) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/IOSpecs.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/IOSpecs.hs index 6fbd890..1b3f421 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/IOSpecs.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/IOSpecs.hs @@ -174,11 +174,12 @@ prettyRestrForm :: Document d => TID.RestrFormula -> d prettyRestrForm (TID.Ato atom) = prettyAtom atom prettyRestrForm (TID.Not f) = text "!(" <> prettyRestrForm f <> text ")" prettyRestrForm (TID.Conn conn l r) = prettyConn conn (parens (prettyRestrForm l)) (parens (prettyRestrForm r)) -prettyRestrForm (TID.REX t f) = error "Patterns in definitions of restrictions not supported in VeriFast." -- text "(" <> (connectREX [t] f) <> text ")" +prettyRestrForm (TID.RFA t f) = error "Patterns in definitions of restrictions not supported in VeriFast." -- text "(" <> (connectRFA [t] f) <> text ")" + {- where - connectREX :: Document d => [T.LNTerm] -> TID.RestrFormula -> d - connectREX qs (TID.REX v formula) = connectREX (qs ++ [v]) formula - connectREX qs formula = exQuantFirst (map (prettyVFLNTerm True) qs) (prettyRestrForm formula) + connectRFA :: Document d => [T.LNTerm] -> TID.RestrFormula -> d + connectRFA qs (TID.REX v formula) = connectRFA (qs ++ [v]) formula + connectRFA qs formula = exQuantFirst (map (prettyVFLNTerm True) qs) (prettyRestrForm formula) -- copied from Main.Console renderDoc :: Doc -> String renderDoc = renderStyle (defaultStyle) @@ -194,6 +195,7 @@ prettyRestrForm (TID.REX t f) = error "Patterns in definitions of restrictions n if x == q then ("?"++x) : xs else x : (auxChangeFirst q xs) + -} prettyAtom :: Document d => TID.Atom -> d prettyAtom (TID.Atom f) = text (prettyFact True f) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs index a68e53b..4838cf8 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs @@ -63,11 +63,11 @@ hasFAPP f = List.foldr (\ t -> (\ a -> isFAPP t || a)) (TamiglooDatatypes.accTermList f) False; -dbiToREX :: +dbiToRFA :: Integer -> ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar); -dbiToREX i = - ForeignImports.LIT (ForeignImports.Var (ForeignImports.LVar "rEX" ForeignImports.LSortMsg i)); +dbiToRFA i = + ForeignImports.LIT (ForeignImports.Var (ForeignImports.LVar "rFA" ForeignImports.LSortMsg i)); restrConj :: [TamiglooDatatypes.RestrFormula] -> Maybe TamiglooDatatypes.RestrFormula; @@ -76,23 +76,23 @@ restrConj fs = else Just (List.foldr (TamiglooDatatypes.Conn ForeignImports.And) (List.butlast fs) (List.last fs))); -unwrapREX :: TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; -unwrapREX (TamiglooDatatypes.REX uu f) = unwrapREX f; -unwrapREX (TamiglooDatatypes.Ato v) = TamiglooDatatypes.Ato v; -unwrapREX (TamiglooDatatypes.Not v) = TamiglooDatatypes.Not v; -unwrapREX (TamiglooDatatypes.Conn v va vb) = TamiglooDatatypes.Conn v va vb; +unwrapRFA :: TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; +unwrapRFA (TamiglooDatatypes.RFA uu f) = unwrapRFA f; +unwrapRFA (TamiglooDatatypes.Ato v) = TamiglooDatatypes.Ato v; +unwrapRFA (TamiglooDatatypes.Not v) = TamiglooDatatypes.Not v; +unwrapRFA (TamiglooDatatypes.Conn v va vb) = TamiglooDatatypes.Conn v va vb; -wrapInREX :: +wrapInRFA :: [ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar)] -> TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; -wrapInREX [] f = f; -wrapInREX (t : ts) f = TamiglooDatatypes.REX t (wrapInREX ts f); +wrapInRFA [] f = f; +wrapInRFA (t : ts) f = TamiglooDatatypes.RFA t (wrapInRFA ts f); -mappingREX :: +mappingRFA :: TamiglooDatatypes.Fact -> [(Integer, ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar))]; -mappingREX f = +mappingRFA f = let { dbis = GenericHelperFunctions.nub @@ -100,7 +100,7 @@ mappingREX f = (List.map_filter (\ x -> (if isFAPP x then Just (getDbis x) else Nothing)) (TamiglooDatatypes.accTermList f))); - } in zip dbis (map dbiToREX dbis); + } in zip dbis (map dbiToRFA dbis); replaceDbiLNTerm :: Integer -> @@ -212,7 +212,7 @@ separateRestr (TamiglooDatatypes.Conn ForeignImports.Or va vb) = error "undefined"; separateRestr (TamiglooDatatypes.Conn ForeignImports.Iff va vb) = error "undefined"; -separateRestr (TamiglooDatatypes.REX v va) = error "undefined"; +separateRestr (TamiglooDatatypes.RFA v va) = error "undefined"; combineRestr :: (TamiglooDatatypes.Fact, TamiglooDatatypes.RestrFormula) -> @@ -313,13 +313,13 @@ linearizeRestr restr = else snd sepNewRestr); } in combineRestr (fst sepNewRestr, rhs); -createEqPatternREX :: +createEqPatternRFA :: TamiglooDatatypes.Fact -> TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; -createEqPatternREX actFact restrREX = +createEqPatternRFA actFact restrRFA = let { defFactTerms = - TamiglooDatatypes.accTermList (fst (separateRestr (unwrapREX restrREX))); + TamiglooDatatypes.accTermList (fst (separateRestr (unwrapRFA restrRFA))); actFactTerms = TamiglooDatatypes.accTermList actFact; zipFAPPActDefTerms = filter (isFAPP . snd) (zip actFactTerms defFactTerms); eqs = map (\ p -> @@ -348,31 +348,31 @@ instantiationMap dbiFact appFact = } in concatMap (GenericHelperFunctions.uncurry instantiationMapLNTerm) (zip dbiTermList appTermList); -createRestrREX :: +createRestrRFA :: TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; -createRestrREX restr = +createRestrRFA restr = let { sepRestr = separateRestr restr; - rexMap = mappingREX (fst sepRestr); - a = List.fold (GenericHelperFunctions.uncurry replaceDbi) rexMap restr; - } in wrapInREX (GenericHelperFunctions.sndList rexMap) a; + rFAMap = mappingRFA (fst sepRestr); + a = List.fold (GenericHelperFunctions.uncurry replaceDbi) rFAMap restr; + } in wrapInRFA (GenericHelperFunctions.sndList rFAMap) a; instantiateHasFAPP :: TamiglooDatatypes.Fact -> TamiglooDatatypes.RestrFormula -> TamiglooDatatypes.RestrFormula; instantiateHasFAPP actFact linRestr = let { - restrREX = createRestrREX linRestr; - eqsPattern = createEqPatternREX actFact restrREX; - unwrapRestrREX = separateRestr (unwrapREX restrREX); - restrREXwithEq = - TamiglooDatatypes.Conn ForeignImports.Imp eqsPattern (snd unwrapRestrREX); + restrRFA = createRestrRFA linRestr; + eqsPattern = createEqPatternRFA actFact restrRFA; + unwrapRestrRFA = separateRestr (unwrapRFA restrRFA); + restrRFAwithEq = + TamiglooDatatypes.Conn ForeignImports.Imp eqsPattern (snd unwrapRestrRFA); instMap = instantiationMap (fst (separateRestr linRestr)) actFact; - instRestr = instantiateWithMapping instMap restrREXwithEq; - rexVars = + instRestr = instantiateWithMapping instMap restrRFAwithEq; + rFAVars = GenericHelperFunctions.sndList - (mappingREX (fst (separateRestr linRestr))); - } in wrapInREX rexVars instRestr; + (mappingRFA (fst (separateRestr linRestr))); + } in wrapInRFA rFAVars instRestr; instantiateRestr :: TamiglooDatatypes.Fact -> diff --git a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/TamiglooDatatypes.hs b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/TamiglooDatatypes.hs index 9466743..7007af2 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/TamiglooDatatypes.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/TamiglooDatatypes.hs @@ -163,7 +163,7 @@ data Rule = Rule RuleGroup String [Fact] [Fact] [Fact] data RestrFormula = Ato Atom | Not RestrFormula | Conn ForeignImports.Connective RestrFormula RestrFormula - | REX (ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar)) + | RFA (ForeignImports.Term (ForeignImports.Lit ForeignImports.Name ForeignImports.LVar)) RestrFormula deriving (Prelude.Show); From a834f6dc1fa3ed0dffcd2bbfcc819bf1c63a1c65 Mon Sep 17 00:00:00 2001 From: swiesner Date: Sat, 27 Aug 2022 15:50:33 +0200 Subject: [PATCH 04/19] Generalize ppFunSym, and ppRule (Tern function encoding and equality encoding) to not just work for type 'Term' but for any given type (changes argument and return type). --- .../src/PrettyIOSpecs/Gobra/TermEncoding.hs | 58 ++++++++++--------- 1 file changed, 30 insertions(+), 28 deletions(-) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/TermEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/TermEncoding.hs index d2e7ddf..8025698 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/TermEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/TermEncoding.hs @@ -59,27 +59,30 @@ termFuncEncoding sigMaude = -- get function signatures from Maude signature funcSyms = S.toList (funSyms sigMaude) in - (vcat $ map ppFunSym funcSyms) $$ text "\n" - where - ppFunSym :: Document d => FunSym -> d - ppFunSym (NoEq (f, (ar, _))) = - -- we do not make a distinction between private and public since we don't consider the adversary - let - args = map (++ " Term") (convenienceNames ar "t") - in - text $ functionDef (reservedGobraWords (BC.unpack f)) args "Term" - ppFunSym (AC o) = - -- AC function symbols are made to be binary - -- This needs to happen in function declaration and application - (text $ functionDef (reservedGobraWords (show o)) ["x Term", "y Term"] "Term") $$ - text "// associativity" $$ - assocEncoding (AC o) $$ - text "// commutativity" $$ - commEncoding (AC o) - ppFunSym (C EMap) = -- TODO not sure if we should print emapSymString or EMap - text $ functionDef (reservedGobraWords (BC.unpack emapSymString)) ["x Term", "y Term"] "Term" - ppFunSym (List) = -- TODO not sure about this one, but does not seem to be used anyway - text $ functionDef "list" ["l seq[Term]"] "Term" + (vcat $ map (ppFunSym "Term") funcSyms) $$ text "\n" + +ppFunSym :: Document d => String -> FunSym -> d +ppFunSym typeId (NoEq (f, (ar, _))) = + -- we do not make a distinction between private and public since we don't consider the adversary + let + args = map (++ " " ++ typeId) (convenienceNames ar "t") + in + text $ functionDef (reservedGobraWords (BC.unpack f)) args typeId +ppFunSym typeId (AC o) = + -- AC function symbols are made to be binary + -- This needs to happen in function declaration and application + (text $ functionDef (reservedGobraWords (show o)) ["x " ++ typeId, "y " ++ typeId] typeId) $$ + -- text ("// " ++ (reservedGobraWords (show o)) ++ " is associative") $$ + text "// associativity" $$ + assocEncoding (AC o) $$ + -- text ("// " ++ (reservedGobraWords (show o)) ++ " is commutative") $$ + text "// commutativity" $$ + commEncoding (AC o) +ppFunSym typeId (C EMap) = -- TODO not sure if we should print emapSymString or EMap + text $ functionDef (reservedGobraWords (BC.unpack emapSymString)) ["x " ++ typeId, "y " ++ typeId] typeId +ppFunSym typeId (List) = -- TODO not sure about this one, but does not seem to be used anyway + text $ functionDef "list" ["l seq[" ++ typeId ++ "]"] typeId + {- AC function symbols need an additional axiom to express it. @@ -88,7 +91,7 @@ termFuncEncoding sigMaude = rrules based on the Tamarin equational theory (see equation encoding). -} {- ---- ---- associativity encoding -} assocEncoding :: Document d => FunSym -> d -assocEncoding acSym@(AC _) = ppRRule Lhs (rruleAssoc acSym) +assocEncoding acSym@(AC _) = ppRRule Lhs "Term" (rruleAssoc acSym) where rruleAssoc :: FunSym -> RRule T.LNTerm rruleAssoc acOp = auxFapp acOp [x1, auxFapp acOp [x2, x3]] @@ -99,7 +102,7 @@ assocEncoding _ = error "assocEncoding called with non-ac function symbol" {- ---- ---- commutativity encoding -} commEncoding :: Document d => FunSym -> d -commEncoding acSym@(AC _) = ppRRule Lhs (rruleComm acSym) +commEncoding acSym@(AC _) = ppRRule Lhs "Term" (rruleComm acSym) where rruleComm :: FunSym -> RRule T.LNTerm rruleComm acOp = termViewToTerm (FApp acOp [x1, x2]) @@ -115,18 +118,17 @@ eqEncoding :: Document d => TriggerSetting -> MaudeSig -> d eqEncoding triggerSetting sigMaude = let rrules = S.toList (rrulesForMaudeSig sigMaude) - settings = repeat triggerSetting in - vcat $ punctuate (text "\n") $ map (uncurry ppRRule) (zip settings rrules) + vcat $ punctuate (text "\n") $ map (ppRRule triggerSetting "Term") rrules {- ---- ---- pretty print rewriting rules -} -ppRRule :: Document d => TriggerSetting -> T.RRule T.LNTerm -> d -ppRRule triggerSetting rr@(T.RRule lhs rhs) = +ppRRule :: Document d => TriggerSetting -> String -> T.RRule T.LNTerm -> d +ppRRule triggerSetting typeId rr@(T.RRule lhs rhs) = let trigger = (auxTrigger lhs) ++ (auxTrigger rhs) body = text (prettyGobraLNTerm True lhs) <> text " == " <> text (prettyGobraLNTerm True rhs) vars = frees rr - doc_vars = sepTerms (map (text . prettyGobraLNTerm True . TID.varToVTerm) vars) <> text " Term" + doc_vars = sepTerms (map (text . prettyGobraLNTerm True . TID.varToVTerm) vars) <> text (" " ++ typeId) in if null vars then axiom body From d7ac2ef42fea7d65b2fc715a94a7b57629375143 Mon Sep 17 00:00:00 2001 From: swiesner Date: Sat, 3 Sep 2022 18:53:51 +0200 Subject: [PATCH 05/19] Update generated code: Adds enum for integers and variations of enum. --- .../GenericHelperFunctions.hs | 19 ++++++++++++++++--- .../src/isabelleGeneratedCode/Restrictions.hs | 11 +++-------- 2 files changed, 19 insertions(+), 11 deletions(-) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/GenericHelperFunctions.hs b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/GenericHelperFunctions.hs index 4a72185..3600bfd 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/GenericHelperFunctions.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/GenericHelperFunctions.hs @@ -3,9 +3,10 @@ module GenericHelperFunctions(anya, nubBy, nub, enum, scanl, isSome, fstList, sndList, uncurry, zipWith, flipPair, collectThe, - stringOfNat, splitAndGetFst, splitAndGetSnd, - prependToString, sortIntoBucketsOrdered, - sortIntoBuckets, stringOfInteger) + enumIntZero, flipEnumInt, stringOfNat, splitAndGetFst, + splitAndGetSnd, flipEnumIntZero, prependToString, + sortIntoBucketsOrdered, sortIntoBuckets, + stringOfInteger) where { import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**), @@ -51,6 +52,9 @@ isSome :: forall a. Maybe a -> Bool; isSome (Just uu) = True; isSome Nothing = False; +enumInt :: forall a. Arith.Nat -> [a] -> [(Integer, a)]; +enumInt i xs = map (\ p -> (Arith.integer_of_nat (fst p), snd p)) (enum i xs); + fstList :: forall a b. [(a, b)] -> [a]; fstList pairList = fst (unzip pairList); @@ -87,6 +91,12 @@ collectThe asa = List.map_filter (\ x -> (if isSome x then Just (Option.the x) else Nothing)) asa; +enumIntZero :: forall a. [a] -> [(Integer, a)]; +enumIntZero ls = enumInt Arith.zero_nat ls; + +flipEnumInt :: forall a. Arith.Nat -> [a] -> [(a, Integer)]; +flipEnumInt i ls = map flipPair (enumInt i ls); + revDigitsOfNumber :: Arith.Nat -> [Arith.Nat]; revDigitsOfNumber i = let { @@ -130,6 +140,9 @@ splitAndGetSnd s = (map (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int)) s)); +flipEnumIntZero :: forall a. [a] -> [(a, Integer)]; +flipEnumIntZero ls = flipEnumInt Arith.zero_nat ls; + prependToString :: String -> String -> String; prependToString first second = (if not (first == "") diff --git a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs index 4838cf8..273553b 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/isabelleGeneratedCode/Restrictions.hs @@ -166,11 +166,6 @@ dbiToBoundLNTerm i = getDbiLitsPerFactArg :: TamiglooDatatypes.Fact -> [[Integer]]; getDbiLitsPerFactArg f = map getDbis (TamiglooDatatypes.accTermList f); -flipEnumInt :: forall a. Arith.Nat -> [a] -> [(a, Integer)]; -flipEnumInt i ls = - map (\ p -> (snd p, Arith.integer_of_nat (fst p))) - (GenericHelperFunctions.enum i ls); - perArgMapping :: TamiglooDatatypes.Fact -> [[(Integer, Integer)]]; perArgMapping f = let { @@ -185,7 +180,7 @@ perArgMapping f = (List.butlast (GenericHelperFunctions.scanl Arith.plus_nat Arith.zero_nat lens)); a = zip minBounds (getDbiLitsPerFactArg f); - } in map (\ p -> flipEnumInt (fst p) (snd p)) a; + } in map (\ p -> GenericHelperFunctions.flipEnumInt (fst p) (snd p)) a; factToDistinctDbis :: TamiglooDatatypes.Fact -> TamiglooDatatypes.Fact; factToDistinctDbis (TamiglooDatatypes.Fact fg ft ts) = @@ -257,8 +252,8 @@ mappingDbis restr = (List.foldr (\ a -> filter (\ b -> a == b)) (GenericHelperFunctions.fstList catPerArg) dbisRhs); _ = map (\ p -> (fst p, [snd p])) - (flipEnumInt (Arith.plus_nat maxDbisLhs Arith.one_nat) - dbisRhsNotInFact); + (GenericHelperFunctions.flipEnumInt + (Arith.plus_nat maxDbisLhs Arith.one_nat) dbisRhsNotInFact); mergedArgMapping = GenericHelperFunctions.sortIntoBuckets catPerArg; } in mergedArgMapping; From 22fec7af1df1b1e984b3139d47324dd0055a7cee Mon Sep 17 00:00:00 2001 From: swiesner Date: Sat, 3 Sep 2022 18:58:25 +0200 Subject: [PATCH 06/19] Adds inline formatting for quantified expressions e.g. forall. --- .../src/PrettyIOSpecs/Gobra/Utils.hs | 29 +++++++++++++++---- 1 file changed, 24 insertions(+), 5 deletions(-) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs index 32710a9..9ad6d76 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs @@ -1,6 +1,8 @@ module PrettyIOSpecs.Gobra.Utils ( reservedGobraWords + + , prettyLit , prettyGobraLNTerm , prettyGobraLNTermWithType , prettyGobraIOSTerm @@ -10,6 +12,7 @@ module PrettyIOSpecs.Gobra.Utils ( , exists , forallWithTriggerSetting + , forallWithTriggerSettingInline , axiom , prettyFact @@ -319,13 +322,17 @@ domain name doc = forallWithTriggerSetting :: Document d => TriggerSetting -> d -> [d] -> d -> d forallWithTriggerSetting = - quantifiedWithTriggerSetting "forall" + quantifiedWithTriggerSetting False "forall" + +forallWithTriggerSettingInline :: Document d => TriggerSetting -> d -> [d] -> d -> d +forallWithTriggerSettingInline = + quantifiedWithTriggerSetting True "forall" exists :: Document d => d -> d -> d -exists termsWithType body = quantifiedWithTriggerSetting "exists" None termsWithType [] body +exists termsWithType body = quantifiedWithTriggerSetting False "exists" None termsWithType [] body -quantifiedWithTriggerSetting :: Document d => String -> TriggerSetting -> d -> [d] -> d -> d -quantifiedWithTriggerSetting quant triggerSetting termsWithType triggers body = +quantifiedWithTriggerSetting :: Document d => Bool -> String -> TriggerSetting -> d -> [d] -> d -> d +quantifiedWithTriggerSetting inline quant triggerSetting termsWithType triggers body = let triggs = if (length triggers) == 0 || triggerSetting == None @@ -336,7 +343,9 @@ quantifiedWithTriggerSetting quant triggerSetting termsWithType triggers body = else triggers ) in - quantified quant termsWithType triggs body + if inline + then quantifiedInline quant termsWithType triggs body + else quantified quant termsWithType triggs body quantified :: Document d => String -> d -> [d] -> d -> d quantified quant termsWithType triggers body = @@ -349,6 +358,16 @@ quantified quant termsWithType triggers body = nest 4 body <> text ")" ) +quantifiedInline :: Document d => String -> d -> [d] -> d -> d +quantifiedInline quant termsWithType triggers body = + let + bracedTriggers = (hcat $ punctuate (text " ") $ map bracesInline triggers) + in + text (quant ++ " ") <> termsWithType <> text " :: " <> + bracedTriggers <> text " (" <> + body <> text ")" + + axiom :: Document d => d -> d axiom body = braces' (text "axiom ") body From dcb9c7988aadf485e377944a7654a92ce3278280 Mon Sep 17 00:00:00 2001 From: swiesner Date: Sat, 3 Sep 2022 19:01:24 +0200 Subject: [PATCH 07/19] Adds 'fst' and 'snd' to reserved words since they are already used in VeriFast's java.lang.javaspec. --- .../lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Utils.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Utils.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Utils.hs index 0e368be..aba200d 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Utils.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Utils.hs @@ -52,6 +52,8 @@ reservedVeriFastWords s = case s of _ | s == "true" -> "ok" _ | s == "pair" -> "paired" + _ | s == "fst" -> "fstTerm" + _ | s == "snd" -> "sndTerm" _ -> id s printTypeOfLNTerm :: T.LNTerm -> String From 2ee3e3be09017a5f82151fbb8e2d6dcdcaf76499 Mon Sep 17 00:00:00 2001 From: swiesner Date: Sat, 3 Sep 2022 19:05:30 +0200 Subject: [PATCH 08/19] Replaces inconsistent use of enum defined in CommonFunctions with the isabelle generated versions. --- .../tamigloo-compiler/src/PrettyIOSpecs/CommonFunctions.hs | 5 +++-- .../src/PrettyIOSpecs/Gobra/FactEncoding.hs | 6 +++--- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/CommonFunctions.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/CommonFunctions.hs index 9abcc7d..50d414c 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/CommonFunctions.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/CommonFunctions.hs @@ -18,7 +18,7 @@ module PrettyIOSpecs.CommonFunctions ( , functionApp , functionDef , joinString - , enum + -- , enum , sepTerms , bracesInline @@ -110,9 +110,10 @@ joinString delimiter args = [a] -> a (a:b:as) -> a ++ delimiter ++ joinString delimiter (b:as) +{- enum :: [a] -> [(a,Integer)] enum ls = zip ls [0..] - +-} sepTerms :: Document d => [d] -> d sepTerms ds = (hcat $ punctuate (text ", ") ds) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs index 568ac9a..6b7a307 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs @@ -14,7 +14,7 @@ import Text.PrettyPrint.Class -- Tamigloo imports -- ---- isabelle generated -import GenericHelperFunctions(nubBy) +import GenericHelperFunctions(nubBy, flipEnumIntZero) import qualified TamiglooDatatypes as TID import qualified IoSpecs as IOS -- ---- other Tamigloo modules @@ -35,9 +35,9 @@ gobraFactEncoding config tamiThy = factEncoding :: Document d => [TID.Fact] -> d factEncoding fs = (vcat $ punctuate (text "\n") $ - map (uncurry singleFactEncoding) (enum fs)) <> + map (uncurry singleFactEncoding) (flipEnumIntZero fs)) <> text "\n" $$ - persistentFunc (enum fs) + persistentFunc (flipEnumIntZero fs) collectFactsIOSFormulas :: [TID.IOSFormula] -> [TID.Fact] collectFactsIOSFormulas fs = nubBy TID.eqFactSig $ concat $ map (TID.getFactsFromFormula TID.getFactsFromIOSTerm) fs getDefsFromIOSpecs :: TID.Theory -> [TID.IOSFormula] From 1c6e61688e8166e4eb9cc5d8b3b548d47c56bfea Mon Sep 17 00:00:00 2001 From: swiesner Date: Sat, 3 Sep 2022 19:08:16 +0200 Subject: [PATCH 09/19] Generalizes functions printing declarations, equations, AC lemmas, etc. so they can be used with types other than 'Term'(e.g. when we later want to use them with bytes). --- .../PrettyIOSpecs/VeriFast/TermEncoding.hs | 84 +++++++++++-------- 1 file changed, 47 insertions(+), 37 deletions(-) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/TermEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/TermEncoding.hs index 92d7958..51ca796 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/TermEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/TermEncoding.hs @@ -7,6 +7,12 @@ module PrettyIOSpecs.VeriFast.TermEncoding ( , veriFastPubEncoding , veriFastFreshEncoding , veriFastPlaceEncoding + + + , funcDecls + , funcACLemmas + , nameACLemmas + , ppRRule ) where import Prelude @@ -50,61 +56,65 @@ veriFastTermEncoding (TID.Theory _thyName fsig _thyItems) = text "fixpoint Term freshTerm(Fresh f);" $$ text "fixpoint Term pubTerm(Pub p);" $$ text "\n\n" $$ text "// Function declarations" $$ - (funcDecls funcSyms) $$ + (funcDecls "Term" funcSyms) $$ text "\n\n" $$ - nest 4 (funcACLemmas funcSyms) $$ + nest 4 (funcACLemmas ppACLemmas funcSyms) $$ text "\n\n" $$ nest 4 (eqEncoding sigMaude) -funcDecls :: Document d => [FunSym] -> d -funcDecls fSyms = +funcDecls :: Document d => String -> [FunSym] -> d +funcDecls typeId fSyms = vcat $ map ppFunSym fSyms where ppFunSym :: Document d => FunSym -> d ppFunSym (NoEq (f, (ar, _))) = -- we do not make a distinction between private and public since we don't consider the adversary let - args = map ((++) "Term ") (convenienceNames ar "t") + args = map ((++) (typeId ++ " ")) (convenienceNames ar "t") in - fixpointNoBody "Term" (reservedVeriFastWords (BC.unpack f)) args + fixpointNoBody typeId (reservedVeriFastWords (BC.unpack f)) args ppFunSym (AC o) = -- AC function symbols are made to be binary -- This needs to happen in function declaration and application - fixpointNoBody "Term" (reservedVeriFastWords (show o)) ["Term x", "Term y"] + fixpointNoBody typeId (reservedVeriFastWords (show o)) [typeId ++ " x", typeId ++ " y"] ppFunSym (C EMap) = -- TODO not sure if we should print emapSymString or EMap - fixpointNoBody "Term" (reservedVeriFastWords (BC.unpack emapSymString)) ["Term x", "Term y"] + fixpointNoBody typeId (reservedVeriFastWords (BC.unpack emapSymString)) [typeId ++ " x", typeId ++ " y"] ppFunSym (List) = -- TODO not sure about this one, but does not seem to be used anyway - error $ functionApp "list" ["l seq[Term]"] -- NYI -funcACLemmas :: Document d => [FunSym] -> d -funcACLemmas fSyms = + error $ functionApp "list" ["l seq["++ typeId ++"]"] -- NYI +funcACLemmas :: Document d => (FunSym -> d) -> [FunSym] -> d +funcACLemmas ppACLemma fSyms = let filterAC = (\fs -> case fs of AC _ -> True _ -> False) in - vcat $ map ppACLemmas (filter filterAC fSyms) - where - ppACLemmas :: Document d => FunSym -> d - ppACLemmas (AC o) = - let - name = (reservedVeriFastWords (show o)) - lemmaNameA = (reservedVeriFastWords (show o) ++ "_A") - lemmaNameC = (reservedVeriFastWords (show o) ++ "_C") - in - text ("// associativity and commutativity for function " ++ name) $$ - -- assoc - (autoLemmaNoBody "void" lemmaNameA ["Term x", "Term y", "Term z"] "true" $ - "true && " ++ - (functionApp name ["x", functionApp name ["y", "z"] ]) ++ " == " ++ - (functionApp name [functionApp name ["x", "y"], "z" ]) - ) $$ - -- comm - (autoLemmaNoBody "void" lemmaNameC ["Term x", "Term y"] "true" $ - "true && " ++ - (functionApp name ["x", "y"]) ++ " == " ++ - (functionApp name ["y", "x"]) - ) + vcat $ map ppACLemma (filter filterAC fSyms) + +ppACLemmas :: Document d => FunSym -> d +ppACLemmas (AC o) = nameACLemmas "Term" (reservedVeriFastWords (show o)) + +nameACLemmas :: Document d => String -> String -> d +nameACLemmas typeId name = + let + lemmaNameA = (name ++ "_A") + lemmaNameC = (name ++ "_C") + in + text ("// associativity and commutativity for function " ++ name) $$ + -- assoc + (autoLemmaNoBody "void" lemmaNameA [typeId ++ " x", typeId ++ " y", typeId ++ " z"] "true" $ + "true && " ++ + (functionApp name ["x", functionApp name ["y", "z"] ]) ++ " == " ++ + (functionApp name [functionApp name ["x", "y"], "z" ]) + ) $$ + -- comm + (autoLemmaNoBody "void" lemmaNameC [typeId ++ " x", typeId ++ " y"] "true" $ + "true && " ++ + (functionApp name ["x", "y"]) ++ " == " ++ + (functionApp name ["y", "x"]) + ) + + {- ---- equation encoding -} @@ -117,14 +127,14 @@ eqEncoding sigMaude = let rrules = S.toList (rrulesForMaudeSig sigMaude) in - vcat $ map (uncurry ppRRule) (zip (convenienceNames (length rrules) "termFuncLemma") rrules) + vcat $ map (uncurry (ppRRule "Term")) (zip (convenienceNames (length rrules) "termFuncLemma") rrules) {- ---- ---- pretty print rewriting rules -} -ppRRule :: Document d => String -> T.RRule T.LNTerm -> d -ppRRule lemmaName rr@(T.RRule lhs rhs) = +ppRRule :: Document d => String -> String -> T.RRule T.LNTerm -> d +ppRRule typeId lemmaName rr@(T.RRule lhs rhs) = let vars = frees rr - args = map ((++) "Term " . prettyVFLNTerm True . TID.varToVTerm) vars + args = map ((++) (typeId ++ " ") . prettyVFLNTerm True . TID.varToVTerm) vars ens = (prettyVFLNTerm True lhs ++ " == " ++ prettyVFLNTerm True rhs) in autoLemmaNoBody "void" lemmaName args "true" ("true && " ++ ens) From 1f8169b7e93edbd203c0f5885116344d5b6486a6 Mon Sep 17 00:00:00 2001 From: swiesner Date: Sat, 3 Sep 2022 19:10:27 +0200 Subject: [PATCH 10/19] Adds Gobra encoding for 'Bytes' (analogous to functions and constants used with 'Term'/'Pub') and 'Gamma' (homomorphism). --- .../src/PrettyIOSpecs/Gobra/BytesEncoding.hs | 265 ++++++++++++++++++ .../src/PrettyIOSpecs/Gobra/Content.hs | 6 +- .../tamigloo-compiler/tamigloo-compiler.cabal | 1 + 3 files changed, 270 insertions(+), 2 deletions(-) create mode 100644 specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/BytesEncoding.hs diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/BytesEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/BytesEncoding.hs new file mode 100644 index 0000000..5859915 --- /dev/null +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/BytesEncoding.hs @@ -0,0 +1,265 @@ +module PrettyIOSpecs.Gobra.BytesEncoding ( + + gobraBytesEncoding + + ) where + + +import Prelude +import qualified Data.Map as Map +import qualified Data.Set as S +import qualified Data.ByteString.Char8 as BC + +-- Tamarin prover imports +import Text.PrettyPrint.Class +import Term.Term.Raw +import Term.Maude.Signature(MaudeSig, rrulesForMaudeSig, funSyms) +import Term.Term.FunctionSymbols +import Term.Builtin.Rules(RRule(..)) +import Term.LTerm (frees) +-- import Term.VTerm(constsVTerm) +import Term.Builtin.Convenience(x1, x2, x3) +import Theory.Model.Signature(_sigMaudeInfo) +import qualified Theory as T + +-- Tamigloo imports +-- ---- isabelle generated +import GenericHelperFunctions(nub, splitAndGetFst, splitAndGetSnd) +import qualified TamiglooDatatypes as TID +-- ---- other Tamigloo modules +import PrettyIOSpecs.Gobra.Utils + + +-- The Byte encoding for verifast presents a different approach to print the byte function signatures and rrules +-- Here this is achieved by changing the printers (e.g. ppFunSymB, ppRRuleB) while in the verifast case the funsyms and rrules are changed + + + + +gobraBytesEncoding :: Document d => Map.Map String String -> TID.Theory -> d +gobraBytesEncoding config thy@(TID.Theory _thyName fsig _thyItems) = + let + -- assume maudeSig has been used appropriately to initialize funSyms + sigMaude = ( _sigMaudeInfo fsig) + in + gobraHeader config "bytes" ["mod_pub", "mod_term"] ( + domain "Bytes" ( + baseEncoding $$ + constEncoding thy $$ + bytesFuncEncoding sigMaude $$ + eqEncoding (read (config Map.! "triggers") :: TriggerSetting) sigMaude + ) $$ text "\n\n\n" $$ + domain "Gamma" ( + gammaEncoding thy + ) + ) + + +gammaEncoding :: Document d => TID.Theory -> d +gammaEncoding thy@(TID.Theory _thyName _fsig _thyItems) = + text "func gamma(Term) Bytes" $$ + text "func oneTerm(Bytes) Term" $$ + text "// totality" $$ + axiom ( + forallWithTriggerSetting + All + (text "b Bytes") + [text "oneTerm(b)"] + (text "gamma(oneTerm(b)) == b") + ) $$ text "\n" $$ + text "// homomorphism" $$ + axiom ( + gammaHomomorphism thy $$ + text "// TODO: Add homomorphism axiom for constructors you added yourself e.g." $$ + text "// &&" $$ + text "// (forall s string :: {gamma(msg(s))} gamma(msg(s)) == msgB(s))" + ) + +gammaHomomorphism :: Document d => TID.Theory -> d +gammaHomomorphism thy@(TID.Theory _thyName fsig _thyItems) = + let + -- get function signatures from Maude signature + sigMaude = ( _sigMaudeInfo fsig) + funcSyms = S.toList (funSyms sigMaude) + in + (vcat $ punctuate (text " &&") $ (gammaConstants thy) ++ (map homomorphismSingleFunc funcSyms)) $$ text "\n" + +homomorphismSingleFunc :: Document d => FunSym -> d +homomorphismSingleFunc fs = + let + args = map (TID.varToVTerm . TID.createLVarFromName) (auxArgs fs) + termFuncApp = termViewToTerm (FApp fs args) + termFuncAppDoc = text (prettyGobraLNTerm True termFuncApp) + gammaArgsDoc = map (\t -> text $ functionApp "gamma" [t]) (auxArgs fs) + gammaApp = functionAppDoc (text "gamma") [termFuncAppDoc] + byteFuncAppDoc = functionAppDoc (text $ funSymName fs ++ "B") gammaArgsDoc + body = gammaApp <> text " == " <> byteFuncAppDoc + in + text "(" <> + (if length (auxArgs fs) > 0 + then + forallWithTriggerSettingInline + All + ((sepTerms $ map text (auxArgs fs)) <> text " Term") + [gammaApp] + body + else + body) + <> text ")" + where + auxArgs :: FunSym -> [String] + auxArgs (NoEq (_, (ar, _))) = (convenienceNames ar "t") + auxArgs _ = (convenienceNames 2 "t") + funSymName :: FunSym -> String + funSymName (NoEq (f, (_, _))) = reservedGobraWords (BC.unpack f) + funSymName (AC o) = reservedGobraWords (show o) + funSymName (C EMap) = reservedGobraWords (BC.unpack emapSymString) + funSymName (List) = "listB" + +gammaConstants :: Document d => TID.Theory -> [d] +gammaConstants thy = + let + constants = nub (TID.extractConsts thy) + in + map (singleGammaConst . makeNameConst) constants + where + singleGammaConst :: Document d => String -> d + singleGammaConst constName = + let + gammaApp = functionAppDoc (text "gamma") [text "pubTerm(" <> text (reservedGobraWords constName) <> text "())"] + constant = functionAppDoc (text (removeConstantSuffix (reservedGobraWords constName) ++ "B")) [] + in + parens (gammaApp <> text " == " <> constant) + +baseEncoding :: Document d => d +baseEncoding = + text "// TODO: Add constructors from other types e.g." $$ + text "// func msgB(string) Bytes" $$ text "\n" + +bytesFuncEncoding :: Document d => MaudeSig -> d +bytesFuncEncoding sigMaude = + let + -- get function signatures from Maude signature + funcSyms = S.toList (funSyms sigMaude) + in + text "// function declarations" $$ + (vcat $ map (ppFunSymB "Bytes") funcSyms) $$ text "\n" + +eqEncoding :: Document d => TriggerSetting -> MaudeSig -> d +eqEncoding triggerSetting sigMaude = + let + rrules = S.toList (rrulesForMaudeSig sigMaude) + in + text "// function equalities" $$ + (vcat $ punctuate (text "\n") $ map (ppRRuleB triggerSetting "Bytes") rrules) + + +constEncoding :: Document d => TID.Theory -> d +constEncoding thy = + let + constants = nub (TID.extractConsts thy) + in + text "// constants"$$ + (vcat $ + map (constFuncDef . makeNameConst) constants) <> text "\n" + where + constFuncDef :: Document d => String -> d + constFuncDef constName = + text $ functionDef (removeConstantSuffix (reservedGobraWords constName) ++ "B") [] "Bytes" + +removeConstantSuffix :: String -> String +removeConstantSuffix s = + if (reverse . splitAndGetFst . reverse) s == "pub" + then (reverse . splitAndGetSnd . reverse) s + else s + +{- ---- ---- associativity encoding -} +assocEncoding :: Document d => FunSym -> d +assocEncoding acSym@(AC _) = ppRRuleB Lhs "Bytes" (rruleAssoc acSym) + where + rruleAssoc :: FunSym -> RRule T.LNTerm + rruleAssoc acOp = auxFapp acOp [x1, auxFapp acOp [x2, x3]] + `RRule` auxFapp acOp [auxFapp acOp [x1, x2], x3] + auxFapp :: FunSym -> [T.LNTerm] -> T.LNTerm + auxFapp fs ts = termViewToTerm (FApp fs ts) +assocEncoding _ = error "assocEncoding called with non-ac function symbol" + +{- ---- ---- commutativity encoding -} +commEncoding :: Document d => FunSym -> d +commEncoding acSym@(AC _) = ppRRuleB Lhs "Bytes" (rruleComm acSym) + where + rruleComm :: FunSym -> RRule T.LNTerm + rruleComm acOp = termViewToTerm (FApp acOp [x1, x2]) + `RRule` termViewToTerm (FApp acOp [x2, x1]) +commEncoding _ = error "commEncoding called with non-ac function symbol" + + + + +ppFunSymB :: Document d => String -> FunSym -> d +ppFunSymB typeId (NoEq (f, (ar, _))) = + -- we do not make a distinction between private and public since we don't consider the adversary + let + args = map (++ " " ++ typeId) (convenienceNames ar "t") + in + text $ functionDef (reservedGobraWords (BC.unpack f) ++ "B") args typeId +ppFunSymB typeId (AC o) = + -- AC function symbols are made to be binary + -- This needs to happen in function declaration and application + (text $ functionDef (reservedGobraWords (show o) ++ "B") ["x " ++ typeId, "y " ++ typeId] typeId) $$ + text ("// " ++ (reservedGobraWords (show o) ++ "B") ++ " is associative") $$ + assocEncoding (AC o) $$ + text ("// " ++ (reservedGobraWords (show o) ++ "B") ++ " is commutative") $$ + commEncoding (AC o) $$ text "\n" +ppFunSymB typeId (C EMap) = -- TODO not sure if we should print emapSymString or EMap + text $ functionDef (reservedGobraWords (BC.unpack emapSymString) ++ "B") ["x " ++ typeId, "y " ++ typeId] typeId +ppFunSymB typeId (List) = -- TODO not sure about this one, but does not seem to be used anyway + text $ functionDef "listB" ["l seq[" ++ typeId ++ "]"] typeId + + + +ppRRuleB :: Document d => TriggerSetting -> String -> T.RRule T.LNTerm -> d +ppRRuleB triggerSetting typeId rr@(T.RRule lhs rhs) = + let + trigger = (auxTrigger lhs) ++ (auxTrigger rhs) + body = text (prettyGobraLNTermB True lhs) <> text " == " <> text (prettyGobraLNTermB True rhs) + vars = frees rr + doc_vars = sepTerms (map (text . prettyGobraLNTermB True . TID.varToVTerm) vars) <> text (" " ++ typeId) + in + if null vars + then axiom body + else axiom (forallWithTriggerSetting triggerSetting doc_vars trigger body) + where + auxTrigger :: Document d => T.LNTerm -> [d] + auxTrigger t = case viewTerm t of + (FApp _ (_:_)) -> [text $ prettyGobraLNTermB True t] + _ -> [emptyDoc] + + +prettyGobraLNTermB :: Bool -> T.LNTerm -> String +prettyGobraLNTermB wrap = prettyGobraTermB (prettyLit wrap) + +-- | Pretty print a term. +prettyGobraTermB :: Show l => (l -> String) -> Term l -> String +prettyGobraTermB ppLit = ppTerm + where + ppTerm t = case viewTerm t of + Lit l -> ppLit l + FApp (AC o) ts -> auxAC (AC o) ts + FApp (NoEq (f, _)) ts -> ppFunBC f ts + FApp (C EMap) ts -> ppFunBC emapSymString ts + FApp List ts -> ppFun "list" ts + + ppFunBC f ts = ppFun (BC.unpack f) ts + + ppFun f ts = + (reservedGobraWords f) ++ "B" ++"(" ++ joinString ", " (map ppTerm ts) ++ ")" + + auxAC (AC o) ts = case ts of + [a] -> ppTerm a + [a, b] -> ppFun (show o) [a, b] + x:xs -> ppFun (show o) [x, termViewToTerm (FApp (AC o) xs)] + _ -> error "AC op cannot have empty args" + auxAC _ _ = error "auxAC called with non-ac function symbol" + + diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Content.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Content.hs index 6c6c18c..8d623b6 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Content.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Content.hs @@ -24,6 +24,7 @@ import PrettyIOSpecs.Gobra.TermEncoding import PrettyIOSpecs.Gobra.FactEncoding import PrettyIOSpecs.Gobra.PermissionEncoding import PrettyIOSpecs.Gobra.IOSpecs +import PrettyIOSpecs.Gobra.BytesEncoding @@ -45,14 +46,15 @@ generatePathsWithContent config tamiThy = where encodings :: Document d => [(String, d)] encodings = - map (\p -> (config Map.! (fst p), snd p)) $ + (map (\p -> (config Map.! (fst p), snd p)) $ [ ("path_claim", gobraClaimEncoding config tamiThy) , ("path_fact", gobraFactEncoding config tamiThy) , ("path_term", gobraTermEncoding config tamiThy) , ("path_place", gobraPlaceEncoding config) , ("path_pub", gobraPubEncoding config tamiThy) , ("path_fresh", gobraFreshEncoding config) - ] + ]) ++ + [(config Map.! "base_dir" "bytes/bytes.gobra", gobraBytesEncoding config tamiThy)] permissions :: Document d => [(String, d)] permissions = let diff --git a/specification-generator/src/lib/tamigloo-compiler/tamigloo-compiler.cabal b/specification-generator/src/lib/tamigloo-compiler/tamigloo-compiler.cabal index 0b95445..a47d054 100644 --- a/specification-generator/src/lib/tamigloo-compiler/tamigloo-compiler.cabal +++ b/specification-generator/src/lib/tamigloo-compiler/tamigloo-compiler.cabal @@ -58,6 +58,7 @@ library PrettyIOSpecs.Gobra.TermEncoding PrettyIOSpecs.Gobra.FactEncoding PrettyIOSpecs.Gobra.Content + PrettyIOSpecs.Gobra.BytesEncoding PrettyIOSpecs.VeriFast.TermEncoding PrettyIOSpecs.VeriFast.FactEncoding From f996614fdf6dde4fb7dec482c4da2ff06f7bd1f5 Mon Sep 17 00:00:00 2001 From: swiesner Date: Sat, 3 Sep 2022 19:13:06 +0200 Subject: [PATCH 11/19] Adds VeriFast encoding for functions/constants defined on bytes (analogous to the ones defined on 'Term's). Adds gamma function (Term to bytes) and homomorphism. --- .../PrettyIOSpecs/VeriFast/BytesEncoding.hs | 198 ++++++++++++++++++ .../src/PrettyIOSpecs/VeriFast/Content.hs | 2 + .../tamigloo-compiler/tamigloo-compiler.cabal | 1 + 3 files changed, 201 insertions(+) create mode 100644 specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/BytesEncoding.hs diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/BytesEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/BytesEncoding.hs new file mode 100644 index 0000000..7df0af9 --- /dev/null +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/BytesEncoding.hs @@ -0,0 +1,198 @@ +module PrettyIOSpecs.VeriFast.BytesEncoding ( + + veriFastBytesEncoding + + ) where + + +import Prelude +import qualified Data.Map as Map +import qualified Data.Set as S +import qualified Data.ByteString.Char8 as BC + +-- Tamarin prover imports +import Text.PrettyPrint.Class +import Term.Term.Raw +import Term.Maude.Signature(MaudeSig, rrulesForMaudeSig, funSyms) +import Term.Term.FunctionSymbols +import Term.Builtin.Rules(RRule(..)) +import Term.LTerm (frees) +import Term.VTerm(constsVTerm) +--import Term.Builtin.Convenience(x1, x2, x3) +import Theory.Model.Signature(_sigMaudeInfo) +import qualified Theory as T + +-- Tamigloo imports +-- ---- isabelle generated +import GenericHelperFunctions(nub, enumIntZero) +import qualified TamiglooDatatypes as TID +-- ---- other Tamigloo modules +import qualified PrettyIOSpecs.VeriFast.TermEncoding as VFT +import PrettyIOSpecs.VeriFast.Utils + + +veriFastBytesEncoding :: Document d => TID.Theory -> d +veriFastBytesEncoding thy@(TID.Theory _thyName fsig _thyItems) = + let + -- assume maudeSig has been used appropriately to initialize funSyms + sigMaude = ( _sigMaudeInfo fsig) + in + ghostBlock $ + text "fixpoint list bytes_int(int i);\n" $$ + text "// TODO: Add constructors from other types e.g." $$ + text "// fixpoint list msgB(string);" $$ text "\n" $$ + constEncoding thy $$ text "\n" $$ + bytesFuncEncoding sigMaude $$ text "\n" $$ + eqEncoding sigMaude $$ text "\n" $$ + gammaEncoding thy + + +gammaEncoding :: Document d => TID.Theory -> d +gammaEncoding thy@(TID.Theory _thyName _fsig _thyItems) = + text "// Gamma" $$ + text "fixpoint list gamma(Term t);" $$ + text "fixpoint Term oneTerm(list b);" $$ + autoLemmaNoBody "void" "gammaOneTerm" ["list bs"] "true" "gamma(oneTerm(bs)) == bs" <> text "\n" $$ + text "// homomorphism" $$ + gammaHomomorphism thy + +gammaFunSym :: FunSym +gammaFunSym = (NoEq (BC.pack "gamma", (1, Public))) + +gammaHomomorphism :: Document d => TID.Theory -> d +gammaHomomorphism thy@(TID.Theory _thyName fsig _thyItems) = + let + -- get function signatures from Maude signature + sigMaude = ( _sigMaudeInfo fsig) + funcSyms = S.toList (funSyms sigMaude) + in + (gammaConstants thy) <> text "\n" $$ + (homomorphismFuncs funcSyms) <> text "\n" $$ + text "// TODO: Add homomorphism axiom for constructors you added yourself e.g." $$ + text "// gamma(msg(string)) == msgB(string)" + +homomorphismFuncs :: Document d => [FunSym] -> d +homomorphismFuncs fss = + vcat $ map (\p -> homomorphismSingleFunc ("gammaLemmaFuncs" ++ show (fst p)) (snd p)) (enumIntZero fss) + +homomorphismSingleFunc :: Document d => String -> FunSym -> d +homomorphismSingleFunc lemmaName fs = + let + args = map (TID.varToVTerm . TID.createLVarFromName) (auxArgs fs) + termFuncApp = termViewToTerm (FApp fs args) + + gammaArgs = map (\t -> termViewToTerm (FApp gammaFunSym [t])) args + gammaApp = termViewToTerm (FApp gammaFunSym [termFuncApp]) + bytesFuncApp = termViewToTerm (FApp (funSymBytes fs) gammaArgs) + in + autoLemmaNoBody "void" lemmaName (map (\a -> "Term " ++ prettyVFLNTerm True a) args) + ("true") + (prettyVFLNTerm True gammaApp ++ " == " ++ prettyVFLNTerm True bytesFuncApp) + + where + auxArgs :: FunSym -> [String] + auxArgs (NoEq (_, (ar, _))) = (convenienceNames ar "t") + auxArgs _ = (convenienceNames 2 "t") + +gammaConstants :: Document d => TID.Theory -> d +gammaConstants thy = + let + constants = enumIntZero $ nub (TID.extractConsts thy) + gammaConsts = + map + (\p -> + singleGammaConst + ("gammaLemmaConstants" ++ show (fst p)) + (makeNameConst $ snd p)) + constants + in + vcat gammaConsts + + where + singleGammaConst :: Document d => String -> String -> d + singleGammaConst lemmaName constName = + let + gammaApp = functionApp "gamma" ["pubTerm("++ reservedVeriFastWords constName ++ ")"] + constant = functionApp (reservedVeriFastWords constName ++ "B") [] + in + autoLemmaNoBody "void" lemmaName [] "true" (gammaApp ++ " == " ++ constant) + + + +bytesFuncEncoding :: Document d => MaudeSig -> d +bytesFuncEncoding sigMaude = + let + -- get function signatures from Maude signature + funcSyms = S.toList (funSyms sigMaude) + in + text "// function declarations" $$ + VFT.funcDecls "list" (map funSymBytes funcSyms) $$ text "\n" $$ + bytesFuncACLemmas funcSyms + +bytesFuncACLemmas :: Document d => [FunSym] -> d +bytesFuncACLemmas fss = VFT.funcACLemmas ppByteACLemma fss + +ppByteACLemma :: Document d => FunSym -> d +ppByteACLemma fs = VFT.nameACLemmas "list" (funSymNameBytes fs) + + +eqEncoding :: Document d => MaudeSig -> d +eqEncoding sigMaude = + let + rrules = map rruleBytes $ S.toList (rrulesForMaudeSig sigMaude) + in + vcat $ map (uncurry (VFT.ppRRule "list")) (zip (convenienceNames (length rrules) "byteFuncLemma") rrules) + + +constEncoding :: Document d => TID.Theory -> d +constEncoding thy = + let + constants = nub (TID.extractConsts thy) + in + text "// constants"$$ + (vcat $ + map (constFuncDef . makeNameConst) constants) <> text "\n" + where + constFuncDef :: Document d => String -> d + constFuncDef constName = + fixpointNoBody "list" (reservedVeriFastWords constName ++ "B") [] + + + + + +funSymName :: FunSym -> String +funSymName (NoEq (f, (_, _))) = reservedVeriFastWords (BC.unpack f) +funSymName (AC o) = reservedVeriFastWords (show o) +funSymName (C EMap) = reservedVeriFastWords (BC.unpack emapSymString) +funSymName (List) = "list" + + +funSymNameBytes :: FunSym -> String +funSymNameBytes fs = (funSymName fs) ++ "B" + +funSymBytes :: FunSym -> FunSym +funSymBytes fs@(NoEq (_, (ar, priv))) = (NoEq (BC.pack (funSymNameBytes fs), (ar, priv))) +funSymBytes fs@(AC _) = (NoEq (BC.pack (funSymNameBytes fs), (2, Public))) +funSymBytes (C EMap) = (C EMap) -- ? +funSymBytes (List) = (List) + +rruleBytes :: RRule T.LNTerm -> RRule T.LNTerm +rruleBytes rrule = fmap lnTermBytes rrule + +lnTermBytes :: T.LNTerm -> T.LNTerm +lnTermBytes t = case viewTerm t of + Lit _ -> t + FApp (AC o) ts -> auxAC (AC o) ts + FApp fs ts -> auxF fs ts + where + auxF :: FunSym -> [T.LNTerm] -> T.LNTerm + auxF fsym terms = termViewToTerm (FApp (funSymBytes fsym) (map lnTermBytes terms)) + auxAC :: FunSym -> [T.LNTerm] -> T.LNTerm + auxAC fsym@(AC o) terms = case terms of + [_, _] -> auxF fsym terms + x:xs -> auxF fsym [x, termViewToTerm (FApp (AC o) xs)] + _ -> error "AC op cannot have unary or empty args" + auxAC _ _ = error "auxAC called with non-ac function symbol" + + diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Content.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Content.hs index dba2741..418ab28 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Content.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Content.hs @@ -26,6 +26,7 @@ import PrettyIOSpecs.VeriFast.TermEncoding import PrettyIOSpecs.VeriFast.FactEncoding import PrettyIOSpecs.VeriFast.PermissionEncoding import PrettyIOSpecs.VeriFast.IOSpecs +import PrettyIOSpecs.VeriFast.BytesEncoding content:: Document d => Map.Map String String -> TID.Theory -> [(FilePath, d)] content = generatePathsWithContent @@ -44,6 +45,7 @@ generatePathsWithContent config tamiThy = , dirPath config "fact" "fact" ["fresh", "pub", "term"] (veriFastFactEncoding tamiThy) -- maybe add multiset encoding here , dirPath config "claim" "claim" ["fresh", "pub", "term"] (veriFastClaimEncoding tamiThy) , dirPath config "place" "place" [] (veriFastPlaceEncoding) + , dirPath config "bytes" "bytes" ["pub", "term"] (veriFastBytesEncoding tamiThy) ] permissions = concat $ [ dirPath config "iospec" "permissions_out" ["place", "fresh", "pub", "term"] (veriFastOutPermissions tamiThy) diff --git a/specification-generator/src/lib/tamigloo-compiler/tamigloo-compiler.cabal b/specification-generator/src/lib/tamigloo-compiler/tamigloo-compiler.cabal index a47d054..d32e85c 100644 --- a/specification-generator/src/lib/tamigloo-compiler/tamigloo-compiler.cabal +++ b/specification-generator/src/lib/tamigloo-compiler/tamigloo-compiler.cabal @@ -67,6 +67,7 @@ library PrettyIOSpecs.VeriFast.MultiSetEncoding PrettyIOSpecs.VeriFast.Utils PrettyIOSpecs.VeriFast.Content + PrettyIOSpecs.VeriFast.BytesEncoding DerivingInstances From fa453eecaac0134a8d513f31d12cd9be0efecb3c Mon Sep 17 00:00:00 2001 From: swiesner Date: Sat, 3 Sep 2022 22:09:49 +0200 Subject: [PATCH 12/19] Simplify TamiglooConfig by unnecessary hardcoded removing path info from config. --- .../src/PrettyIOSpecs/Gobra/Content.hs | 62 ++++++++++++------- .../tamigloo-compiler/src/TamiglooConfig.hs | 29 +-------- 2 files changed, 42 insertions(+), 49 deletions(-) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Content.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Content.hs index 8d623b6..8e54ccd 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Content.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Content.hs @@ -11,12 +11,12 @@ import qualified Data.Map as Map import Text.PrettyPrint.Class import System.FilePath -import qualified Theory as T -import qualified Theory.Model.Formula as Form +-- import qualified Theory as T +-- import qualified Theory.Model.Formula as Form -import TamiglooConfig +-- import TamiglooConfig import qualified TamiglooDatatypes as TID -import qualified IoSpecs as IOS +-- import qualified IoSpecs as IOS -- import Arith (integer_of_nat) import PrettyIOSpecs.Gobra.Utils @@ -35,6 +35,24 @@ content config tamiThy = then (generatePathsWithContent config tamiThy) else tail (generatePathsWithContent config tamiThy) +filePathRel :: String -> String +filePathRel name = name (name ++ ".gobra") + +filePathBase :: Map.Map String String -> String -> String +filePathBase config name = config Map.! "base_dir" (filePathRel name) + +modNames :: [String] +modNames = + [ "place" + , "fresh" + , "pub" + , "term" + , "bytes" + , "claim" + , "fact" + , "iospec" + ] + generatePathsWithContent :: Document d => Map.Map String String -> TID.Theory -> [(String, d)] generatePathsWithContent config tamiThy = goMod ++ @@ -46,25 +64,24 @@ generatePathsWithContent config tamiThy = where encodings :: Document d => [(String, d)] encodings = - (map (\p -> (config Map.! (fst p), snd p)) $ - [ ("path_claim", gobraClaimEncoding config tamiThy) - , ("path_fact", gobraFactEncoding config tamiThy) - , ("path_term", gobraTermEncoding config tamiThy) - , ("path_place", gobraPlaceEncoding config) - , ("path_pub", gobraPubEncoding config tamiThy) - , ("path_fresh", gobraFreshEncoding config) - ]) ++ - [(config Map.! "base_dir" "bytes/bytes.gobra", gobraBytesEncoding config tamiThy)] + [ (filePathBase config "place", gobraPlaceEncoding config) + , (filePathBase config "fresh", gobraFreshEncoding config) + , (filePathBase config "pub", gobraPubEncoding config tamiThy) + , (filePathBase config "term", gobraTermEncoding config tamiThy) + , (filePathBase config "bytes", gobraBytesEncoding config tamiThy) + , (filePathBase config "claim", gobraClaimEncoding config tamiThy) + , (filePathBase config "fact", gobraFactEncoding config tamiThy) + ] permissions :: Document d => [(String, d)] permissions = let - base = takeDirectory (config Map.! "path_iospec") + dir = config Map.! "base_dir" "iospec" permsIntern = gobraInternalPermissions config tamiThy - pathsIntern = map (\p -> base "permissions_" ++ (fst p) ++ "_internal.gobra") permsIntern + pathsIntern = map (\p -> dir "permissions_" ++ (fst p) ++ "_internal.gobra") permsIntern permsOut = gobraOutPermissions config tamiThy - pathOut = base "permissions_out.gobra" + pathOut = dir "permissions_out.gobra" permsIn = gobraInPermissions config tamiThy - pathIn = base "permissions_in.gobra" + pathIn = dir "permissions_in.gobra" in (pathOut, permsOut) : (pathIn, permsIn) : @@ -72,11 +89,11 @@ generatePathsWithContent config tamiThy = iospecs :: Document d => [(String, d)] iospecs = let - base = takeDirectory (config Map.! "path_iospec") - iospecs = gobraIOSpecs config tamiThy - paths = map (\p -> base (fst p) ++ ".gobra") iospecs + dir = config Map.! "base_dir" "iospec" + iospecsContent = gobraIOSpecs config tamiThy + paths = map (\p -> dir (fst p) ++ ".gobra") iospecsContent in - (zip paths (map snd iospecs)) + (zip paths (map snd iospecsContent)) debug :: Document d => [(String, d)] debug = [(config Map.! "base_dir" "tamiglooModel.debug", @@ -91,7 +108,8 @@ generatePathsWithContent config tamiThy = readMeFile :: Document d => Map.Map String String -> [(String, d)] -> [(String, d)] -> d readMeFile config perms ios = let - relPaths = Map.elems $ defaultRelativePaths + relPaths = map filePathRel modNames + in text "Running the following commands from the base directory (directory where the readme resides) will verify the respective generated encoding using the provided Gobra jar." $$ text "\n" $$ diff --git a/specification-generator/src/lib/tamigloo-compiler/src/TamiglooConfig.hs b/specification-generator/src/lib/tamigloo-compiler/src/TamiglooConfig.hs index 0e35da6..c7cdf4e 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/TamiglooConfig.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/TamiglooConfig.hs @@ -4,7 +4,6 @@ module TamiglooConfig( defaultConfig , tamiglooReadConfig - , defaultRelativePaths , defaultRelativeModules @@ -25,10 +24,8 @@ defaultConfig inputConfig = config = Map.union inputConfig defaultOptions in Map.union - config $ - Map.union - (defaultModules config) $ -- add package names for input - defaultPaths config -- add paths for output files + config + (defaultModules config) -- add package names for input -- package names with modules prefix. Used for import statements defaultModules :: Map.Map String String -> Map.Map String String @@ -64,28 +61,6 @@ defaultOptions = -- ("base_dir", "needs to be specified") ]) --- paths of output files -defaultPaths :: Map.Map String String -> Map.Map String String -defaultPaths config = - let - baseDir = config Map.! "base_dir" - in - Map.map (baseDir ) defaultRelativePaths - --- paths of file outputs relative to a base directory -defaultRelativePaths :: Map.Map String String -defaultRelativePaths = - (Map.map addSuffix $ Map.mapKeys modToPath $ filterMod defaultRelativeModules) - where - -- returns keys starting with "mod" - filterMod :: Map.Map String String -> Map.Map String String - filterMod = Map.filterWithKey (\k _ -> takeWhile (/= '_') k == "mod") - modToPath :: String -> String - modToPath s = "path" ++ (dropWhile (/= '_') s) - -- adds a file of the same name to the directory s - addSuffix :: String -> String - addSuffix s = s (s++".gobra") - -- reads a file (containing an even number of whitespace separated words) -- and turns it into a String key-value Map tamiglooReadConfig :: FilePath -> IO (Map.Map String String) From 078106eaee3dd7084972d1834bddb7b535142a96 Mon Sep 17 00:00:00 2001 From: swiesner Date: Sat, 3 Sep 2022 23:33:54 +0200 Subject: [PATCH 13/19] Moves Gobra file path methods to utils. --- .../src/PrettyIOSpecs/Gobra/Content.hs | 34 +++++-------------- .../src/PrettyIOSpecs/Gobra/Utils.hs | 24 +++++++++++-- 2 files changed, 30 insertions(+), 28 deletions(-) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Content.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Content.hs index 8e54ccd..cec8ee7 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Content.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Content.hs @@ -35,24 +35,6 @@ content config tamiThy = then (generatePathsWithContent config tamiThy) else tail (generatePathsWithContent config tamiThy) -filePathRel :: String -> String -filePathRel name = name (name ++ ".gobra") - -filePathBase :: Map.Map String String -> String -> String -filePathBase config name = config Map.! "base_dir" (filePathRel name) - -modNames :: [String] -modNames = - [ "place" - , "fresh" - , "pub" - , "term" - , "bytes" - , "claim" - , "fact" - , "iospec" - ] - generatePathsWithContent :: Document d => Map.Map String String -> TID.Theory -> [(String, d)] generatePathsWithContent config tamiThy = goMod ++ @@ -64,13 +46,13 @@ generatePathsWithContent config tamiThy = where encodings :: Document d => [(String, d)] encodings = - [ (filePathBase config "place", gobraPlaceEncoding config) - , (filePathBase config "fresh", gobraFreshEncoding config) - , (filePathBase config "pub", gobraPubEncoding config tamiThy) - , (filePathBase config "term", gobraTermEncoding config tamiThy) - , (filePathBase config "bytes", gobraBytesEncoding config tamiThy) - , (filePathBase config "claim", gobraClaimEncoding config tamiThy) - , (filePathBase config "fact", gobraFactEncoding config tamiThy) + [ (gobraFilePathBase config "place", gobraPlaceEncoding config) + , (gobraFilePathBase config "fresh", gobraFreshEncoding config) + , (gobraFilePathBase config "pub", gobraPubEncoding config tamiThy) + , (gobraFilePathBase config "term", gobraTermEncoding config tamiThy) + , (gobraFilePathBase config "bytes", gobraBytesEncoding config tamiThy) + , (gobraFilePathBase config "claim", gobraClaimEncoding config tamiThy) + , (gobraFilePathBase config "fact", gobraFactEncoding config tamiThy) ] permissions :: Document d => [(String, d)] permissions = @@ -108,7 +90,7 @@ generatePathsWithContent config tamiThy = readMeFile :: Document d => Map.Map String String -> [(String, d)] -> [(String, d)] -> d readMeFile config perms ios = let - relPaths = map filePathRel modNames + relPaths = map gobraFilePathRel modNames in text "Running the following commands from the base directory (directory where the readme resides) will verify the respective generated encoding using the provided Gobra jar." $$ diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs index 9ad6d76..2395374 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs @@ -1,6 +1,9 @@ module PrettyIOSpecs.Gobra.Utils ( - reservedGobraWords + gobraFilePathRel + , gobraFilePathBase + , modNames + , reservedGobraWords , prettyLit , prettyGobraLNTerm @@ -38,6 +41,7 @@ module PrettyIOSpecs.Gobra.Utils ( import Prelude import qualified Data.Map as Map import qualified Data.ByteString.Char8 as BC +import System.FilePath -- Tamarin prover imports import Text.PrettyPrint.Class @@ -58,7 +62,23 @@ import qualified IoSpecs as IOS import DerivingInstances() import PrettyIOSpecs.CommonFunctions - +gobraFilePathRel :: String -> String +gobraFilePathRel name = name (name ++ ".gobra") + +gobraFilePathBase :: Map.Map String String -> String -> String +gobraFilePathBase config name = config Map.! "base_dir" (gobraFilePathRel name) + +modNames :: [String] +modNames = + [ "place" + , "fresh" + , "pub" + , "term" + , "bytes" + , "claim" + , "fact" + , "iospec" + ] data TriggerSetting = None | Lhs | All deriving (Prelude.Read, Prelude.Show, Prelude.Eq) From 647804377ac24f0d1d8a22aa197c4a91fc833f90 Mon Sep 17 00:00:00 2001 From: swiesner Date: Sat, 3 Sep 2022 23:40:39 +0200 Subject: [PATCH 14/19] Simplify TamiglooConfig by removing unnecessary mod_ entries in config. --- .../src/PrettyIOSpecs/Gobra/BytesEncoding.hs | 2 +- .../src/PrettyIOSpecs/Gobra/FactEncoding.hs | 4 +-- .../src/PrettyIOSpecs/Gobra/IOSpecs.hs | 2 +- .../PrettyIOSpecs/Gobra/PermissionEncoding.hs | 6 ++-- .../src/PrettyIOSpecs/Gobra/TermEncoding.hs | 2 +- .../src/PrettyIOSpecs/Gobra/Utils.hs | 8 ++--- .../tamigloo-compiler/src/TamiglooConfig.hs | 35 +++---------------- 7 files changed, 16 insertions(+), 43 deletions(-) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/BytesEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/BytesEncoding.hs index 5859915..965b01c 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/BytesEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/BytesEncoding.hs @@ -42,7 +42,7 @@ gobraBytesEncoding config thy@(TID.Theory _thyName fsig _thyItems) = -- assume maudeSig has been used appropriately to initialize funSyms sigMaude = ( _sigMaudeInfo fsig) in - gobraHeader config "bytes" ["mod_pub", "mod_term"] ( + gobraHeader config "bytes" ["pub", "term"] ( domain "Bytes" ( baseEncoding $$ constEncoding thy $$ diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs index 6b7a307..f274625 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs @@ -24,7 +24,7 @@ import PrettyIOSpecs.Gobra.Utils gobraFactEncoding :: Document d => Map.Map String String -> TID.Theory -> d gobraFactEncoding config tamiThy = - gobraHeader config "fact" ["mod_term", "mod_pub", "mod_fresh"] ( + gobraHeader config "fact" ["term", "pub", "fresh"] ( domain "Fact" ( factEncoding (collectFactsIOSFormulas . getDefsFromIOSpecs $ tamiThy) <> (text "\n") @@ -47,7 +47,7 @@ gobraFactEncoding config tamiThy = gobraClaimEncoding :: Document d => Map.Map String String -> TID.Theory -> d gobraClaimEncoding config tamiThy = - gobraHeader config "claim" ["mod_term"] ( + gobraHeader config "claim" ["term"] ( domain "Claim" ( claimEncoding (collectClaimsIOSFormulas . getDefsFromIOSpecs $ tamiThy) <> (text "\n") diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs index 74b102b..70146b6 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs @@ -39,7 +39,7 @@ gobraIOSpecs config thy = header :: Document d => d -> d header spec = gobraHeader config "iospec" - ["mod_claim", "mod_fact", "mod_term", "mod_place", "mod_pub", "mod_fresh"] + ["claim", "fact", "term", "place", "pub", "fresh"] spec prettyIOSpecs :: Document d => TID.Theory -> [(String, d)] diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/PermissionEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/PermissionEncoding.hs index 55d1bfa..1dfa20e 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/PermissionEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/PermissionEncoding.hs @@ -49,7 +49,7 @@ gobraInternalPermissions config thy = header :: Document d => d -> d header body = gobraHeader config "iospec" - ["mod_claim", "mod_fact", "mod_term", "mod_place", "mod_pub", "mod_fresh"] + ["claim", "fact", "term", "place", "pub", "fresh"] body {- internal permissions -} @@ -73,7 +73,7 @@ gobraOutPermissions config thy = concatMap (\inp -> map snd $ IOS.getAbsPhisWithDef (snd inp)) (IOS.extractIOSpec thy) in gobraHeader config "iospec" - ["mod_claim", "mod_fact", "mod_term", "mod_place", "mod_pub", "mod_fresh"] + ["claim", "fact", "term", "place", "pub", "fresh"] ( vcat $ permEncoding formulas TID.Out_RG ) @@ -85,7 +85,7 @@ gobraInPermissions config thy = concatMap (\inp -> map snd $ IOS.getAbsPhisWithDef (snd inp)) (IOS.extractIOSpec thy) in gobraHeader config "iospec" - ["mod_claim", "mod_fact", "mod_term", "mod_place", "mod_pub", "mod_fresh"] + ["claim", "fact", "term", "place", "pub", "fresh"] ( vcat $ permEncoding formulas TID.In_RF ) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/TermEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/TermEncoding.hs index 8025698..611297e 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/TermEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/TermEncoding.hs @@ -41,7 +41,7 @@ gobraTermEncoding config (TID.Theory _thyName fsig _thyItems) = -- assume maudeSig has been used appropriately to initialize funSyms sigMaude = ( _sigMaudeInfo fsig) in - gobraHeader config "term" ["mod_pub", "mod_fresh"] ( + gobraHeader config "term" ["pub", "fresh"] ( domain "Term" ( baseTermEncoding $$ termFuncEncoding sigMaude $$ diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs index 2395374..f42d86e 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs @@ -315,10 +315,10 @@ showTamiFactTag ft = case ft of {- Formatting -} gobraHeader :: Document d => Map.Map String String -> String -> [String] -> d -> d -gobraHeader config packageName importKeys spec = +gobraHeader config packageName importedPackages spec = packageHeader packageName $$ (text "\n") $$ - importHeader config importKeys $$ + importHeader config importedPackages $$ (text "\n") $$ spec @@ -329,8 +329,8 @@ packageHeader package_name = ) importHeader :: Document d => Map.Map String String -> [String] -> d -importHeader config mod_keys = - vcat $ map (text . ("import . " ++)) $ map (quotes' . (config Map.!)) mod_keys +importHeader config importedPackages = + vcat $ map (text . ("import . " ++)) $ map (\i -> quotes' $ config Map.! "module" i) importedPackages where quotes' :: String -> String quotes' s = "\""++s++"\"" diff --git a/specification-generator/src/lib/tamigloo-compiler/src/TamiglooConfig.hs b/specification-generator/src/lib/tamigloo-compiler/src/TamiglooConfig.hs index c7cdf4e..3938924 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/TamiglooConfig.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/TamiglooConfig.hs @@ -4,49 +4,22 @@ module TamiglooConfig( defaultConfig , tamiglooReadConfig - , defaultRelativeModules ) where import Prelude import qualified Data.Map as Map -import System.FilePath +-- import System.FilePath -- Takes the inputConfig from user and fills up unspecified options with the defaults -- Also calculates the paths for import statements, etc and adds them to config -- A minimal working input config needs to contain the base_dir and input_file key defaultConfig :: Map.Map String String -> Map.Map String String defaultConfig inputConfig = - let - -- Map.union is left-biased: in case of duplicates left value is kept - -- add default options if not specified - config = Map.union inputConfig defaultOptions - in - Map.union - config - (defaultModules config) -- add package names for input - --- package names with modules prefix. Used for import statements -defaultModules :: Map.Map String String -> Map.Map String String -defaultModules config = - let - baseMod = config Map.! "module" - in - Map.map (baseMod ) defaultRelativeModules - --- package names -defaultRelativeModules :: Map.Map String String -defaultRelativeModules = - Map.fromList( - [ ("mod_iospec", "iospec") - , ("mod_claim", "claim") - , ("mod_fact", "fact") - , ("mod_term", "term") - , ("mod_place", "place") - , ("mod_pub", "pub") - , ("mod_fresh", "fresh") - ]) + -- Map.union is left-biased: in case of duplicates left value is kept + -- add default options if not specified + Map.union inputConfig defaultOptions -- supported options defaultOptions :: Map.Map String String From 39290994cd9d1b5223bfcde6758d68eb3f0d08a3 Mon Sep 17 00:00:00 2001 From: swiesner Date: Sun, 4 Sep 2022 00:42:47 +0200 Subject: [PATCH 15/19] Resolves majority of warnings due to unused variables, non-exhaustive patterns, redundant imports, shadowing bindings, etc. --- .../src/DerivingInstances.hs | 2 +- .../src/PrettyIOSpecs/CommonFunctions.hs | 4 ++ .../src/PrettyIOSpecs/Gobra/IOSpecs.hs | 27 +++++----- .../PrettyIOSpecs/Gobra/PermissionEncoding.hs | 52 ++++++++++++------- .../src/PrettyIOSpecs/Gobra/TermEncoding.hs | 2 +- .../PrettyIOSpecs/VeriFast/BytesEncoding.hs | 6 +-- .../src/PrettyIOSpecs/VeriFast/Content.hs | 15 +++--- .../PrettyIOSpecs/VeriFast/FactEncoding.hs | 2 +- .../src/PrettyIOSpecs/VeriFast/IOSpecs.hs | 22 ++++---- .../VeriFast/PermissionEncoding.hs | 24 +++++---- .../PrettyIOSpecs/VeriFast/TermEncoding.hs | 9 ++-- .../src/PrettyIOSpecs/VeriFast/Utils.hs | 6 ++- .../src/TamarinToTamigloo.hs | 34 ++++++------ .../src/src/Main/Mode/TamiglooMain.hs | 6 +-- 14 files changed, 121 insertions(+), 90 deletions(-) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/DerivingInstances.hs b/specification-generator/src/lib/tamigloo-compiler/src/DerivingInstances.hs index 2cc3030..88d25ff 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/DerivingInstances.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/DerivingInstances.hs @@ -4,7 +4,7 @@ module DerivingInstances( IOSpecWithDefs ) where import qualified TamiglooDatatypes as TID -import qualified Theory as T +-- import qualified Theory as T deriving instance Eq TID.SetOpId diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/CommonFunctions.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/CommonFunctions.hs index 50d414c..a1ffd79 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/CommonFunctions.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/CommonFunctions.hs @@ -72,18 +72,22 @@ expectsBin ts b = -- gives the return values (input values) of a permission permReturnTerms :: TID.IOSFormula -> [TID.IOSTerm] permReturnTerms (TID.IOSFpred pOp ts) = listPermReturnTerms pOp ts +permReturnTerms _ = error "permReturnTerms called with wrong arguments." listPermReturnTerms :: TID.PredOpId -> [a] -> [a] listPermReturnTerms (TID.Perm TID.In_RF _) ts = tail (tail ts) -- everything except src place and rid listPermReturnTerms (TID.Perm _ _) ts = [last ts] -- target place +listPermReturnTerms _ _ = error "listPermReturnTerms called with wrong arguments." -- gives the arguments (output values) of a permission permArgTerms :: TID.IOSFormula -> [TID.IOSTerm] permArgTerms (TID.IOSFpred pOp ts) = listPermArgTerms pOp ts +permArgTerms _ = error "permArgTerms called with wrong arguments." listPermArgTerms :: TID.PredOpId -> [a] -> [a] listPermArgTerms (TID.Perm TID.In_RF _) ts = take 2 ts listPermArgTerms (TID.Perm _ _) ts = init ts +listPermArgTerms _ _ = error "listPermArgTerms called with wrong arguments." diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs index 70146b6..cfeebd6 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/IOSpecs.hs @@ -20,8 +20,8 @@ import qualified IoSpecs as IOS -- import Arith (integer_of_nat) import PrettyIOSpecs.Gobra.Utils -import PrettyIOSpecs.Gobra.TermEncoding -import PrettyIOSpecs.Gobra.FactEncoding +-- import PrettyIOSpecs.Gobra.TermEncoding +-- import PrettyIOSpecs.Gobra.FactEncoding import PrettyIOSpecs.Gobra.PermissionEncoding @@ -47,7 +47,7 @@ prettyIOSpecs thy = map (\p -> (fst p, appTupel prettyIOSpecWithDef (snd p))) (IOS.extractIOSpec thy) where appTupel :: Document d => (b -> c -> d) -> (a, (b, c)) -> d - appTupel f (a, (b, c)) = f b c -- omit Psi + appTupel f (_, (b, c)) = f b c -- omit Psi -- pretty I/O spec @@ -75,11 +75,11 @@ prettyGobraIOSFormula :: Document d => TID.IOSFormula -> d prettyGobraIOSFormula f = case f of TID.IOSFpred _ _ -> prettyIOSFpred f - TID.IOSFRestr f -> parens (prettyRestrForm f) + TID.IOSFRestr rf -> parens (prettyRestrForm rf) TID.IOSFand a b -> prettyGobraIOSFormula a <> text " &&" $$ prettyGobraIOSFormula b TID.IOSFimpl a b -> parens (prettyGobraIOSFormula a) <> (text " ==>") $$ parens (prettyGobraIOSFormula b) - TID.IOSFsepConj l -> prettySepConj f - TID.IOSFex v inF -> prettyGobraIOSFormula inF -- exists only occurs for vars in Permissions for which we use getters + TID.IOSFsepConj _ -> prettySepConj f + TID.IOSFex _v inF -> prettyGobraIOSFormula inF -- exists only occurs for vars in Permissions for which we use getters TID.IOSFfa v inF -> (connectFa [v] inF) where {- @@ -123,6 +123,7 @@ prettyGobraRestrs (TID.Theory _ _ thyItems) = where getRestrName :: TID.TheoryItem -> String getRestrName (TID.RestrItem name _) = name + getRestrName _ = error "getRestrName called with wrong arguments." prettyRestrForm :: Document d => TID.RestrFormula -> d prettyRestrForm (TID.Ato atom) = prettyAtom atom @@ -151,7 +152,6 @@ showConn Form.Imp = " ==> " showConn Form.Iff = " == " - prettySepConj :: Document d => TID.IOSFormula -> d prettySepConj (TID.IOSFsepConj ls) = if TID.isPerm (head ls) @@ -163,11 +163,12 @@ prettySepConj (TID.IOSFsepConj ls) = ) else (vcat . punctuate (text " &&" ) $ map prettyGobraIOSFormula ls) +prettySepConj _ = error "prettySepConj called with wrong arguments." prettyPredUsingGetters :: Document d => TID.IOSFormula -> TID.IOSFormula -> d -prettyPredUsingGetters perm (TID.IOSFpred (TID.Pred name) ts) = - functionAppDoc (text name) (map (prettyGobraIOSTermGeneric (prettyLNTermGetPerm perm)) ts) +prettyPredUsingGetters permission (TID.IOSFpred (TID.Pred name) ts) = + functionAppDoc (text name) (map (prettyGobraIOSTermGeneric (prettyLNTermGetPerm permission)) ts) where isGetter :: TID.IOSFormula -> T.LNTerm -> Bool isGetter perm term = Map.member term (mappingRetTermsGetterTerms perm) @@ -182,11 +183,7 @@ prettyPredUsingGetters perm (TID.IOSFpred (TID.Pred name) ts) = if isGetter perm term then wrapFreshPub True (sortOfGetter perm term) $ prettyGobraLNTerm False term else prettyGobraLNTerm True term - - - - - +prettyPredUsingGetters _ _ = error "prettyPredUsingGetters called with wrong arguments." prettyIOSFpred :: Document d => TID.IOSFormula -> d prettyIOSFpred f@(TID.IOSFpred op ts) = @@ -208,7 +205,7 @@ prettyIOSFpred f@(TID.IOSFpred op ts) = (text $ prettyFact True (head fIn)) <> text (" " ++ opName ++ " ") <> (prettyGobraIOSTerm True fs) - + auxMIn _ _ _ = error "auxMIn of prettyIOSFpred called with wrong arguments." prettyIOSFpred _ = error "prettyIOSFpred not called with IOSFPred" diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/PermissionEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/PermissionEncoding.hs index 1dfa20e..db0df05 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/PermissionEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/PermissionEncoding.hs @@ -27,7 +27,7 @@ import qualified Data.ByteString.Char8 as BC -- Tamarin prover imports import Text.PrettyPrint.Class import qualified Theory as T -import Term.LTerm(sortOfLNTerm) +-- import Term.LTerm(sortOfLNTerm) -- Tamigloo imports -- ---- isabelle generated import GenericHelperFunctions(nubBy) @@ -116,20 +116,22 @@ singlePerm p@(TID.IOSFpred (TID.Perm permType name) _) = TID.Internal_R -> def <> text "\n" $$ (internBIO p) TID.In_RF -> def) <> text "\n\n" +singlePerm _ = error "singlePerm called with wrong arguments." -- application of a permission permApp :: Document d => TID.IOSFormula -> d -permApp p@(TID.IOSFpred (TID.Perm _ name) ts) = +permApp p@(TID.IOSFpred (TID.Perm _ name) _) = let terms = (map (prettyGobraIOSTerm False) $ permArgTerms p) in functionAppDoc (text name) terms +permApp _ = error "permApp called with wrong arguments." -- definition of a permission (permission encoding) permDef :: Document d => TID.IOSFormula -> d -permDef p@(TID.IOSFpred (TID.Perm _ name) ts) = +permDef p@(TID.IOSFpred (TID.Perm _ name) _) = let argTerms = permArgTerms p types = map (text . printTypeOfIOSTerm) argTerms @@ -138,10 +140,11 @@ permDef p@(TID.IOSFpred (TID.Perm _ name) ts) = termsWithType = zipWith (\a b -> text "ghost " <> a <> text " " <> b) termNames types in text "pred " <> functionAppDoc (text name) termsWithType +permDef _ = error "permDef called with wrong arguments." -- definition of the getter functions of a permission getPermDef :: Document d => TID.IOSFormula -> [d] -getPermDef p@(TID.IOSFpred (TID.Perm _ name) ts) = +getPermDef p@(TID.IOSFpred (TID.Perm _ _name) _) = map (uncurry (\nr nrt -> @@ -154,43 +157,51 @@ getPermDef p@(TID.IOSFpred (TID.Perm _ name) ts) = (zip (nameRetTerms p) (nameRetTermsWithType p)) where functionDefPerm :: Document d => TID.IOSFormula -> String -> [d] -> String -> d - functionDefPerm p@(TID.IOSFpred (TID.Perm _ _) _) name termsWithType retTermWithType = + functionDefPerm perm@(TID.IOSFpred (TID.Perm _ _) _) n termsWithType retTermWithType = text "ghost" $$ - text "requires " <> permApp p $$ - text "pure " <> functionDefDoc (text name) termsWithType (text retTermWithType) + text "requires " <> permApp perm $$ + text "pure " <> functionDefDoc (text n) termsWithType (text retTermWithType) + functionDefPerm _ _ _ _ = error "functionDefPerm called with wrong arguments." +getPermDef _ = error "getPermDef called with wrong arguments." -- the names of the return values of a permission as named as r1, ..., rn, placeDst nameRetTerms :: TID.IOSFormula -> [String] nameRetTerms p@(TID.IOSFpred (TID.Perm _ _) _) = (convenienceNames (length (permReturnTerms p) - 1) "r") ++ ["placeDst"] +nameRetTerms _ = error "nameRetTerms called with wrong arguments." -- names and types of the return values e.g. r1 Term, ..., rn Fresh, placeDst Place nameRetTermsWithType :: TID.IOSFormula -> [String] -nameRetTermsWithType p@(TID.IOSFpred (TID.Perm _ _) ts) = +nameRetTermsWithType p@(TID.IOSFpred (TID.Perm _ _) _) = zipWith (\a b -> a ++ " " ++ b) (nameRetTerms p) (map printTypeOfIOSTerm $ permReturnTerms p) +nameRetTermsWithType _ = error "nameRetTermsWithType called with wrong arguments." -- give a name to a getter function of a permission permGetterName :: TID.IOSFormula -> String -> String -permGetterName p@(TID.IOSFpred (TID.Perm _ name) _) suffix = - "get_" ++ name ++ "_" ++ suffix +permGetterName (TID.IOSFpred (TID.Perm _ name) _) suffix = + "get_" ++ name ++ "_" ++ suffix +permGetterName _ _ = error "permGetterName called with wrong arguments." -- applications of the getters of a permission getPermApp :: Document d => TID.IOSFormula -> [d] -getPermApp p@(TID.IOSFpred (TID.Perm _ _) ts) = +getPermApp p@(TID.IOSFpred (TID.Perm _ _) _) = map (\nr -> functionAppDoc (text $ permGetterName p nr) (map (prettyGobraIOSTerm False) $ permArgTerms p)) (nameRetTerms p) +getPermApp _ = error "getPermApp called with wrong arguments." -- application of a permission +{- getPermApp is used instead singleGetPermApp :: Document d => TID.IOSFormula -> Int -> d -singleGetPermApp p@(TID.IOSFpred (TID.Perm _ _) ts) idx = +singleGetPermApp p@(TID.IOSFpred (TID.Perm _ _) _) idx = let nr = (nameRetTerms p) !! idx in functionAppDoc (text $ permGetterName p nr) (map (prettyGobraIOSTerm False) $ permArgTerms p) - +singleGetPermApp _ = error "singleGetPermApp called with wrong arguments." +-} getPermToLNTerm :: TID.IOSFormula -> [T.LNTerm] -getPermToLNTerm p@(TID.IOSFpred (TID.Perm _ _) ts) = +getPermToLNTerm p@(TID.IOSFpred (TID.Perm _ _) _) = map (\suffix -> T.FAPP @@ -198,18 +209,21 @@ getPermToLNTerm p@(TID.IOSFpred (TID.Perm _ _) ts) = (map TID.getLNTermFromIOSTerm $ permArgTerms p) ) (nameRetTerms p) +getPermToLNTerm _ = error "getPermToLNTerm called with wrong arguments." getPermFunSym :: String -> TID.IOSFormula -> T.FunSym -getPermFunSym name p@(TID.IOSFpred (TID.Perm _ _) ts) = +getPermFunSym name p@(TID.IOSFpred (TID.Perm _ _) _) = T.NoEq ( BC.pack name, (length (permArgTerms p), T.Public)) +getPermFunSym _ _ = error "getPermFunSym called with wrong arguments." singleGetPermToLNTerm :: TID.IOSFormula -> Int -> T.LNTerm singleGetPermToLNTerm p idx = getPermToLNTerm p !! idx replacePermRetValues :: TID.IOSFormula -> TID.IOSFormula -> TID.IOSFormula -replacePermRetValues p@(TID.IOSFpred (TID.Perm _ _) ts) f = +replacePermRetValues p@(TID.IOSFpred (TID.Perm _ _) _) f = TID.mapTermsInFormula (\_ -> replacePermRetIOSTerm p) f +replacePermRetValues _ _ = error "replacePermRetValues called with wrong arguments." replacePermRetIOSTerm :: TID.IOSFormula -> TID.IOSTerm -> TID.IOSTerm replacePermRetIOSTerm perm term = @@ -225,7 +239,7 @@ replacePermRetIOSTerm perm term = mapFact f (TID.Fact fg ft lnTerms) = TID.Fact fg ft (map f lnTerms) replacePermRetLNTerm :: TID.IOSFormula -> T.LNTerm -> T.LNTerm -replacePermRetLNTerm p@(TID.IOSFpred (TID.Perm _ _) ts) term = +replacePermRetLNTerm p@(TID.IOSFpred (TID.Perm _ _) _) term = let maybeIdx = elemIndex term (map TID.getLNTermFromIOSTerm $ permReturnTerms p) idx = maybe 0 id maybeIdx @@ -235,6 +249,7 @@ replacePermRetLNTerm p@(TID.IOSFpred (TID.Perm _ _) ts) term = singleGetPermToLNTerm p idx else term +replacePermRetLNTerm _ _ = error "replacePermRetLNTerm called with wrong arguments." mappingRetTermsGetterTerms :: TID.IOSFormula -> Map.Map T.LNTerm T.LNTerm mappingRetTermsGetterTerms perm = @@ -263,6 +278,7 @@ internBIO p@(TID.IOSFpred (TID.Perm TID.Internal_R name) ts) = text "requires token(" <> placeSrc <> text ") && " <> permApp p $$ text "ensures token(" <> placeDst <> text ") && " <> placeDst <> text " == old(" <> (getPermApp p !! 0) <> text ")" $$ - functionDefDoc (text $ "internBIO_" ++ name) argsWithType (parens retTermWithType) + functionDefDoc (text $ "internBIO_" ++ name) argsWithType (parens retTermWithType) +internBIO _ = error "internBIO not called with the right argument." diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/TermEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/TermEncoding.hs index 611297e..2765f7f 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/TermEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/TermEncoding.hs @@ -19,7 +19,7 @@ import Term.Maude.Signature(MaudeSig, rrulesForMaudeSig, funSyms) import Term.Term.FunctionSymbols import Term.Builtin.Rules(RRule(..)) import Term.LTerm (frees) -import Term.VTerm(constsVTerm) +-- import Term.VTerm(constsVTerm) import Term.Builtin.Convenience(x1, x2, x3) import Theory.Model.Signature(_sigMaudeInfo) import qualified Theory as T diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/BytesEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/BytesEncoding.hs index 7df0af9..534f987 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/BytesEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/BytesEncoding.hs @@ -6,7 +6,7 @@ module PrettyIOSpecs.VeriFast.BytesEncoding ( import Prelude -import qualified Data.Map as Map +-- import qualified Data.Map as Map import qualified Data.Set as S import qualified Data.ByteString.Char8 as BC @@ -16,8 +16,8 @@ import Term.Term.Raw import Term.Maude.Signature(MaudeSig, rrulesForMaudeSig, funSyms) import Term.Term.FunctionSymbols import Term.Builtin.Rules(RRule(..)) -import Term.LTerm (frees) -import Term.VTerm(constsVTerm) +-- import Term.LTerm (frees) +-- import Term.VTerm(constsVTerm) --import Term.Builtin.Convenience(x1, x2, x3) import Theory.Model.Signature(_sigMaudeInfo) import qualified Theory as T diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Content.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Content.hs index 418ab28..2befe6a 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Content.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Content.hs @@ -10,18 +10,18 @@ import Prelude import qualified Data.Map as Map import Text.PrettyPrint.Class import System.FilePath -import Text.RawString.QQ +-- import Text.RawString.QQ -import qualified Theory as T -import qualified Theory.Model.Formula as Form +-- import qualified Theory as T +-- import qualified Theory.Model.Formula as Form -import TamiglooConfig +-- import TamiglooConfig import qualified TamiglooDatatypes as TID -import qualified IoSpecs as IOS +-- import qualified IoSpecs as IOS import GenericHelperFunctions(nub) -- import Arith (integer_of_nat) -import PrettyIOSpecs.VeriFast.Utils +-- import PrettyIOSpecs.VeriFast.Utils import PrettyIOSpecs.VeriFast.TermEncoding import PrettyIOSpecs.VeriFast.FactEncoding import PrettyIOSpecs.VeriFast.PermissionEncoding @@ -92,10 +92,11 @@ dirPath config packageName fileName dependencies body = , (javaspecPath, javaspecContent) ] +{- dropPrefix :: Eq a => [a] -> [a] -> [a] dropPrefix [] l = l dropPrefix _ [] = error "Prefix is longer than list." dropPrefix (p:ps) (x:xs) = if p == x then dropPrefix ps xs else error "Not a prefix." - +-} diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/FactEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/FactEncoding.hs index 58d59e0..9276c49 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/FactEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/FactEncoding.hs @@ -7,7 +7,7 @@ module PrettyIOSpecs.VeriFast.FactEncoding ( -- import Prelude -import qualified Data.Map as Map +-- import qualified Data.Map as Map -- Tamarin prover imports import Text.PrettyPrint.Class diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/IOSpecs.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/IOSpecs.hs index 1b3f421..f4f2a4f 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/IOSpecs.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/IOSpecs.hs @@ -11,13 +11,13 @@ module PrettyIOSpecs.VeriFast.IOSpecs ( ) where import Prelude -import qualified Data.Map as Map +-- import qualified Data.Map as Map import Text.PrettyPrint.Class import Data.List(delete) -import Data.List.Split +-- import Data.List.Split -import qualified Theory as T +-- import qualified Theory as T import qualified Theory.Model.Formula as Form import qualified TamiglooDatatypes as TID @@ -37,7 +37,7 @@ prettyIOSpecs thy = map (\p -> (fst p, appTupel prettyIOSpecWithDef (snd p) (fst p))) (IOS.extractIOSpec thy) where appTupel :: Document d => (b -> c -> (String -> d)) -> (a, (b, c)) -> (String -> d) - appTupel f (a, (b, c)) = f b c -- omit Psi + appTupel f (_, (b, c)) = f b c -- omit Psi -- pretty I/O spec prettyIOSpecWithDef :: Document d => (TID.IOSFormula, TID.IOSFormula) -> [(TID.IOSFormula, TID.IOSFormula)] -> String -> d @@ -95,7 +95,8 @@ collectFa qs (TID.IOSFfa v formula) = collectFa (qs ++ [v]) formula collectFa qs _ = qs nameContainerConstr :: TID.IOSFormula -> String -nameContainerConstr (TID.IOSFpred (TID.Pred name) ts) = GHF.prependToString "quant" name +nameContainerConstr (TID.IOSFpred (TID.Pred name) _) = GHF.prependToString "quant" name +nameContainerConstr _ = error "nameContainerConstr called with wrong arguments." @@ -140,16 +141,16 @@ prettyVFIOSFormula :: Document d => TID.IOSFormula -> d prettyVFIOSFormula f = case f of TID.IOSFpred _ _ -> prettyIOSFpred f - TID.IOSFRestr f -> parens (prettyRestrForm f) + TID.IOSFRestr rf -> parens (prettyRestrForm rf) TID.IOSFand a b -> prettyVFIOSFormula a <> text " &&" $$ prettyVFIOSFormula b TID.IOSFimpl a b -> (prettyVFIOSFormula a) $$ (text "?") $$ parens (prettyVFIOSFormula b) $$ text ":" $$ text "true" TID.IOSFsepConj _ -> prettySepConj f - TID.IOSFex v inF -> prettyVFIOSFormula inF -- exists only occurs for vars in Permissions for which we use getters + TID.IOSFex _v inF -> prettyVFIOSFormula inF -- exists only occurs for vars in Permissions for which we use getters TID.IOSFfa v inF -> (connectFa [v] inF) where connectFa :: Document d => [TID.IOSTerm] -> TID.IOSFormula -> d connectFa qs (TID.IOSFfa v formula) = connectFa (qs ++ [v]) formula - connectFa qs formula = (prettyVFIOSFormula formula) + connectFa _qs formula = (prettyVFIOSFormula formula) @@ -174,7 +175,7 @@ prettyRestrForm :: Document d => TID.RestrFormula -> d prettyRestrForm (TID.Ato atom) = prettyAtom atom prettyRestrForm (TID.Not f) = text "!(" <> prettyRestrForm f <> text ")" prettyRestrForm (TID.Conn conn l r) = prettyConn conn (parens (prettyRestrForm l)) (parens (prettyRestrForm r)) -prettyRestrForm (TID.RFA t f) = error "Patterns in definitions of restrictions not supported in VeriFast." -- text "(" <> (connectRFA [t] f) <> text ")" +prettyRestrForm (TID.RFA _t _f) = error "Patterns in definitions of restrictions not supported in VeriFast." -- text "(" <> (connectRFA [t] f) <> text ")" {- where connectRFA :: Document d => [T.LNTerm] -> TID.RestrFormula -> d @@ -212,11 +213,13 @@ prettyConn Form.Iff l r = l <> text " == " <> r prettySepConj :: Document d => TID.IOSFormula -> d prettySepConj (TID.IOSFsepConj ls) = (vcat . punctuate (text " &*&" ) $ map prettyVFIOSFormula ls) +prettySepConj _ = error "prettySepConj called with wrong arguments." prettySepConjIterSepConj :: Document d => TID.IOSFormula -> d prettySepConjIterSepConj (TID.IOSFsepConj ls) = (vcat . punctuate (text " &*&" ) $ map (\l -> functionAppDoc (text "bigstar") [prettyVFIOSFormula l, text "nil"] ) ls) +prettySepConjIterSepConj _ = error "prettySepConjIterSepConj called with wrong arguments." -- pred @@ -240,6 +243,7 @@ prettyIOSFpred f@(TID.IOSFpred op ts) = auxMIn :: Document d => TID.IOSTerm -> TID.IOSTerm -> d auxMIn (TID.IOSTermFacts fIn) fs = functionAppDocMLine (text "msetIn") [text (prettyFact True (head fIn)), (prettyVFIOSTerm True fs)] + auxMIn _ _ = error "auxMIn of prettyIOSFpred called with wrong arguments." prettyIOSFpred _ = error "prettyIOSFpred not called with IOSFPred" diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/PermissionEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/PermissionEncoding.hs index f16e445..7e54097 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/PermissionEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/PermissionEncoding.hs @@ -14,15 +14,15 @@ module PrettyIOSpecs.VeriFast.PermissionEncoding ( -- import Prelude -import qualified Data.Map as Map -import Data.Maybe(isJust) -import Data.List(elemIndex) -import qualified Data.ByteString.Char8 as BC +-- import qualified Data.Map as Map +-- import Data.Maybe(isJust) +-- import Data.List(elemIndex) +-- import qualified Data.ByteString.Char8 as BC -- Tamarin prover imports import Text.PrettyPrint.Class -import qualified Theory as T -import Term.LTerm(sortOfLNTerm) +-- import qualified Theory as T +-- import Term.LTerm(sortOfLNTerm) -- Tamigloo imports -- ---- isabelle generated import GenericHelperFunctions(nubBy) @@ -79,7 +79,7 @@ permEncoding formulas permType = -- encoding of a single permission singlePerm :: Document d => TID.IOSFormula -> d -singlePerm p@(TID.IOSFpred (TID.Perm permType name) _) = +singlePerm p@(TID.IOSFpred (TID.Perm permType _name) _) = let def = (permDef p) -- perm @@ -89,17 +89,19 @@ singlePerm p@(TID.IOSFpred (TID.Perm permType name) _) = TID.Internal_R -> def <> text "\n" $$ (internBIO p) TID.In_RF -> def) <> text "\n\n" +singlePerm _ = error "singlePerm called with wrong arguments." -- definition of a permission (permission encoding) permDef :: Document d => TID.IOSFormula -> d -permDef p@(TID.IOSFpred (TID.Perm _ name) ts) = +permDef (TID.IOSFpred (TID.Perm _ name) ts) = let termsWithType = map (\t -> text (printTypeOfIOSTerm t) <> text " " <> (prettyVFIOSTerm False) t) ts in text "predicate " <> functionAppDoc (text name) termsWithType <> text ";" +permDef _ = error "permDef called with wrong arguments." permAppQ :: Document d => TID.IOSFormula -> d -permAppQ p@(TID.IOSFpred (TID.Perm permType name) ts) = +permAppQ (TID.IOSFpred (TID.Perm permType name) ts) = let pOp = (TID.Perm permType name) termDocs = map (prettyVFIOSTerm False) ts @@ -109,6 +111,7 @@ permAppQ p@(TID.IOSFpred (TID.Perm permType name) ts) = retsQ = map (\r -> text "?" <> r) rets in functionAppDoc (text name) (args ++ retsQ) +permAppQ _ = error "permAppQ called with wrong arguments." -- definition of an internal basic input output operation internBIO :: Document d => TID.IOSFormula -> d @@ -131,4 +134,5 @@ internBIO p@(TID.IOSFpred (TID.Perm TID.Internal_R name) ts) = argsWithType (text "token(" <> placeSrc <> text ") &*& " <> permApp) (text "token(" <> placeDst <> text ")") - (text "assume(false);") \ No newline at end of file + (text "assume(false);") +internBIO _ = error "internBIO called with wrong arguments." \ No newline at end of file diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/TermEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/TermEncoding.hs index 51ca796..f77990d 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/TermEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/TermEncoding.hs @@ -20,13 +20,13 @@ import qualified Data.Set as S import qualified Data.ByteString.Char8 as BC -- Tamarin prover imports import Text.PrettyPrint.Class -import Term.Term.Raw +-- import Term.Term.Raw import Term.Maude.Signature(MaudeSig, rrulesForMaudeSig, funSyms) import Term.Term.FunctionSymbols -import Term.Builtin.Rules(RRule(..)) +-- import Term.Builtin.Rules(RRule(..)) import Term.LTerm (frees) -import Term.VTerm(constsVTerm) -import Term.Builtin.Convenience(x1, x2, x3) +-- import Term.VTerm(constsVTerm) +-- import Term.Builtin.Convenience(x1, x2, x3) import Theory.Model.Signature(_sigMaudeInfo) import qualified Theory as T -- Tamigloo imports @@ -93,6 +93,7 @@ funcACLemmas ppACLemma fSyms = ppACLemmas :: Document d => FunSym -> d ppACLemmas (AC o) = nameACLemmas "Term" (reservedVeriFastWords (show o)) +ppACLemmas _ = error "ppACLemmas called with wrong arguments." nameACLemmas :: Document d => String -> String -> d nameACLemmas typeId name = diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Utils.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Utils.hs index aba200d..e59f11a 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Utils.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/VeriFast/Utils.hs @@ -24,7 +24,7 @@ module PrettyIOSpecs.VeriFast.Utils ( -- import Prelude -import qualified Data.Map as Map +-- import qualified Data.Map as Map import qualified Data.ByteString.Char8 as BC -- Tamarin prover imports @@ -36,11 +36,13 @@ import qualified Theory as T -- Tamigloo imports -- ---- isabelle generated -import GenericHelperFunctions(nub) +-- import GenericHelperFunctions(nub) import qualified TamiglooDatatypes as TID +{- in case a debug output is created import qualified ProtocolFormat as PF import qualified InterfaceModel as IM import qualified Decomposition as D +-} import qualified IoSpecs as IOS -- ---- other Tamigloo modules import DerivingInstances() diff --git a/specification-generator/src/lib/tamigloo-compiler/src/TamarinToTamigloo.hs b/specification-generator/src/lib/tamigloo-compiler/src/TamarinToTamigloo.hs index d1d5f1a..7f468ef 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/TamarinToTamigloo.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/TamarinToTamigloo.hs @@ -21,7 +21,7 @@ import qualified Data.Set as S -- Tamarin prover imports import qualified Theory as T -import Theory.Model.Signature (SignaturePure) +-- import Theory.Model.Signature (SignaturePure) import qualified Theory.Model.Fact as F import qualified Theory.Model.Rule as R import qualified Theory.Model.Restriction as Restr @@ -34,7 +34,7 @@ import Text.Parsec hiding ((<|>)) -- Tamigloo imports -- ---- isabelle generated -import DerivingInstances +import DerivingInstances() import qualified TamiglooDatatypes as TID import qualified GenericHelperFunctions as TamiHelper @@ -97,7 +97,7 @@ checkRestrFormat (Restr.Restriction _name f) = checkFormFormat f && length (T.fo logConn :: Form.LNFormula -> Bool logConn (Form.Ato (Atom.EqE _ _)) = True logConn (Form.TF _) = True - logConn (Form.Not f) = logConn f + logConn (Form.Not form) = logConn form logConn (Form.Conn _ l r) = logConn l && logConn r logConn _ = False checkFormFormat :: Form.LNFormula -> Bool @@ -110,16 +110,17 @@ checkRestrFormat (Restr.Restriction _name f) = checkFormFormat f && length (T.fo -- checks that vars used in RHS of implication are subset of vars used in LHS/Fact -- assumes that ForAll quanitifiers are only used to wrap the overall formula, thus the same de brujin index corresponds to same quantified var checkBVars :: Form.LNFormula -> Bool -- TODO add checkBVars to checkRestrFormat - checkBVars (Form.Qua Form.All _hint (Form.Conn conn l r)) = + checkBVars (Form.Qua Form.All _hint (Form.Conn _conn l r)) = all id $ map (\e -> (elem) e (collectBVarsDups l)) (collectBVarsDups r) checkBVars (Form.Qua Form.All _hint nestedF) = checkBVars nestedF checkBVars _ = False collectBVarsDups :: Form.LNFormula -> [Integer] -- contains duplicates collectBVarsDups (Form.Ato (Atom.EqE t1 t2)) = getIntBVars t1 ++ getIntBVars t2 collectBVarsDups (Form.Ato _) = [] -- does not conform to format - collectBVarsDups (Form.Not f) = collectBVarsDups f + collectBVarsDups (Form.Not form) = collectBVarsDups form collectBVarsDups (Form.Conn _ l r) = collectBVarsDups l ++ collectBVarsDups r - collectBVarsDups (Form.Qua _ _ f) = collectBVarsDups f + collectBVarsDups (Form.Qua _ _ form) = collectBVarsDups form + collectBVarsDups (Form.TF _) = [] getIntBVars :: T.VTerm c (T.BVar T.LVar) -> [Integer] getIntBVars t = map (\(T.Bound i) -> i) (T.varsVTerm t) checkRestrFormat _ = False @@ -139,6 +140,7 @@ changeLNFormToTamiForm (Form.Qua _ _ f) = changeLNFormToTamiForm f changeTypeProtoAtom :: (Atom.ProtoAtom s (T.VTerm T.Name (T.BVar v))) -> TID.Atom changeTypeProtoAtom (Atom.Action _ f) = TID.Atom (factBVarToTIDFact f) changeTypeProtoAtom (Atom.EqE t1 t2) = TID.EqE (bVarTermToLNTerm t1) (bVarTermToLNTerm t2) +changeTypeProtoAtom _ = error "changeTypeProtoAtom called with wrong arguments." -- change to TID.Fact -- only used in restrictions: abuse LVar's index to represent De Brujin indices of BVar @@ -208,7 +210,7 @@ createConsistencyMap thy = foldr getConsist Map.empty facts where getConsist :: TID.Fact -> Map.Map TID.FactTag TID.FactGroup -> Map.Map TID.FactTag TID.FactGroup - getConsist fact@(TID.Fact fg ft _) cMap = + getConsist (TID.Fact fg ft _) cMap = let mostSpec = (mostSpecificFactGroup (cMap Map.! ft) fg) ifRightMostSpec = fromRight (error $ errMsgConsistency ft) mostSpec @@ -335,11 +337,11 @@ changeActFact :: F.LNFact -> TID.Fact changeActFact (F.Fact tag _ terms) = changeFreshPubToMsg $ TID.Fact TID.ActionGroup (changeFactTag tag) terms changeFreshPubToMsg :: TID.Fact -> TID.Fact -changeFreshPubToMsg f@(TID.Fact fg ft lnTerms) = +changeFreshPubToMsg (TID.Fact fg ft lnTerms) = TID.Fact fg ft (map (fmap (fmap freshPubLVarToMsg)) lnTerms) where freshPubLVarToMsg :: T.LVar -> T.LVar - freshPubLVarToMsg lvar@(T.LVar name lsort lindex) = + freshPubLVarToMsg (T.LVar name lsort lindex) = T.LVar name (newLsort lsort) lindex newLsort :: T.LSort -> T.LSort newLsort s = case s of @@ -367,7 +369,7 @@ getNameProtoRuleEInfo r | (_:_) <- R._preRestriction r = error $ "Unexpected non-empty _preRestriction in ProtoRuleEInfo: "++ show r errMsgIsRule :: T.OpenProtoRule -> String -errMsgIsRule r@(T.OpenProtoRule (R.Rule i p c a _) _) = +errMsgIsRule (T.OpenProtoRule (R.Rule i p c a _) _) = "Error trying to parse (OpenProto)Rule:\n" ++ " The rule '" ++ getNameProtoRuleEInfo i ++ "' does not adhere to formatting assumptions.\n" ++ " It is not a protocol rule:\n" ++ @@ -379,7 +381,7 @@ errMsgIsRule r@(T.OpenProtoRule (R.Rule i p c a _) _) = formatMsg (isEnvRuleBoolList p a c) where formatMsg :: [(Bool, String)] -> String - formatMsg boolList = unlines $ map (\p -> " - " ++ snd p ++ ": " ++ show (fst p)) boolList + formatMsg boolList = unlines $ map (\pa -> " - " ++ snd pa ++ ": " ++ show (fst pa)) boolList @@ -388,7 +390,7 @@ isStateRule pr act cncl = and $ TamiHelper.fstList $ isStateRuleBoolList pr act -- list can be used for error msgs isStateRuleBoolList :: [F.LNFact] -> [F.LNFact] -> [F.LNFact] -> [(Bool, String)] -isStateRuleBoolList pr act cncl = +isStateRuleBoolList pr _act cncl = [ (isStateOrSetupPr pr, "premise contains a state or setup fact") , (isStateCncl cncl, "conclusion contains a state fact") ] @@ -407,7 +409,7 @@ isEnvRule pr act cncl = and $ TamiHelper.fstList $ isEnvRuleBoolList pr act cncl isEnvRuleBoolList :: [F.LNFact] -> [F.LNFact] -> [F.LNFact] -> [(Bool, String)] -isEnvRuleBoolList pr act cncl = +isEnvRuleBoolList pr _act cncl = [ (all (not . isStateFact) pr, "no state facts in premise") , (all (not . isStateFact) cncl, "no state facts in conclusion") ] @@ -503,13 +505,15 @@ factName :: F.LNFact -> String factName = (F.factTagName . F.factTag) -- all and at least one +{- allAndOne :: (a->Bool) -> [a] -> Bool allAndOne _ [] = False allAndOne f xs = all f xs - +-} allSame :: (Eq a) => [a] -> Bool allSame xs = and $ map (uncurry (==)) $ zip xs $ tail xs +{- intersectEq :: (a -> a -> Bool) -> [a] -> [a] -> [a] intersectEq _f [] _ = [] intersectEq _f _ [] = [] @@ -517,5 +521,5 @@ intersectEq f (a:as) bs = if (any (f a) bs) then a : intersectEq f as bs else intersectEq f as bs - +-} diff --git a/specification-generator/src/src/Main/Mode/TamiglooMain.hs b/specification-generator/src/src/Main/Mode/TamiglooMain.hs index 7d5464c..81a6355 100644 --- a/specification-generator/src/src/Main/Mode/TamiglooMain.hs +++ b/specification-generator/src/src/Main/Mode/TamiglooMain.hs @@ -6,7 +6,7 @@ module Main.Mode.TamiglooMain ( ) where import Prelude -import Theory.Text.Pretty +-- import Theory.Text.Pretty import qualified Text.PrettyPrint.Class as Pretty --import System.FilePath --import Theory.Text.Parser.Token(parseFile) @@ -17,15 +17,13 @@ import Main.TheoryLoader(loadOpenThy) import qualified Theory as T import TamarinToTamigloo import TamiglooConfig -import qualified TamiglooDatatypes as TID +-- import qualified TamiglooDatatypes as TID -- import PrettyIOSpecs.PrettyDebug as Debug import qualified PrettyIOSpecs.Gobra.Content as Gobra import qualified PrettyIOSpecs.VeriFast.Content as VF - - import System.Directory (createDirectoryIfMissing) import System.FilePath From 63cbc50c2952baa0bdbb7ef5433116420d4e6945 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 16 Sep 2025 16:14:35 +0200 Subject: [PATCH 16/19] updates I/O spec generator to latest syntax changes in Gobra --- .../tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs | 4 ++++ .../src/PrettyIOSpecs/Gobra/PermissionEncoding.hs | 2 ++ .../lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs | 2 +- 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs index f274625..aa8bd4e 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs @@ -214,6 +214,7 @@ mFunc :: Document d => d mFunc = text "ghost" $$ text "ensures res == (linearFacts(l) subset s && persistentFacts(l) subset s)" $$ + text "decreases" $$ text "pure func M(l mset[Fact], s mset[Fact]) (res bool) {" $$ nest 4 ( text "// non-persistent facts" $$ @@ -231,6 +232,7 @@ uFunc :: Document d => d uFunc = text "ghost" $$ text "ensures result == s setminus linearFacts(l) union r" $$ + text "decreases" $$ text "pure func U(l mset[Fact], r mset[Fact], s mset[Fact]) (result mset[Fact])" {- ---- -} @@ -240,6 +242,7 @@ filterIsPersFunc = text "ghost" $$ text "// returns a multiset containing just the persistent facts of l all with multiplicity 1" $$ text "ensures forall f Fact :: { f # result } (f # result) == (persistent(f) && (f # l) > 0 ? 1 : 0)" $$ + text "decreases" $$ text "pure func persistentFacts(l mset[Fact]) (result mset[Fact])" {- ---- -} @@ -249,6 +252,7 @@ filterIsLinFunc = text "ghost" $$ text "// returns a multiset containing just the non-persistent facts of l while retaining their multiplicity" $$ text "ensures forall f Fact :: { f # result } (f # result) == (persistent(f) ? 0 : (f # l))" $$ + text "decreases" $$ text "pure func linearFacts(l mset[Fact]) (result mset[Fact])" diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/PermissionEncoding.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/PermissionEncoding.hs index db0df05..7bcebc9 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/PermissionEncoding.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/PermissionEncoding.hs @@ -160,6 +160,7 @@ getPermDef p@(TID.IOSFpred (TID.Perm _ _name) _) = functionDefPerm perm@(TID.IOSFpred (TID.Perm _ _) _) n termsWithType retTermWithType = text "ghost" $$ text "requires " <> permApp perm $$ + text "decreases" $$ text "pure " <> functionDefDoc (text n) termsWithType (text retTermWithType) functionDefPerm _ _ _ _ = error "functionDefPerm called with wrong arguments." getPermDef _ = error "getPermDef called with wrong arguments." @@ -278,6 +279,7 @@ internBIO p@(TID.IOSFpred (TID.Perm TID.Internal_R name) ts) = text "requires token(" <> placeSrc <> text ") && " <> permApp p $$ text "ensures token(" <> placeDst <> text ") && " <> placeDst <> text " == old(" <> (getPermApp p !! 0) <> text ")" $$ + text "decreases" $$ functionDefDoc (text $ "internBIO_" ++ name) argsWithType (parens retTermWithType) internBIO _ = error "internBIO not called with the right argument." diff --git a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs index f42d86e..bb6e655 100644 --- a/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs +++ b/specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs @@ -337,7 +337,7 @@ importHeader config importedPackages = domain :: Document d => String -> d -> d domain name doc = - braces' (text ("type " ++ name ++ " domain")) doc + braces' (text ("ghost type " ++ name ++ " domain")) doc forallWithTriggerSetting :: Document d => TriggerSetting -> d -> [d] -> d -> d From 66c8d2ad23bfb0899ff418f29269e6361bae2864 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Sun, 21 Sep 2025 15:18:20 +0200 Subject: [PATCH 17/19] updates WireGuard oracle to Python3, updates Dockerfile such that it builds again --- tamarin-docker/Dockerfile | 36 +++++++++++++++++--------------- wireguard/model/wireguard.oracle | 9 +++----- 2 files changed, 22 insertions(+), 23 deletions(-) diff --git a/tamarin-docker/Dockerfile b/tamarin-docker/Dockerfile index 517a60f..cc9dfbe 100644 --- a/tamarin-docker/Dockerfile +++ b/tamarin-docker/Dockerfile @@ -1,28 +1,29 @@ -# the image for verifying the Tamarin model is based on Python2 because `wireguard.oracle` -# is a Python file that has to be executed with Python2. -FROM python:2.7 +FROM debian:bookworm-slim@sha256:df52e55e3361a81ac1bead266f3373ee55d29aa50cf0975d440c2be3483d8ed3 +# note that trixie does not have `libtinfo5` anymore (but `libtinfo6` which doesn't work with the current Maude version) RUN apt-get update && \ apt-get install -y \ curl \ - zip \ - locales \ - graphviz \ # libtinfo5 is needed by maude - libtinfo5 + libtinfo5 \ + locales \ + # we need python for our Tamarin oracle: + python3 \ + # vim is only provided for convenience: + vim \ + wget \ + zip \ + make \ + git # `/.local/bin` is the installation location of Tamarin and its dependencies RUN mkdir -p /.local/bin ENV PATH=/.local/bin:$PATH -# install Haskell stack -RUN curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C /.local/bin '*/stack' && \ - chmod a+x /.local/bin/stack && \ - stack --no-terminal setup - # install Maude -ENV TAMARIN_VERSION 1.6.0 -ENV MAUDE_URL https://github.com/tamarin-prover/tamarin-prover/releases/download/$TAMARIN_VERSION/Maude-2.7.1-linux.zip +ENV TAMARIN_RELEASE_VERSION_FOR_MAUDE="1.6.0" +ENV MAUDE_VERSION="2.7.1" +ENV MAUDE_URL="https://github.com/tamarin-prover/tamarin-prover/releases/download/$TAMARIN_RELEASE_VERSION_FOR_MAUDE/Maude-$MAUDE_VERSION-linux.zip" RUN curl -q -s -S -L --create-dirs -o maude.zip $MAUDE_URL && \ unzip maude.zip -d /.local/bin/ && \ rm maude.zip && \ @@ -30,6 +31,7 @@ RUN curl -q -s -S -L --create-dirs -o maude.zip $MAUDE_URL && \ chmod a+x /.local/bin/maude # install tamarin-prover +ENV TAMARIN_VERSION="1.10.0" RUN curl -q -s -S -L --create-dirs -o tamarin.tar.gz https://github.com/tamarin-prover/tamarin-prover/releases/download/$TAMARIN_VERSION/tamarin-prover-$TAMARIN_VERSION-linux64-ubuntu.tar.gz && \ tar -x -C /.local/bin/ -f tamarin.tar.gz && \ rm tamarin.tar.gz && \ @@ -39,9 +41,9 @@ RUN curl -q -s -S -L --create-dirs -o tamarin.tar.gz https://github.com/tamarin- USER root RUN sed -i '/en_US.UTF-8/s/^# //g' /etc/locale.gen && \ locale-gen -ENV LANG en_US.UTF-8 -ENV LANGUAGE en_US:en -ENV LC_ALL en_US.UTF-8 +ENV LANG="en_US.UTF-8" +ENV LANGUAGE="en_US:en" +ENV LC_ALL="en_US.UTF-8" WORKDIR /tamarin COPY dh/model/dh.spthy . diff --git a/wireguard/model/wireguard.oracle b/wireguard/model/wireguard.oracle index 1b2ba55..63ca07b 100755 --- a/wireguard/model/wireguard.oracle +++ b/wireguard/model/wireguard.oracle @@ -1,9 +1,7 @@ -#!/usr/bin/python2 +#!/usr/bin/python3 import re -import os import sys -debug = True lines = sys.stdin.readlines() lemma = sys.argv[1] @@ -17,7 +15,7 @@ lemma = sys.argv[1] rank = [] # list of list of goals, main list is ordered by priority maxPrio = 110 -for i in range(0,maxPrio): +for i in range(0, maxPrio): rank.append([]) # SOURCES LEMMAS @@ -39,5 +37,4 @@ else: for listGoals in reversed(rank): for goal in listGoals: sys.stderr.write(goal) - print goal - + print(goal) From 66316cb8cf55a0bc15f67a2f8c06a3203e7b8937 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Sun, 21 Sep 2025 15:19:27 +0200 Subject: [PATCH 18/19] adds dependabot --- .github/dependabot.yml | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 .github/dependabot.yml diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 0000000..13109b4 --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,12 @@ +version: 2 + +updates: + - package-ecosystem: github-actions + directory: "/" + schedule: + interval: monthly + day: monday + groups: + all: + patterns: + - "*" From f743167d72f6113dab83c1c48e5041f690dad855 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Sun, 21 Sep 2025 15:25:33 +0200 Subject: [PATCH 19/19] fixes scripts for running Tamarin to disables timeouts while checking well-formedness --- tamarin-docker/verify-dh.sh | 2 +- tamarin-docker/verify-wireguard.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tamarin-docker/verify-dh.sh b/tamarin-docker/verify-dh.sh index 654a4f9..6f471cf 100755 --- a/tamarin-docker/verify-dh.sh +++ b/tamarin-docker/verify-dh.sh @@ -1,3 +1,3 @@ #!/bin/bash -tamarin-prover --prove dh.spthy +tamarin-prover --derivcheck-timeout=0 --prove dh.spthy diff --git a/tamarin-docker/verify-wireguard.sh b/tamarin-docker/verify-wireguard.sh index 0e6c1bf..13e1d27 100755 --- a/tamarin-docker/verify-wireguard.sh +++ b/tamarin-docker/verify-wireguard.sh @@ -1,3 +1,3 @@ #!/bin/bash -tamarin-prover --heuristic=O --oraclename="wireguard.oracle" --prove wireguard.spthy +tamarin-prover --derivcheck-timeout=0 --heuristic=O --oraclename="wireguard.oracle" --prove wireguard.spthy