MSR to ProVerif translation (#538)

Co-authored-by: Julian Biehl <julianbiehl@yahoo.de>

lib/export/tamarin-prover-export.cabal

@@ -64,3 +64,4 @@ library
 
     exposed-modules:
         Export
+        RuleTranslation

lib/sapic/src/Sapic/Compression.hs

@@ -59,16 +59,16 @@ getProducedFacts rules = facts
                            ) S.empty rules
 
 mergeInfo :: ProtoRuleEInfo -> ProtoRuleEInfo -> ProtoRuleEInfo
-mergeInfo info info2 =
+mergeInfo (ProtoRuleEInfo (StandRule name) attr res) (ProtoRuleEInfo (StandRule name2) attr2 res2) =
   ProtoRuleEInfo (StandRule (mergeStand name name2)) (mergeAttr attr attr2) (res ++ res2)
- where ProtoRuleEInfo (StandRule name ) attr  res  = info
-       ProtoRuleEInfo (StandRule name2) attr2 res2 = info2
+ where
        mergeStand n _ = n  -- ++ "_" ++ n'
        -- NOTE: concatenating makes veryyyy big name rules, that completely make the the graphs unreadble
        -- NOTE: if we reintroduce Yavor's Dot output, recall 9e7e99fe070776172bd09cb977e8d3a83da3ed51
        mergeAttr a a' =  let completeList = a ++ a' in
                             take 1 [i |  i@(RuleColor _) <- completeList]
                          ++ take 1 [i |  i@(Process   _) <- completeList]
+mergeInfo _ _ = error "FreshRule(s) passed to mergeInfo"
 
 
 canMerge  :: Bool -> Rule ProtoRuleEInfo -> Rule ProtoRuleEInfo -> Bool

lib/sapic/src/Sapic/Exceptions.hs

@@ -12,7 +12,8 @@
 module Sapic.Exceptions (
     WFLockTag(..),
     WFerror(..),
-    SapicException(..)
+    SapicException(..),
+    ExportException(..)
 , prettySapicException) where
 import Data.Typeable
 import Data.Set as S
@@ -60,6 +61,24 @@ data SapicException p = NotImplementedError String
                     | CannotExpandPredicate FactTag SyntacticRestriction
     deriving (Typeable)
 
+data ExportException = UnsupportedBuiltinMS
+                       | UnsupportedBuiltinBP
+                       | UnsupportedTypes [String]
+
+instance Show ExportException where
+
+    show (UnsupportedTypes incorrectFunctionUsages) = do
+        let functionsString = List.intercalate ", " incorrectFunctionUsages
+        (case length functionsString of
+          1 -> "The function " ++ functionsString ++ ", which is declared with a user-defined type, appears in a rewrite rule. "
+          _ -> "The functions " ++ functionsString ++ ", which are declared with a user-defined type, appear in a rewrite rule. ")
+        ++ "However, the translation of rules only works with bitstrings at the moment."
+    show unsuppBuiltin = 
+        "The builtins bilinear-pairing and multiset are not supported for export. However, your model uses " ++
+        (case unsuppBuiltin of
+            UnsupportedBuiltinBP -> "bilinear-pairing."
+            UnsupportedBuiltinMS -> "multiset.")
+
 prettyVarSet :: S.Set LVar -> String
 prettyVarSet = List.intercalate ", "  . List.map show . toList
 
@@ -124,3 +143,4 @@ instance Show WFerror where
 
 instance Exception WFerror
 instance (Typeable a, Show a) => Exception (SapicException a)
+instance Exception ExportException

lib/sapic/src/Sapic/Facts.hs

@@ -11,10 +11,12 @@ module Sapic.Facts (
    , TransFact(..)
    , SpecialPosition(..)
    , AnnotatedRule(..)
+   , FactType(..)
    , mapAct
    , StateKind(..)
    , isSemiState
    , isState
+   , isFrFact
    , isOutFact
    , isStateFact
    , isLetFact
@@ -30,6 +32,10 @@ module Sapic.Facts (
    , varMID
    , varProgress
    , msgVarProgress
+   , patternInsFilter
+   , nonPatternInsFilter
+   , isPattern
+   , hasPattern
    , propagateNames
 ) where
 -- import Data.Maybe
@@ -122,6 +128,10 @@ data AnnotatedRule ann = AnnotatedRule {
     , index        :: Int             -- Index to distinguish multiple rules originating from the same process
 }
 
+-- | Fact types used by the MSR to ProverIf translation.
+data FactType = GET | IN | NEW | EVENT | INSERT | OUT
+  deriving Eq
+
 -- | applies function acting on rule taple on annotated rule.
 mapAct :: (([TransFact], [TransAction], [TransFact],[SyntacticLNFormula])
            -> ([TransFact], [TransAction], [TransFact],[SyntacticLNFormula]))
@@ -262,6 +272,10 @@ isOutFact :: Fact t -> Bool
 isOutFact (Fact OutFact _ _) = True
 isOutFact _                 = False
 
+isFrFact :: Fact t -> Bool
+isFrFact (Fact FreshFact _ _) = True
+isFrFact _                 = False
+
 
 isLetFact :: Fact LNTerm -> Bool
 isLetFact (Fact (ProtoFact _ name _) _ _) =
@@ -281,6 +295,19 @@ isLockFact (Fact (ProtoFact _ name _) _ _) =
   "L_CellLocked" `List.isPrefixOf` name
 isLockFact _ = False
 
+patternInsFilter :: LNFact -> Bool
+patternInsFilter f = isInFact f && hasPattern f
+
+nonPatternInsFilter :: LNFact -> Bool
+nonPatternInsFilter f = isInFact f && not (hasPattern f)
+
+isPattern :: Term l -> Bool
+isPattern t = case viewTerm t of
+    Lit _ -> False
+    _     -> True
+
+hasPattern :: LNFact -> Bool
+hasPattern (Fact _ _ ts) = any isPattern ts
 
 prettyEitherPositionOrSpecial:: Either ProcessPosition SpecialPosition -> String
 prettyEitherPositionOrSpecial (Left pos) = prettyPosition pos

lib/theory/src/Theory/Constraint/Solver/Contradictions.hs

@@ -146,9 +146,9 @@ maybeNonNormalTerms :: MaudeHandle -> System -> [LNTerm]
 maybeNonNormalTerms hnd se =
     sortednub . concatMap getTerms . M.elems . L.get sNodes $ se
     where getTerms (Rule _ ps cs as nvs) = do
-          f <- ps++cs++as
-          t <- factTerms f ++ nvs
-          maybeNotNfSubterms (mhMaudeSig hnd) t
+           f <- ps++cs++as
+           t <- factTerms f ++ nvs
+           maybeNotNfSubterms (mhMaudeSig hnd) t
 
 substCreatesNonNormalTerms :: MaudeHandle -> System -> LNSubst -> LNSubstVFresh -> Bool
 substCreatesNonNormalTerms hnd sys fsubst =