Merge pull request #330 from GaloisInc/fix/issue324

Fixes #54. Fixes #324.  Note, however that #325 still applies. However, a bugfix is already applied in HEAD Z3 and the similar CVC4 error has been worked around by changing tuple representations.

what4/src/What4/Protocol/Online.hs

@@ -11,6 +11,7 @@ solvers that support online interaction modes.
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 module What4.Protocol.Online
   ( OnlineSolver(..)
   , SolverProcess(..)
@@ -155,6 +156,7 @@ reset :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
 reset p =
   do let c = solverConn p
      resetEntryStack c
+     resetDeclaredStructs c
      writeIORef (solverEarlyUnsat p) Nothing
      addCommand c (resetCommand c)
 
@@ -183,7 +185,8 @@ pop p =
 
 -- | Perform an action in the scope of a solver assumption frame.
 inNewFrame :: (MonadIO m, MonadMask m, SMTReadWriter solver) => SolverProcess scope solver -> m a -> m a
-inNewFrame p = bracket_ (liftIO $ push p) (liftIO $ pop p)
+inNewFrame p action =
+  bracket_ (liftIO $ push p) (liftIO $ try @SomeException $ pop p) action
 
 checkWithAssumptions ::
   SMTReadWriter solver =>

what4/src/What4/Protocol/SMTLib2.hs

@@ -52,7 +52,6 @@ module What4.Protocol.SMTLib2
     -- * Type
   , SMT2.Sort(..)
   , SMT2.arraySort
-  , structSort
     -- * Term
   , Term(..)
   , arrayConst
@@ -217,14 +216,48 @@ class SMTLib2Tweaks a where
       [] -> error "arrayUpdate given empty list"
       i1:ir -> nestedArrayUpdate a (i1, ir) v
 
--- | A struct with the given fields.
---
--- This uses SMTLIB2 datatypes and are not primitive to the language.
-structSort :: [SMT2.Sort] -> SMT2.Sort
-structSort flds = SMT2.Sort $ "(Struct" <> Builder.decimal n <> foldMap f flds <> ")"
-  where f :: SMT2.Sort -> Builder
-        f (SMT2.Sort s) = " " <> s
-        n = length flds
+  -- | The sort of structs with the given field types.
+  --
+  -- By default, this uses SMTLIB2 datatypes and are not primitive to the language.
+  smtlib2StructSort :: [SMT2.Sort] -> SMT2.Sort
+  smtlib2StructSort [] = SMT2.Sort "Struct0"
+  smtlib2StructSort flds = SMT2.Sort $ "(Struct" <> Builder.decimal n <> foldMap f flds <> ")"
+       where f :: SMT2.Sort -> Builder
+             f (SMT2.Sort s) = " " <> s
+             n = length flds
+
+  -- | Construct a struct value from the given field values
+  smtlib2StructCtor :: [Term] -> Term
+  smtlib2StructCtor args = term_app nm args
+    where nm = "mk-struct" <> Builder.decimal (length args)
+
+  -- | Construct a struct field projection term
+  smtlib2StructProj ::
+    Int {- ^ number of fields in the struct -} ->
+    Int {- ^ 0-based index of the struct field -} ->
+    Term {- ^ struct term to project from -} ->
+    Term
+  smtlib2StructProj n i a = term_app nm [a]
+    where nm = "struct" <> Builder.decimal n <> "-proj" <> Builder.decimal i
+
+  -- By default, this uses the SMTLib 2.6 standard version of the declare-datatype command.
+  smtlib2declareStructCmd :: Int -> Maybe SMT2.Command
+  smtlib2declareStructCmd 0 = Just $
+    SMT2.Cmd $ app "declare-datatype" [ fromString "Struct0", builder_list [ builder_list ["mk-struct0"]]]
+  smtlib2declareStructCmd n = Just $
+    let n_str = fromString (show n)
+        tp = "Struct" <> n_str
+        cnstr = "mk-struct" <> n_str
+        idxes = map (fromString . show) [0 .. n-1]
+        tp_names = [ "T" <> i_str
+                   | i_str <- idxes
+                   ]
+        flds = [ app ("struct" <> n_str <> "-proj" <> i_str) [ "T" <> i_str ]
+               | i_str <- idxes
+               ]
+     in SMT2.Cmd $ app "declare-datatype" [ tp, app "par" [ builder_list tp_names, builder_list [app cnstr flds]]]
+
+
 
 asSMT2Type :: forall a tp . SMTLib2Tweaks a => TypeMap tp -> SMT2.Sort
 asSMT2Type BoolTypeMap    = SMT2.boolSort
@@ -234,15 +267,15 @@ asSMT2Type RealTypeMap    = SMT2.realSort
 asSMT2Type (BVTypeMap w)  = SMT2.bvSort (natValue w)
 asSMT2Type (FloatTypeMap fpp) = SMT2.Sort $ mkFloatSymbol "FloatingPoint" (asSMTFloatPrecision fpp)
 asSMT2Type ComplexToStructTypeMap =
-  structSort [ SMT2.realSort, SMT2.realSort ]
+  smtlib2StructSort @a [ SMT2.realSort, SMT2.realSort ]
 asSMT2Type ComplexToArrayTypeMap =
   smtlib2arrayType @a [SMT2.boolSort] SMT2.realSort
 asSMT2Type (PrimArrayTypeMap i r) =
   smtlib2arrayType @a (toListFC (asSMT2Type @a) i) (asSMT2Type @a r)
 asSMT2Type (FnArrayTypeMap _ _) =
   error "SMTLIB backend does not support function types as first class."
 asSMT2Type (StructTypeMap f) =
-  structSort (toListFC (asSMT2Type @a) f)
+  smtlib2StructSort @a (toListFC (asSMT2Type @a) f)
 
 -- Default instance.
 instance SMTLib2Tweaks () where
@@ -418,12 +451,6 @@ instance SupportTermOps Term where
   realExp = un_app "exp"
   realLog = un_app "log"
 
-  structCtor args = term_app nm args
-    where nm = "mk-struct" <> Builder.decimal (length args)
-
-  structFieldSelect n a i = term_app nm [a]
-    where nm = "struct" <> Builder.decimal n <> "-proj" <> Builder.decimal i
-
   smtFnApp nm args = term_app (SMT2.renderTerm nm) args
 
   fromText t = SMT2.T (Builder.fromText t)
@@ -496,25 +523,27 @@ instance SMTLib2Tweaks a => SMTWriter (Writer a) where
     let resolveArg (var, Some tp) = (var, asSMT2Type @a tp)
      in SMT2.defineFun f (resolveArg <$> args) (asSMT2Type @a return_type) e
 
-  declareStructDatatype conn n = do
+  resetDeclaredStructs conn = do
+    let r = declaredTuples (connState conn)
+    writeIORef r mempty
+
+  declareStructDatatype conn flds = do
+    let n = Ctx.sizeInt (Ctx.size flds)
     let r = declaredTuples (connState conn)
     s <- readIORef r
     when (Set.notMember n s) $ do
-      let type_name i = fromString ('T' : show i)
-      let params = builder_list $ type_name  <$> [1..n]
-      let n_str = fromString (show n)
-      let tp = "Struct" <> n_str
-      let ctor = "mk-struct" <> n_str
-      let field_def i = app field_nm [type_name i]
-            where field_nm = "struct" <> n_str <> "-proj" <> fromString (show (i-1))
-      let fields = field_def <$> [1..n]
-      let decl = app tp [app ctor fields]
-      let decls = "(" <> decl <> ")"
-      let cmd = SMT2.Cmd $ app "declare-datatypes" [ params, decls ]
-      addCommand conn cmd
-
+      case smtlib2declareStructCmd @a n of
+        Nothing -> return ()
+        Just cmd -> addCommand conn cmd
       writeIORef r $! Set.insert n s
 
+  structCtor _conn _tps vals = smtlib2StructCtor @a vals
+
+  structProj _conn tps idx v =
+    let n = Ctx.sizeInt (Ctx.size tps)
+        i = Ctx.indexVal idx
+     in smtlib2StructProj @a n i v
+
   writeCommand conn (SMT2.Cmd cmd) =
     do let cmdout = Lazy.toStrict (Builder.toLazyText cmd)
        Streams.write (Just (cmdout <> "\n")) (connHandle conn)

what4/src/What4/Protocol/SMTLib2/Syntax.hs

@@ -62,6 +62,7 @@ module What4.Protocol.SMTLib2.Syntax
   , term_app
   , pairwise_app
   , namedTerm
+  , builder_list
     -- * Core theory
   , true
   , false