ctd automata model checking

smucclaw · Sep 18, 2021 · 028aebc · 028aebc
1 parent 9fe2292
commit 028aebc
Show file tree

Hide file tree

Showing 6 changed files with 151 additions and 83 deletions.
diff --git a/l4/speedlimit_sorted.l4 b/l4/speedlimit_sorted.l4
@@ -237,7 +237,8 @@ maxSpeed instCar instDay instRoad instSpeed1
 # Not valid, countermodel for example for a vehicle that is not a car.
 assert {SMT:
            {valid,
-            rules: {del : {maxSpeedCarNotRestricted, maxSpeedInversionNotRestricted, maxSpeedCar'Orig}}
+            rules: {del : {maxSpeedCarNotRestricted, maxSpeedInversionNotRestricted, maxSpeedCar'Orig}},
+	    config: {loglevel: 0}
            }
        }
 #forall iv: Vehicle. forall id: Day. forall ir: Road. exists sp: Integer. maxSpeed iv id ir sp

diff --git a/src/Exec.hs b/src/Exec.hs
@@ -5,7 +5,9 @@ module Exec where
 import Data.List
 import Syntax
 import Typing
-import SyntaxManipulation (mkFunTp, abstractF, abstractFvd)
+import SyntaxManipulation (mkFunTp, abstractF, abstractFvd, liftExpr, dropVar)
+import PrintProg (renameAndPrintExpr, printExpr)
+import Data.Maybe (fromMaybe)
 
 liftUarithOp :: UArithOp -> Val -> Val
 liftUarithOp u c = case (u, c) of
@@ -78,7 +80,7 @@ data EvalResult t
     deriving (Eq, Ord, Show, Read)
 type ReductEnv t = [EvalResult t]
 
-lookupEnv :: Int -> ReductEnv t -> Maybe (EvalResult t)
+lookupEnv :: Int -> [t] -> Maybe t
 lookupEnv i env = if i < length env then Just (env!!i) else Nothing
 
 -- Evaluates an expression like a functional language. 
@@ -102,33 +104,40 @@ evalExpr env x = case x of
       ExprResult fres -> evalExpr [evalExpr env a] fres
       ClosResult clenv v fbd -> evalExpr (evalExpr env a:clenv) fbd
   FunE t v e -> ClosResult env v e
-  e -> ExprResult (substClos env 0 e)
-
+  e -> ExprResult (substClos (map reduceEvalResult env) 0 e)
+    -- error ((show env) ++ "expr: "  ++ (printExpr e))
+    -- 
 
+reduceEvalResult :: EvalResult (Tp()) -> Expr (Tp())
+reduceEvalResult (ExprResult er) = er
+reduceEvalResult (ClosResult clenv v er) = substClos (map reduceEvalResult clenv) 0 (abstractFvd [v] er)
 
 reduceExpr :: Expr (Tp()) -> Expr (Tp())
+reduceExpr e = reduceEvalResult (evalExpr [] e)
+{-
 reduceExpr e = case evalExpr [] e of
   ExprResult er -> er
-  ClosResult clenv v er -> substClos clenv 0 (abstractFvd [v] er)
+  ClosResult clenv v er -> error "reduce does not produce expr"
+    -- substClos clenv 0 (abstractFvd [v] er)
+-}
 
-substClos :: ReductEnv (Tp()) -> Int ->  Expr (Tp()) -> Expr (Tp())
+-- TODO: check if the indexing is correct in the variable case
+substClos :: [Expr (Tp())] -> Int ->  Expr (Tp()) -> Expr (Tp())
 substClos [] _ e = e
 substClos env d e@ValE{} = e
 substClos env d v@(VarE _ GlobalVar {}) = v
-substClos env d v@(VarE _ (LocalVar _vn i)) =
+substClos env d ve@(VarE t v@(LocalVar _vn i)) =
   if i < d
-  then v
-  else
-    case lookupEnv (i - d) env of
-      Nothing -> v
-      Just (ExprResult e) ->  e
-      Just (ClosResult nenv v ne) -> substClos nenv 0 (abstractFvd [v] ne)
+  then ve
+  else fromMaybe (VarE t (dropVar v)) (lookupEnv (i - d) env)
+      -- Just (ClosResult nenv v ne) -> error "clos in substClos"
+        -- substClos nenv 0 (abstractFvd [v] ne)
 substClos env d (UnaOpE t uop e) = UnaOpE t uop (substClos env d e)
 substClos env d (BinOpE t bop e1 e2) = BinOpE t bop (substClos env d e1) (substClos env d e2)
 substClos env d (IfThenElseE t ec e1 e2) = IfThenElseE t (substClos env d ec) (substClos env d e1) (substClos env d e2)
 substClos env d (AppE t f a) = AppE t (substClos env d f) (substClos env d a)
-substClos env d (FunE t v e) = FunE t v (substClos env (d + 1) e)
-substClos env d (QuantifE t q v e) = QuantifE t q v (substClos env (d + 1) e)
+substClos env d (FunE t v e) = FunE t v (substClos (map (liftExpr d) env) (d + 1) e)
+substClos env d (QuantifE t q v e) = QuantifE t q v (substClos (map (liftExpr d) env) (d + 1) e)
 substClos env d (FldAccE t e fn) = FldAccE t (substClos env d e) fn
 substClos env d (TupleE t es) = TupleE t (map (substClos env d) es)
 substClos env d (CastE t ct e) = CastE t ct (substClos env d e)

diff --git a/src/Smt.hs b/src/Smt.hs
@@ -1,6 +1,6 @@
 -- L4 to SMT interface using the SimpleSMT library
 
-module Smt(proveProgram) where
+module Smt(proveProgram, proveExpr) where
 
 import Annotation (LocTypeAnnot (typeAnnot))
 import KeyValueMap
@@ -36,6 +36,13 @@ declareSort proc srt ar =
   do ackCommand proc $ fun "declare-sort" [ Atom srt, Atom (show ar) ]
      return (SMT.const srt)
 
+-- defineSort is here more restrictive than the SMT define-sort,
+-- and is only used for aliasing sort symbols according to function sortAlias
+defineSort :: Solver -> ClassName -> IO SExpr
+defineSort proc cn =
+  do ackCommand proc $ fun "define-sort" [ Atom (stringOfClassName cn), List [], sortAlias cn ]
+     return (SMT.const (stringOfClassName cn))
+
 getModel  :: Solver -> IO SExpr
 getModel proc =
   command proc $ List [ Atom "get-model" ]
@@ -100,19 +107,50 @@ varDeclsToFunEnv :: Show t => Solver -> SMTSortEnv -> [VarDecl t] -> IO SMTFunEn
 varDeclsToFunEnv s se = mapM (varDeclToFun s se)
 
 
-classDeclsToSortEnv :: Solver -> [ClassDecl t] -> IO SMTSortEnv
-classDeclsToSortEnv s cds = mapM (classDeclToSort s) [cd | cd <- cds,  ClsNm "Class" `elem` superClassesOfClassDecl cd ]
+topLevelUserClassDecl :: ClassDecl t -> Bool
+topLevelUserClassDecl cd = (length (superClassesOfClassDecl cd) >= 2) && superClassesOfClassDecl cd!!1 == ClassC
+
+-- Only the following class declarations are meant to be translated to SMT sorts:
+-- - Some special system defined classes (not subclasses of Class)
+-- - Top-level user defined classes (direct subclasses of Class)
+declarableSort :: ClassDecl t -> Bool
+declarableSort cd =
+  topLevelUserClassDecl cd ||
+  nameOfClassDecl cd == StateC
 
-classDeclToSort :: Solver -> ClassDecl t -> IO (ClassName, SExpr)
-classDeclToSort s (ClassDecl _ cn _) =
+-- For each definable sort, a sort alias has to be introduced in sortAlias
+definableSort :: ClassDecl t -> Bool
+definableSort cd =
+  nameOfClassDecl cd == TimeC
+
+sortAlias :: ClassName -> SExpr
+sortAlias TimeC = Atom "Real"
+sortAlias cn = error ("sort alias for " ++ show cn ++ " (internal error)")
+
+classDeclToSortDecl :: Solver -> ClassDecl t -> IO (ClassName, SExpr)
+classDeclToSortDecl s (ClassDecl _ cn _) =
   do
     se <- declareSort s (stringOfClassName cn) 0
     return (cn, se)
 
+classDeclToSortDefn :: Solver -> ClassDecl t -> IO (ClassName, SExpr)
+classDeclToSortDefn s (ClassDecl _ cn _) =
+  do
+    se <- defineSort s cn
+    return (cn, se)
+
+
+classDeclsToSortEnv :: Solver -> [ClassDecl t] -> IO SMTSortEnv
+classDeclsToSortEnv s cds = do
+  sdecls <- mapM (classDeclToSortDecl s) (filter declarableSort cds)
+  sdefns <- mapM (classDeclToSortDefn s) (filter definableSort cds)
+  return (sdecls ++ sdefns)
+
 
 valToSExpr :: Val -> SExpr
 valToSExpr (BoolV b) = bool b
 valToSExpr (IntV i) = int i
+valToSExpr (FloatV f) = real (toRational f)
 valToSExpr _ = error "valToSExpr: not implemented"
 
 -- TODO: For this to work, names (also of bound variables) have to be unique
@@ -181,12 +219,15 @@ exprToSExpr _    e = error ("exprToSExpr: term " ++ show e ++ " not translatable
 -- Launching the solver and retrieving results
 -------------------------------------------------------------
 
+-- When no explicit log level is provided, the default is set to 1
+-- (silent mode not showing interaction with SMT solver)
 selectLogLevel :: Maybe ValueKVM -> Int
 selectLogLevel config =
-  case selectAssocOfValue "loglevel" (fromMaybe (IntVM 0) config) of
-    Nothing -> 0
+  let defaultLogLevel = 1
+  in case selectAssocOfValue "loglevel" (fromMaybe (IntVM 0) config) of
+    Nothing -> defaultLogLevel
     Just (IntVM n) -> fromIntegral n
-    Just _ -> 0
+    Just _ -> defaultLogLevel
 
 createSolver :: Maybe ValueKVM -> Maybe Logger -> IO Solver
 createSolver config lg =

diff --git a/src/Syntax.hs b/src/Syntax.hs
@@ -3,6 +3,7 @@
 -- {-# OPTIONS_GHC -Wpartial-fields #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PatternSynonyms #-}
 
 module Syntax where
 
@@ -107,12 +108,12 @@ updateAnnotOfTLE f e = case e of
      RuleTLE ru -> RuleTLE $ ru { annotOfRule = f (annotOfRule ru) }
      AssertionTLE as -> AssertionTLE $ as { annotOfAssertion = f (annotOfAssertion as) }
      AutomatonTLE ta -> AutomatonTLE $ ta { annotOfTA = f (annotOfTA ta) }
-     
+
 instance HasLoc t => HasLoc (TopLevelElement t) where
   getLoc = getLoc . getAnnotOfTLE
 
 instance HasAnnot TopLevelElement where
-  getAnnot = getAnnotOfTLE 
+  getAnnot = getAnnotOfTLE
   updateAnnot = updateAnnotOfTLE
 
 data NewProgram t = NewProgram { annotOfNewProgram :: t
@@ -174,12 +175,12 @@ mapClassDecl f e = case e of
 mapRule :: (Rule t -> Rule t) -> TopLevelElement t -> TopLevelElement t
 mapRule f e = case e of
   RuleTLE r -> RuleTLE (f r)
-  x -> x  
+  x -> x
 
 mapAssertion :: (Assertion t -> Assertion t) -> TopLevelElement t -> TopLevelElement t
 mapAssertion f e = case e of
   AssertionTLE r -> AssertionTLE (f r)
-  x -> x  
+  x -> x
 
 newProgramToProgram :: NewProgram t -> Program t
 newProgramToProgram np = Program {
@@ -204,7 +205,7 @@ data Tp t
   = ClassT {annotOfTp :: t, classNameOfTp :: ClassName}
   | FunT {annotOfTp :: t, funTp :: Tp t, argTp :: Tp t}
   | TupleT {annotOfTp :: t, componentsOfTpTupleT :: [Tp t]}
-  | ErrT 
+  | ErrT
   | OkT        -- fake type appearing in constructs (classes, rules etc.) that do not have a genuine type
   | KindT
   deriving (Eq, Ord, Show, Read, Functor, Data, Typeable)
@@ -215,19 +216,39 @@ instance HasLoc t => HasLoc (Tp t) where
 instance HasDefault (Tp t) where
   defaultVal = OkT
 
+
+pattern BooleanC :: ClassName
+pattern BooleanC = ClsNm "Boolean"
+pattern ClassC :: ClassName
+pattern ClassC = ClsNm "Class"
+pattern FloatC :: ClassName
+pattern FloatC = ClsNm "Float"
+pattern IntegerC :: ClassName
+pattern IntegerC = ClsNm "Integer"
+pattern NumberC :: ClassName
+pattern NumberC = ClsNm "Number"
+pattern StateC :: ClassName
+pattern StateC = ClsNm "State"
+pattern StringC :: ClassName
+pattern StringC = ClsNm "String"
+pattern TimeC :: ClassName
+pattern TimeC = ClsNm "Time"
+
 booleanT :: Tp ()
-booleanT = ClassT () (ClsNm "Boolean")
-integerT :: Tp ()
-integerT = ClassT () (ClsNm "Integer")
+booleanT = ClassT () BooleanC
 floatT :: Tp ()
-floatT = ClassT () (ClsNm "Float")
+floatT = ClassT () FloatC
+integerT :: Tp ()
+integerT = ClassT () IntegerC
+stateT :: Tp ()
+stateT = ClassT () StateC
 stringT :: Tp ()
-stringT = ClassT () (ClsNm "String")
--- already contained in Prelude as subtype of Float
+stringT = ClassT () StringC
 timeT :: Tp ()
-timeT = ClassT () (ClsNm "Time")
+timeT = ClassT () TimeC
 numberT :: Tp ()
-numberT = ClassT () (ClsNm "Number")
+numberT = ClassT () NumberC
+
 
 data VarDecl t = VarDecl {annotOfVarDecl :: t, nameOfVarDecl :: VarName, tpOfVarDecl :: Tp t}
   deriving (Eq, Ord, Show, Read, Functor, Data, Typeable)

diff --git a/src/SyntaxManipulation.hs b/src/SyntaxManipulation.hs
@@ -138,6 +138,10 @@ fv (TupleE _ es) = Set.unions (map fv es)
 fv (CastE _ _ e) = fv e
 fv (ListE _ _ es) = Set.unions (map fv es)
 
+dropVar :: Var t -> Var t
+dropVar (LocalVar vn i) = LocalVar vn (i - 1)
+dropVar v = v
+
 -- Lift variables and expressions: 
 -- Increase by one all indices of bound variables with index number >= n
 -- Used for pushing an expression below a quantifier