From 6ee9bcb062d1d3ab77c4796326aecc312e9f9028 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Mon, 8 Apr 2019 14:49:44 -0700
Subject: [PATCH 1/8] Fix the syntax of the parameterized SMTLib2 functions
 `fp.to_sbv` and `fp.to_ubv`.

---
 what4/src/What4/Protocol/SMTLib2.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/what4/src/What4/Protocol/SMTLib2.hs b/what4/src/What4/Protocol/SMTLib2.hs
index 0c3db7fdd..83c1cee38 100644
--- a/what4/src/What4/Protocol/SMTLib2.hs
+++ b/what4/src/What4/Protocol/SMTLib2.hs
@@ -388,9 +388,9 @@ instance SupportTermOps Term where
   realToFloat fpp r = un_app $ mkRoundingOp (mkFloatSymbol "to_fp" (asSMTFloatPrecision fpp)) r
 
   floatToBV w r =
-    un_app $ mkRoundingOp ("(fp.to_ubv " <> fromString (show w) <> ")") r
+    un_app $ mkRoundingOp ("(_ fp.to_ubv " <> fromString (show w) <> ")") r
   floatToSBV w r =
-    un_app $ mkRoundingOp ("(fp.to_sbv " <> fromString (show w) <> ")") r
+    un_app $ mkRoundingOp ("(_ fp.to_sbv " <> fromString (show w) <> ")") r
 
   floatToReal = un_app "fp.to_real"
 

From 51df64f667b3d99df8be78032556ab17907da771 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Tue, 9 Apr 2019 15:13:06 -0700
Subject: [PATCH 2/8] Add a new crucible statement for constructing fresh
 floating point values. These cannot use the ordinary `fresh` construct
 because the base type underlying the interpreted floating point values is not
 known at CFG construction time, as it depends on the symbolic backend.

---
 crucible/src/Lang/Crucible/CFG/Core.hs           | 10 ++++++++++
 crucible/src/Lang/Crucible/CFG/Reg.hs            |  6 ++++++
 crucible/src/Lang/Crucible/CFG/SSAConversion.hs  |  8 ++++++++
 crucible/src/Lang/Crucible/Simulator/EvalStmt.hs |  6 ++++++
 crucible/src/Lang/Crucible/Utils/CoreRewrite.hs  |  1 +
 5 files changed, 31 insertions(+)

diff --git a/crucible/src/Lang/Crucible/CFG/Core.hs b/crucible/src/Lang/Crucible/CFG/Core.hs
index 3374bc108..389716593 100644
--- a/crucible/src/Lang/Crucible/CFG/Core.hs
+++ b/crucible/src/Lang/Crucible/CFG/Core.hs
@@ -311,6 +311,11 @@ data Stmt ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) where
                 -> !(Maybe SolverSymbol)
                 -> Stmt ext ctx (ctx ::> BaseToType bt)
 
+  -- Create a fresh floating-point constant
+  FreshFloat :: !(FloatInfoRepr fi)
+             -> !(Maybe SolverSymbol)
+             -> Stmt ext ctx (ctx ::> FloatType fi)
+
   -- Allocate a new reference cell
   NewRefCell :: !(TypeRepr tp)
              -> !(Reg ctx tp)
@@ -467,6 +472,9 @@ applyEmbeddingStmt ctxe stmt =
     FreshConstant bt nm -> Pair (FreshConstant bt nm)
                                 (Ctx.extendEmbeddingBoth ctxe)
 
+    FreshFloat fi nm -> Pair (FreshFloat fi nm)
+                             (Ctx.extendEmbeddingBoth ctxe)
+
     NewRefCell tp r -> Pair (NewRefCell tp (reg r))
                             (Ctx.extendEmbeddingBoth ctxe)
     NewEmptyRefCell tp -> Pair (NewEmptyRefCell tp)
@@ -569,6 +577,7 @@ nextStmtHeight h s =
     ReadGlobal{} -> incSize h
     WriteGlobal{} -> h
     FreshConstant{} -> Ctx.incSize h
+    FreshFloat{} -> Ctx.incSize h
     NewRefCell{} -> Ctx.incSize h
     NewEmptyRefCell{} ->Ctx.incSize h
     ReadRefCell{} -> Ctx.incSize h
@@ -590,6 +599,7 @@ ppStmt r s =
     ReadGlobal v -> text "read" <+> ppReg r <+> pretty v
     WriteGlobal v e -> text "write" <+> pretty v <+> pretty e
     FreshConstant bt nm -> ppReg r <+> text "=" <+> text "fresh" <+> pretty bt <+> maybe mempty (text . show) nm
+    FreshFloat fi nm -> ppReg r <+> text "=" <+> text "fresh-float" <+> pretty fi <+> maybe mempty (text . show) nm
     NewRefCell _ e -> ppReg r <+> text "=" <+> ppFn "newref" [ pretty e ]
     NewEmptyRefCell tp -> ppReg r <+> text "=" <+> ppFn "emptyref" [ pretty tp ]
     ReadRefCell e -> ppReg r <+> text "= !" <> pretty e
diff --git a/crucible/src/Lang/Crucible/CFG/Reg.hs b/crucible/src/Lang/Crucible/CFG/Reg.hs
index 17d96b4ba..cdb5ac208 100644
--- a/crucible/src/Lang/Crucible/CFG/Reg.hs
+++ b/crucible/src/Lang/Crucible/CFG/Reg.hs
@@ -451,6 +451,8 @@ data AtomValue ext s (tp :: CrucibleType) where
   NewEmptyRef :: !(TypeRepr tp) -> AtomValue ext s (ReferenceType tp)
   -- Create a fresh uninterpreted constant of base type
   FreshConstant :: !(BaseTypeRepr bt) -> !(Maybe SolverSymbol) -> AtomValue ext s (BaseToType bt)
+  -- Create a fresh uninterpreted constant of floating point type
+  FreshFloat :: !(FloatInfoRepr fi) -> !(Maybe SolverSymbol) -> AtomValue ext s (FloatType fi)
 
   Call :: !(Atom s (FunctionHandleType args ret))
        -> !(Assignment (Atom s) args)
@@ -468,6 +470,7 @@ instance PrettyExt ext => Pretty (AtomValue ext s tp) where
       NewRef a -> text "newref" <+> pretty a
       NewEmptyRef tp -> text "emptyref" <+> pretty tp
       FreshConstant bt nm -> text "fresh" <+> pretty bt <+> maybe mempty (text . show) nm
+      FreshFloat fi nm -> text "fresh" <+> pretty fi <+> maybe mempty (text . show) nm
       Call f args _ -> pretty f <> parens (commas (toListFC pretty args))
 
 typeOfAtomValue :: (TypeApp (StmtExtension ext) , TypeApp (ExprExtension ext))
@@ -483,6 +486,7 @@ typeOfAtomValue v =
     NewRef a -> ReferenceRepr (typeOfAtom a)
     NewEmptyRef tp -> ReferenceRepr tp
     FreshConstant bt _ -> baseToType bt
+    FreshFloat fi _ -> FloatRepr fi
     Call _ _ r -> r
 
 -- | Fold over all values in an 'AtomValue'.
@@ -497,6 +501,7 @@ foldAtomValueInputs _ (NewEmptyRef _)     b = b
 foldAtomValueInputs f (NewRef a)          b = f (AtomValue a) b
 foldAtomValueInputs f (EvalApp app0)      b = foldApp (f . AtomValue) b app0
 foldAtomValueInputs _ (FreshConstant _ _) b = b
+foldAtomValueInputs _ (FreshFloat _ _)    b = b
 foldAtomValueInputs f (Call g a _)        b = f (AtomValue g) (foldrFC' (f . AtomValue) b a)
 
 substAtomValue :: ( Applicative m, TraverseExt ext )
@@ -511,6 +516,7 @@ substAtomValue _ (NewEmptyRef tp) = pure $ NewEmptyRef tp
 substAtomValue f (NewRef a) = NewRef <$> substAtom f a
 substAtomValue f (EvalApp ap) = EvalApp <$> traverseFC (substAtom f) ap
 substAtomValue _ (FreshConstant tp sym) = pure $ FreshConstant tp sym
+substAtomValue _ (FreshFloat fi sym)    = pure $ FreshFloat fi sym
 substAtomValue f (Call g as ret) = Call <$> substAtom f g
                                         <*> traverseFC (substAtom f) as
                                         <*> pure ret
diff --git a/crucible/src/Lang/Crucible/CFG/SSAConversion.hs b/crucible/src/Lang/Crucible/CFG/SSAConversion.hs
index 17ebeffdb..ce650f0cd 100644
--- a/crucible/src/Lang/Crucible/CFG/SSAConversion.hs
+++ b/crucible/src/Lang/Crucible/CFG/SSAConversion.hs
@@ -798,6 +798,14 @@ resolveStmts nm bi sz reg_map bindings appMap (Posd p s0:rest) t = do
           let stmt = C.FreshConstant bt cnm
           C.ConsStmt pl stmt (resolveStmts nm bi sz' reg_map' bindings' appMap' rest t)
 
+        FreshFloat fi cnm -> do
+          let sz' = incSize sz
+          let reg_map'  = reg_map  & assignRegister (AtomValue a) sz
+          let bindings' = bindings & extendRegExprs NothingF
+          let appMap'   = appMap   & appRegMap_extend
+          let stmt = C.FreshFloat fi cnm
+          C.ConsStmt pl stmt (resolveStmts nm bi sz' reg_map' bindings' appMap' rest t)
+
         Call h args _ -> do
           let return_type = typeOfAtom a
           let h' = resolveAtom reg_map h
diff --git a/crucible/src/Lang/Crucible/Simulator/EvalStmt.hs b/crucible/src/Lang/Crucible/Simulator/EvalStmt.hs
index ea1006f13..c0333e380 100644
--- a/crucible/src/Lang/Crucible/Simulator/EvalStmt.hs
+++ b/crucible/src/Lang/Crucible/Simulator/EvalStmt.hs
@@ -61,6 +61,7 @@ import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
 import           What4.Config
 import           What4.Interface
+import           What4.InterpretedFloatingPoint (freshFloatConstant)
 import           What4.Partial
 import           What4.ProgramLoc
 import           What4.Symbol (emptySymbol)
@@ -274,6 +275,11 @@ stepStmt verb stmt rest =
             v <- liftIO $ freshConstant sym nm bt
             continueWith $ stateCrucibleFrame %~ extendFrame (baseToType bt) v rest
 
+       FreshFloat fi mnm ->
+         do let nm = fromMaybe emptySymbol mnm
+            v <- liftIO $ freshFloatConstant sym nm fi
+            continueWith $ stateCrucibleFrame %~ extendFrame (FloatRepr fi) v rest
+
        SetReg tp e ->
          do v <- evalExpr verb e
             continueWith $ stateCrucibleFrame %~ extendFrame tp v rest
diff --git a/crucible/src/Lang/Crucible/Utils/CoreRewrite.hs b/crucible/src/Lang/Crucible/Utils/CoreRewrite.hs
index 98c786273..61b60b38e 100644
--- a/crucible/src/Lang/Crucible/Utils/CoreRewrite.hs
+++ b/crucible/src/Lang/Crucible/Utils/CoreRewrite.hs
@@ -103,6 +103,7 @@ stmtDiff stmt =
     ReadGlobal {}    -> Ctx.knownDiff
     WriteGlobal {}   -> Ctx.knownDiff
     FreshConstant{}  -> Ctx.knownDiff
+    FreshFloat{}     -> Ctx.knownDiff
     NewRefCell {}    -> Ctx.knownDiff
     NewEmptyRefCell{}-> Ctx.knownDiff
     ReadRefCell {}   -> Ctx.knownDiff

From 82d3a750a4c43dbb81f91f7054157655bc6ad81f Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Tue, 9 Apr 2019 15:18:01 -0700
Subject: [PATCH 3/8] Add `crucible-syntax` support for floating-point types
 and some of the conversions to and from floating point types.

---
 .../src/Lang/Crucible/Syntax/Atoms.hs         | 148 +++++++++-----
 .../src/Lang/Crucible/Syntax/Concrete.hs      | 152 +++++++++++++--
 .../test-data/parser-tests/floats.cbl         |  74 +++++++
 .../test-data/parser-tests/floats.out.good    | 182 ++++++++++++++++++
 4 files changed, 487 insertions(+), 69 deletions(-)
 create mode 100644 crucible-syntax/test-data/parser-tests/floats.cbl
 create mode 100644 crucible-syntax/test-data/parser-tests/floats.out.good

diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs
index 003348217..d0a280759 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs
@@ -46,16 +46,15 @@ data Keyword = Defun | DefBlock | DefGlobal
              | Start
              | SetGlobal
              | SetRef | DropRef_
-             | Unpack
              | Plus | Minus | Times | Div | Negate | Abs
              | Just_ | Nothing_ | FromJust
              | Inj | Proj
              | AnyT | UnitT | BoolT | NatT | IntegerT | RealT | ComplexRealT | CharT | StringT
-             | BitvectorT | VectorT | FunT | MaybeT | VariantT | RefT
+             | BitvectorT | VectorT | FPT | FunT | MaybeT | VariantT | RefT
+             | Half_ | Float_ | Double_ | Quad_ | X86_80_ | DoubleDouble_
              | The
              | Equalp | Integerp
              | If
-             | Pack
              | Not_ | And_ | Or_ | Xor_
              | Mod
              | Lt | Le
@@ -76,20 +75,85 @@ data Keyword = Defun | DefBlock | DefGlobal
              | BVCarry_ | BVSCarry_ | BVSBorrow_
              | BVNot_ | BVAnd_ | BVOr_ | BVXor_ | BVShl_ | BVLshr_ | BVAshr_
              | Sle | Slt | Sdiv | Smod | ZeroExt | SignExt
+             | RNE_ | RNA_ | RTP_ | RTN_ | RTZ_
+             | FPToUBV_ | FPToSBV_ | UBVToFP_ | SBVToFP_ | BinaryToFP_ | FPToBinary_
+             | FPToReal_ | RealToFP_
   deriving (Eq, Ord)
 
 keywords :: [(Text, Keyword)]
 keywords =
+    -- function/block defintion
   [ ("defun" , Defun)
+  , ("start" , Start)
   , ("defblock", DefBlock)
   , ("defglobal", DefGlobal)
   , ("registers", Registers)
+
+    -- statements
   , ("let", Let)
   , ("set-global!", SetGlobal)
   , ("set-ref!", SetRef)
   , ("drop-ref!", DropRef_)
-  , ("start" , Start)
-  , ("unpack" , Unpack)
+  , ("fresh", Fresh)
+  , ("jump" , Jump_)
+  , ("case", Case)
+  , ("return" , Return_)
+  , ("branch" , Branch_)
+  , ("maybe-branch" , MaybeBranch_)
+  , ("tail-call" , TailCall_)
+  , ("error", Error_)
+  , ("output", Output_)
+  , ("print" , Print_)
+  , ("Ref", RefT)
+  , ("deref", Deref)
+  , ("ref", Ref)
+  , ("empty-ref", EmptyRef)
+  , ("set-register!", SetRegister)
+  , ("assert!", Assert_)
+  , ("assume!", Assume_)
+  , ("funcall", Funcall)
+
+    -- types
+  , ("Any" , AnyT)
+  , ("Unit" , UnitT)
+  , ("Bool" , BoolT)
+  , ("Nat" , NatT)
+  , ("Integer" , IntegerT)
+  , ("FP", FPT)
+  , ("Real" , RealT)
+  , ("ComplexReal" , ComplexRealT)
+  , ("Char" , CharT)
+  , ("String" , StringT)
+  , ("Bitvector" , BitvectorT)
+  , ("Vector", VectorT)
+  , ("->", FunT)
+  , ("Maybe", MaybeT)
+  , ("Variant", VariantT)
+
+    -- floating-point variants
+  , ("Half", Half_)
+  , ("Float", Float_)
+  , ("Double", Double_)
+  , ("Quad", Quad_)
+  , ("X86_80", X86_80_)
+  , ("DoubleDouble", DoubleDouble_)
+
+    -- misc
+  , ("the" , The)
+  , ("equal?" , Equalp)
+  , ("if" , If)
+
+    -- ANY types
+  , ("to-any", ToAny)
+  , ("from-any", FromAny)
+
+    -- booleans
+  , ("not" , Not_)
+  , ("and" , And_)
+  , ("or" , Or_)
+  , ("xor" , Xor_)
+
+    -- arithmetic
   , ("+" , Plus)
   , ("-" , Minus)
   , ("*" , Times)
@@ -102,31 +166,19 @@ keywords =
   , ("smod", Smod)
   , ("negate", Negate)
   , ("abs", Abs)
-  , ("show", Show)
+  , ("mod" , Mod)
+  , ("integer?" , Integerp)
+
+    -- Variants
   , ("inj", Inj)
   , ("proj", Proj)
+
+    -- Maybe
   , ("just" , Just_)
   , ("nothing" , Nothing_)
   , ("from-just" , FromJust)
-  , ("to-any", ToAny)
-  , ("from-any", FromAny)
-  , ("the" , The)
-  , ("equal?" , Equalp)
-  , ("integer?" , Integerp)
-  , ("Any" , AnyT)
-  , ("Unit" , UnitT)
-  , ("Bool" , BoolT)
-  , ("Nat" , NatT)
-  , ("Integer" , IntegerT)
-  , ("Real" , RealT)
-  , ("ComplexReal" , ComplexRealT)
-  , ("Char" , CharT)
-  , ("String" , StringT)
-  , ("Bitvector" , BitvectorT)
-  , ("Vector", VectorT)
-  , ("->", FunT)
-  , ("Maybe", MaybeT)
-  , ("Variant", VariantT)
+
+    -- Vectors
   , ("vector", VectorLit_)
   , ("vector-replicate", VectorReplicate_)
   , ("vector-empty?", VectorIsEmpty_)
@@ -134,32 +186,12 @@ keywords =
   , ("vector-get", VectorGetEntry_)
   , ("vector-set", VectorSetEntry_)
   , ("vector-cons", VectorCons_)
-  , ("if" , If)
-  , ("pack" , Pack)
-  , ("not" , Not_)
-  , ("and" , And_)
-  , ("or" , Or_)
-  , ("xor" , Xor_)
-  , ("mod" , Mod)
-  , ("fresh", Fresh)
-  , ("jump" , Jump_)
-  , ("case", Case)
-  , ("return" , Return_)
-  , ("branch" , Branch_)
-  , ("maybe-branch" , MaybeBranch_)
-  , ("tail-call" , TailCall_)
-  , ("error", Error_)
-  , ("output", Output_)
-  , ("print" , Print_)
+
+    -- strings
+  , ("show", Show)
   , ("string-append", StringAppend)
-  , ("Ref", RefT)
-  , ("deref", Deref)
-  , ("ref", Ref)
-  , ("empty-ref", EmptyRef)
-  , ("set-register!", SetRegister)
-  , ("assert!", Assert_)
-  , ("assume!", Assume_)
-  , ("funcall", Funcall)
+
+    -- bitvector
   , ("bv", BV)
   , ("bv-concat", BVConcat_)
   , ("bv-select", BVSelect_)
@@ -178,8 +210,22 @@ keywords =
   , ("shl", BVShl_)
   , ("lshr", BVLshr_)
   , ("ashr", BVAshr_)
-  ]
 
+    -- floating-point
+  , ("fp-to-ubv", FPToUBV_)
+  , ("fp-to-sbv", FPToSBV_)
+  , ("ubv-to-fp", UBVToFP_)
+  , ("sbv-to-fp", SBVToFP_)
+  , ("fp-to-binary", FPToBinary_)
+  , ("binary-to-fp", BinaryToFP_)
+  , ("real-to-fp", RealToFP_)
+  , ("fp-to-real", FPToReal_)
+  , ("rne" , RNE_)
+  , ("rna" , RNA_)
+  , ("rtp" , RTP_)
+  , ("rtn" , RTN_)
+  , ("rtz" , RTZ_)
+  ]
 
 instance Show Keyword where
   show k = case [str | (str, k') <- keywords, k == k'] of
diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
index 1bf539126..2828421a0 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
@@ -193,6 +193,23 @@ atomName = sideCondition "Crucible atom literal" isCAtom atomic
   where isCAtom (At a) = Just a
         isCAtom _ = Nothing
 
+roundingMode :: MonadSyntax Atomic m => m RoundingMode
+roundingMode = describe "rounding mode" $
+        asum [ kw RNE_ $> RNE
+             , kw RNA_ $> RNA
+             , kw RTP_ $> RTP
+             , kw RTN_ $> RTN
+             , kw RTZ_ $> RTZ
+             ]
+
+fpinfo :: MonadSyntax Atomic m => m (Some FloatInfoRepr)
+fpinfo = asum [ kw Half_         $> Some HalfFloatRepr
+              , kw Float_        $> Some SingleFloatRepr
+              , kw Double_       $> Some DoubleFloatRepr
+              , kw Quad_         $> Some QuadFloatRepr
+              , kw X86_80_       $> Some X86_80FloatRepr
+              , kw DoubleDouble_ $> Some DoubleDoubleFloatRepr
+              ]
 
 bool :: MonadSyntax Atomic m => m  Bool
 bool = sideCondition "Boolean literal" isBool atomic
@@ -235,15 +252,25 @@ isBaseType =
        NotBaseType -> empty
        AsBaseType bt -> return (Some bt)
 
-data PosNat =
-  forall w. (1 <= w) => PosNat (NatRepr w)
+isFloatingType :: MonadSyntax Atomic m => m (Some FloatInfoRepr)
+isFloatingType =
+  describe "floating-point type" $
+  do Some tp <- isType
+     case tp of
+       FloatRepr fi -> return (Some fi)
+       _ -> empty
+
+data BoundedNat bnd =
+  forall w. (bnd <= w) => BoundedNat (NatRepr w)
+
+type PosNat = BoundedNat 1
 
 posNat :: MonadSyntax Atomic m => m PosNat
 posNat =
    do i <- sideCondition "positive nat literal" checkPosNat nat
       maybe empty return $ do Some x <- return $ mkNatRepr i
                               LeqProof <- isPosNat x
-                              return $ PosNat x
+                              return $ BoundedNat x
   where checkPosNat i | i > 0 = Just i
         checkPosNat _ = Nothing
 
@@ -253,7 +280,7 @@ natRepr = mkNatRepr <$> nat
 isType :: MonadSyntax Atomic m => m (Some TypeRepr)
 isType =
   describe "type" $ call
-    (atomicType <|> vector <|> ref <|> bv <|> fun <|> maybeT <|> var)
+    (atomicType <|> vector <|> ref <|> bv <|> fp <|> fun <|> maybeT <|> var)
 
   where
     atomicType =
@@ -271,16 +298,18 @@ isType =
     vector = unary VectorT isType <&> \(Some t) -> Some (VectorRepr t)
     ref    = unary RefT isType <&> \(Some t) -> Some (ReferenceRepr t)
     bv :: MonadSyntax Atomic m => m  (Some TypeRepr)
-    bv     = do Some len <- unary BitvectorT (mkNatRepr <$> nat)
-                describe "positive number" $
-                  case testLeq (knownNat :: NatRepr 1) len of
-                    Nothing -> empty
-                    Just LeqProof -> return $ Some $ BVRepr len
+    bv     = do BoundedNat len <- unary BitvectorT posNat
+                return $ Some $ BVRepr len
+
+    fp :: MonadSyntax Atomic m => m (Some TypeRepr)
+    fp = do Some fpi <- unary FPT fpinfo
+            return $ Some $ FloatRepr fpi
 
     fun :: MonadSyntax Atomic m => m (Some TypeRepr)
     fun = cons (kw FunT) (repUntilLast isType) <&> \((), (args, ret)) -> mkFunRepr args ret
 
     maybeT = unary MaybeT isType <&> \(Some t) -> Some (MaybeRepr t)
+
     var :: MonadSyntax Atomic m => m (Some TypeRepr)
     var = cons (kw VariantT) (rep isType) <&> \((), toCtx -> Some tys) -> Some (VariantRepr tys)
 
@@ -401,6 +430,8 @@ synthExpr typeHint =
      just <|> nothing <|> fromJust_ <|> injection <|> projection <|>
      vecLit <|> vecCons <|> vecRep <|> vecLen <|> vecEmptyP <|> vecGet <|> vecSet <|>
      ite <|>  intLit <|> rationalLit <|> intp <|>
+     binaryToFp <|> fpToBinary <|> realToFp <|> fpToReal <|>
+     ubvToFloat <|> floatToUBV <|> sbvToFloat <|> floatToSBV <|>
      unaryBV BVNonzero_ BVNonzero <|> compareBV BVCarry_ BVCarry <|>
      compareBV BVSCarry_ BVSCarry <|> compareBV BVSBorrow_ BVSBorrow <|>
      compareBV Slt BVSlt <|> compareBV Sle BVSle)
@@ -671,6 +702,86 @@ synthExpr typeHint =
            Nothing ->
              describe ("expected unambiguous variant") empty
 
+    fpToBinary :: m (SomeExpr s)
+    fpToBinary =
+       kw FPToBinary_ `followedBy`
+       (depCons synth $ \(Pair tp x) ->
+         case tp of
+           FloatRepr fpi
+             | BaseBVRepr w <- floatInfoToBVTypeRepr fpi
+             , Just LeqProof <- isPosNat w ->
+                 emptyList $> (SomeE (BVRepr w) $ EApp $ FloatToBinary fpi x)
+           _ -> empty)
+
+    binaryToFp :: m (SomeExpr s)
+    binaryToFp =
+       kw BinaryToFP_ `followedBy`
+       (depCons fpinfo $ \(Some fpi) ->
+        depCons (check (baseToType (floatInfoToBVTypeRepr fpi))) $ \x ->
+        emptyList $> (SomeE (FloatRepr fpi) $ EApp $ FloatFromBinary fpi x))
+
+    fpToReal :: m (SomeExpr s)
+    fpToReal =
+       kw FPToReal_ `followedBy`
+       (depCons synth $ \(Pair tp x) ->
+         case tp of
+           FloatRepr _fpi -> emptyList $> (SomeE RealValRepr $ EApp $ FloatToReal x)
+           _ -> empty)
+
+    realToFp :: m (SomeExpr s)
+    realToFp =
+       kw RealToFP_ `followedBy`
+       (depCons fpinfo $ \(Some fpi) ->
+        depCons roundingMode $ \rm ->
+        depCons (check RealValRepr) $ \x ->
+        emptyList $> (SomeE (FloatRepr fpi) $ EApp $ FloatFromReal fpi rm x))
+
+    ubvToFloat :: m (SomeExpr s)
+    ubvToFloat =
+       kw UBVToFP_ `followedBy`
+       (depCons fpinfo $ \(Some fpi) ->
+        depCons roundingMode $ \rm ->
+        depCons synth $ \(Pair tp x) ->
+          case tp of
+            BVRepr _w ->
+              emptyList $> (SomeE (FloatRepr fpi) $ EApp $ FloatFromBV fpi rm x)
+            _ -> empty
+        )
+
+    sbvToFloat :: m (SomeExpr s)
+    sbvToFloat =
+       kw SBVToFP_ `followedBy`
+       (depCons fpinfo $ \(Some fpi) ->
+        depCons roundingMode $ \rm ->
+        depCons synth $ \(Pair tp x) ->
+          case tp of
+            BVRepr _w ->
+              emptyList $> (SomeE (FloatRepr fpi) $ EApp $ FloatFromSBV fpi rm x)
+            _ -> empty
+       )
+
+    floatToUBV :: m (SomeExpr s)
+    floatToUBV =
+       kw FPToUBV_ `followedBy`
+       (depCons posNat $ \(BoundedNat w) ->
+        depCons roundingMode $ \rm ->
+        depCons synth $ \(Pair tp x) ->
+          case tp of
+            FloatRepr _fpi ->
+              emptyList $> (SomeE (BVRepr w) $ EApp $ FloatToBV w rm x)
+            _ -> empty)
+
+    floatToSBV :: m (SomeExpr s)
+    floatToSBV =
+       kw FPToSBV_ `followedBy`
+       (depCons posNat $ \(BoundedNat w) ->
+        depCons roundingMode $ \rm ->
+        depCons synth $ \(Pair tp x) ->
+          case tp of
+            FloatRepr _fpi ->
+              emptyList $> (SomeE (BVRepr w) $ EApp $ FloatToSBV w rm x)
+            _ -> empty)
+
     ite :: m (SomeExpr s)
     ite =
       do (c, (et, (ef, ()))) <-
@@ -811,7 +922,7 @@ synthBV widthHint =
     bvLit :: m (SomeBVExpr s)
     bvLit =
       describe "bitvector literal" $
-      do (PosNat w, i) <- binary BV posNat int
+      do (BoundedNat w, i) <- binary BV posNat int
          return $ SomeBVExpr w $ EApp $ BVLit w i
 
     unaryBV :: Keyword
@@ -858,12 +969,12 @@ synthBV widthHint =
 
     boolToBV :: m (SomeBVExpr s)
     boolToBV =
-      do (PosNat w, x) <- binary BoolToBV_ posNat (check BoolRepr)
+      do (BoundedNat w, x) <- binary BoolToBV_ posNat (check BoolRepr)
          return $ SomeBVExpr w $ EApp $ BoolToBV w x
 
     bvSelect :: m (SomeBVExpr s)
     bvSelect =
-      do (Some idx, (PosNat len, (SomeBVExpr w x, ()))) <-
+      do (Some idx, (BoundedNat len, (SomeBVExpr w x, ()))) <-
              followedBy (kw BVSelect_) (commit *> cons natRepr (cons posNat (cons (bvSubterm NoHint) emptyList)))
          case testLeq (addNat idx len) w of
            Just LeqProof -> return $ SomeBVExpr len $ EApp $ BVSelect idx len w x
@@ -877,21 +988,21 @@ synthBV widthHint =
 
     bvTrunc :: m (SomeBVExpr s)
     bvTrunc =
-      do (PosNat r, SomeBVExpr w x) <- binary BVTrunc_ posNat (bvSubterm NoHint)
+      do (BoundedNat r, SomeBVExpr w x) <- binary BVTrunc_ posNat (bvSubterm NoHint)
          case testLeq (incNat r) w of
            Just LeqProof -> return $ SomeBVExpr r (EApp $ BVTrunc r w x)
            _ -> later $ describe "valid bitvector truncation" $ empty
 
     bvZext :: m (SomeBVExpr s)
     bvZext =
-      do (PosNat r, SomeBVExpr w x) <- binary BVZext_ posNat (bvSubterm NoHint)
+      do (BoundedNat r, SomeBVExpr w x) <- binary BVZext_ posNat (bvSubterm NoHint)
          case testLeq (incNat w) r of
            Just LeqProof -> return $ SomeBVExpr r (EApp $ BVZext r w x)
            _ -> later $ describe "valid zero extension" $ empty
 
     bvSext :: m (SomeBVExpr s)
     bvSext =
-      do (PosNat r, SomeBVExpr w x) <- binary BVSext_ posNat (bvSubterm NoHint)
+      do (BoundedNat r, SomeBVExpr w x) <- binary BVSext_ posNat (bvSubterm NoHint)
          case testLeq (incNat w) r of
            Just LeqProof -> return $ SomeBVExpr r (EApp $ BVSext r w x)
            _ -> later $ describe "valid zero extension" $ empty
@@ -1160,14 +1271,19 @@ atomSetter (AtomName anText) =
          return $ Pair (ReferenceRepr t') anAtom
 
     fresh =
-      do Some t <- reading (unary Fresh isBaseType)
+      do t <- reading (unary Fresh ((Left <$> isBaseType) <|> (Right <$> isFloatingType)))
          describe "user symbol" $
            case userSymbol (T.unpack anText) of
              Left err -> describe (T.pack (show err)) empty
              Right nm ->
                do loc <- position
-                  Pair (baseToType t) <$>
-                    freshAtom loc (FreshConstant t (Just nm))
+                  case t of
+                    Left (Some bt) ->
+                      Pair (baseToType bt) <$>
+                        freshAtom loc (FreshConstant bt (Just nm))
+                    Right (Some fi) ->
+                      Pair (FloatRepr fi) <$>
+                        freshAtom loc (FreshFloat fi (Just nm))
 
     evaluated =
        do Pair tp e' <- reading synth
diff --git a/crucible-syntax/test-data/parser-tests/floats.cbl b/crucible-syntax/test-data/parser-tests/floats.cbl
new file mode 100644
index 000000000..b954e2abd
--- /dev/null
+++ b/crucible-syntax/test-data/parser-tests/floats.cbl
@@ -0,0 +1,74 @@
+;; exercise floating-point expression formers
+
+(defun @test-float () Unit
+  (start start:
+    (let a_f (fresh (FP Float)))
+    (let b_d (fresh (FP Double)))
+    (let c_h (fresh (FP Half)))
+    (let d_q (fresh (FP Quad)))
+    (let e_dd (fresh (FP DoubleDouble)))
+    (let f_x87 (fresh (FP X86_80)))
+
+    (let r1 (fresh Real))
+    (let r2 (fresh Real))
+    (let r3 (fresh Real))
+
+    (let bv16 (fresh (Bitvector 16)))
+    (let bv32 (fresh (Bitvector 32)))
+    (let bv64 (fresh (Bitvector 64)))
+    (let bv128 (fresh (Bitvector 128)))
+    (let bv80 (fresh (Bitvector 80)))
+
+    (let f16 (binary-to-fp Half bv16))
+    (let f32 (binary-to-fp Float bv32))
+    (let f64 (binary-to-fp Double bv64))
+    (let f128 (binary-to-fp Quad bv128))
+    (let fdd (binary-to-fp DoubleDouble bv128))
+    (let f80 (binary-to-fp X86_80 bv80))
+
+    (let n1 (fp-to-binary a_f))
+    (let n2 (fp-to-binary b_d))
+    (let n3 (fp-to-binary c_h))
+    (let n4 (fp-to-binary d_q))
+    (let n5 (fp-to-binary e_dd))
+    (let n6 (fp-to-binary f_x87))
+
+    (let u1 (ubv-to-fp Half rne bv64))
+    (let u2 (ubv-to-fp Float rna bv16))
+    (let u3 (ubv-to-fp Double rtp bv32))
+    (let u4 (ubv-to-fp Quad rtn bv80))
+    (let u5 (ubv-to-fp DoubleDouble rtz bv64))
+
+    (let s1 (sbv-to-fp Half rne bv64))
+    (let s2 (sbv-to-fp Float rna bv16))
+    (let s3 (sbv-to-fp Double rtp bv32))
+    (let s4 (sbv-to-fp Quad rtn bv80))
+    (let s5 (sbv-to-fp DoubleDouble rtz bv64))
+
+    (let x1 (fp-to-ubv 32 rne a_f))
+    (let x2 (fp-to-ubv 40 rna b_d))
+    (let x3 (fp-to-ubv 64 rtp c_h))
+    (let x4 (fp-to-ubv 16 rtn d_q))
+    (let x5 (fp-to-ubv 128 rtz e_dd))
+
+    (let y1 (fp-to-sbv 32 rne a_f))
+    (let y2 (fp-to-sbv 40 rna b_d))
+    (let y3 (fp-to-sbv 64 rtp c_h))
+    (let y4 (fp-to-sbv 16 rtn d_q))
+    (let y5 (fp-to-sbv 128 rtz e_dd))
+
+    (let w1 (fp-to-real a_f))
+    (let w2 (fp-to-real b_d))
+    (let w3 (fp-to-real c_h))
+    (let w4 (fp-to-real d_q))
+    (let w5 (fp-to-real e_dd))
+    (let w6 (fp-to-real f_x87))
+
+    (let q1 (real-to-fp Float rne r1))
+    (let q2 (real-to-fp Double rna r2))
+    (let q3 (real-to-fp Half rtp r3))
+    (let q4 (real-to-fp DoubleDouble rtn r1))
+    (let q5 (real-to-fp X86_80 rtz r2))
+
+    (return ()))
+)
diff --git a/crucible-syntax/test-data/parser-tests/floats.out.good b/crucible-syntax/test-data/parser-tests/floats.out.good
new file mode 100644
index 000000000..bcb07df22
--- /dev/null
+++ b/crucible-syntax/test-data/parser-tests/floats.out.good
@@ -0,0 +1,182 @@
+(defun @test-float () Unit
+   (start start:
+      (let a_f (fresh (FP Float)))
+      (let b_d (fresh (FP Double)))
+      (let c_h (fresh (FP Half)))
+      (let d_q (fresh (FP Quad)))
+      (let e_dd (fresh (FP DoubleDouble)))
+      (let f_x87 (fresh (FP X86_80)))
+      (let r1 (fresh Real))
+      (let r2 (fresh Real))
+      (let r3 (fresh Real))
+      (let bv16 (fresh (Bitvector 16)))
+      (let bv32 (fresh (Bitvector 32)))
+      (let bv64 (fresh (Bitvector 64)))
+      (let bv128 (fresh (Bitvector 128)))
+      (let bv80 (fresh (Bitvector 80)))
+      (let f16 (binary-to-fp Half bv16))
+      (let f32 (binary-to-fp Float bv32))
+      (let f64 (binary-to-fp Double bv64))
+      (let f128 (binary-to-fp Quad bv128))
+      (let fdd (binary-to-fp DoubleDouble bv128))
+      (let f80 (binary-to-fp X86_80 bv80))
+      (let n1 (fp-to-binary a_f))
+      (let n2 (fp-to-binary b_d))
+      (let n3 (fp-to-binary c_h))
+      (let n4 (fp-to-binary d_q))
+      (let n5 (fp-to-binary e_dd))
+      (let n6 (fp-to-binary f_x87))
+      (let u1 (ubv-to-fp Half rne bv64))
+      (let u2 (ubv-to-fp Float rna bv16))
+      (let u3 (ubv-to-fp Double rtp bv32))
+      (let u4 (ubv-to-fp Quad rtn bv80))
+      (let u5 (ubv-to-fp DoubleDouble rtz bv64))
+      (let s1 (sbv-to-fp Half rne bv64))
+      (let s2 (sbv-to-fp Float rna bv16))
+      (let s3 (sbv-to-fp Double rtp bv32))
+      (let s4 (sbv-to-fp Quad rtn bv80))
+      (let s5 (sbv-to-fp DoubleDouble rtz bv64))
+      (let x1 (fp-to-ubv 32 rne a_f))
+      (let x2 (fp-to-ubv 40 rna b_d))
+      (let x3 (fp-to-ubv 64 rtp c_h))
+      (let x4 (fp-to-ubv 16 rtn d_q))
+      (let x5 (fp-to-ubv 128 rtz e_dd))
+      (let y1 (fp-to-sbv 32 rne a_f))
+      (let y2 (fp-to-sbv 40 rna b_d))
+      (let y3 (fp-to-sbv 64 rtp c_h))
+      (let y4 (fp-to-sbv 16 rtn d_q))
+      (let y5 (fp-to-sbv 128 rtz e_dd))
+      (let w1 (fp-to-real a_f))
+      (let w2 (fp-to-real b_d))
+      (let w3 (fp-to-real c_h))
+      (let w4 (fp-to-real d_q))
+      (let w5 (fp-to-real e_dd))
+      (let w6 (fp-to-real f_x87))
+      (let q1 (real-to-fp Float rne r1))
+      (let q2 (real-to-fp Double rna r2))
+      (let q3 (real-to-fp Half rtp r3))
+      (let q4 (real-to-fp DoubleDouble rtn r1))
+      (let q5 (real-to-fp X86_80 rtz r2))
+      (return ())))
+
+test-float
+%0
+  % 5:14
+  $0 = fresh-float SingleFloatRepr a_f
+  % 6:14
+  $1 = fresh-float DoubleFloatRepr b_d
+  % 7:14
+  $2 = fresh-float HalfFloatRepr c_h
+  % 8:14
+  $3 = fresh-float QuadFloatRepr d_q
+  % 9:15
+  $4 = fresh-float DoubleDoubleFloatRepr e_dd
+  % 10:16
+  $5 = fresh-float X86_80FloatRepr f_x87
+  % 12:13
+  $6 = fresh BaseRealRepr r1
+  % 13:13
+  $7 = fresh BaseRealRepr r2
+  % 14:13
+  $8 = fresh BaseRealRepr r3
+  % 16:15
+  $9 = fresh BaseBVRepr 16 bv16
+  % 17:15
+  $10 = fresh BaseBVRepr 32 bv32
+  % 18:15
+  $11 = fresh BaseBVRepr 64 bv64
+  % 19:16
+  $12 = fresh BaseBVRepr 128 bv128
+  % 20:15
+  $13 = fresh BaseBVRepr 80 bv80
+  % 22:14
+  $14 = floatFromBinary(HalfFloatRepr, $9)
+  % 23:14
+  $15 = floatFromBinary(SingleFloatRepr, $10)
+  % 24:14
+  $16 = floatFromBinary(DoubleFloatRepr, $11)
+  % 25:15
+  $17 = floatFromBinary(QuadFloatRepr, $12)
+  % 26:14
+  $18 = floatFromBinary(DoubleDoubleFloatRepr, $12)
+  % 27:14
+  $19 = floatFromBinary(X86_80FloatRepr, $13)
+  % 29:13
+  $20 = floatToBinary(SingleFloatRepr, $0)
+  % 30:13
+  $21 = floatToBinary(DoubleFloatRepr, $1)
+  % 31:13
+  $22 = floatToBinary(HalfFloatRepr, $2)
+  % 32:13
+  $23 = floatToBinary(QuadFloatRepr, $3)
+  % 33:13
+  $24 = floatToBinary(DoubleDoubleFloatRepr, $4)
+  % 34:13
+  $25 = floatToBinary(X86_80FloatRepr, $5)
+  % 36:13
+  $26 = floatFromBV(HalfFloatRepr, RNE, $11)
+  % 37:13
+  $27 = floatFromBV(SingleFloatRepr, RNA, $9)
+  % 38:13
+  $28 = floatFromBV(DoubleFloatRepr, RTP, $10)
+  % 39:13
+  $29 = floatFromBV(QuadFloatRepr, RTN, $13)
+  % 40:13
+  $30 = floatFromBV(DoubleDoubleFloatRepr, RTZ, $11)
+  % 42:13
+  $31 = floatFromSBV(HalfFloatRepr, RNE, $11)
+  % 43:13
+  $32 = floatFromSBV(SingleFloatRepr, RNA, $9)
+  % 44:13
+  $33 = floatFromSBV(DoubleFloatRepr, RTP, $10)
+  % 45:13
+  $34 = floatFromSBV(QuadFloatRepr, RTN, $13)
+  % 46:13
+  $35 = floatFromSBV(DoubleDoubleFloatRepr, RTZ, $11)
+  % 48:13
+  $36 = floatToBV(32, RNE, $0)
+  % 49:13
+  $37 = floatToBV(40, RNA, $1)
+  % 50:13
+  $38 = floatToBV(64, RTP, $2)
+  % 51:13
+  $39 = floatToBV(16, RTN, $3)
+  % 52:13
+  $40 = floatToBV(128, RTZ, $4)
+  % 54:13
+  $41 = floatToSBV(32, RNE, $0)
+  % 55:13
+  $42 = floatToSBV(40, RNA, $1)
+  % 56:13
+  $43 = floatToSBV(64, RTP, $2)
+  % 57:13
+  $44 = floatToSBV(16, RTN, $3)
+  % 58:13
+  $45 = floatToSBV(128, RTZ, $4)
+  % 60:13
+  $46 = floatToReal($0)
+  % 61:13
+  $47 = floatToReal($1)
+  % 62:13
+  $48 = floatToReal($2)
+  % 63:13
+  $49 = floatToReal($3)
+  % 64:13
+  $50 = floatToReal($4)
+  % 65:13
+  $51 = floatToReal($5)
+  % 67:13
+  $52 = floatFromReal(SingleFloatRepr, RNE, $6)
+  % 68:13
+  $53 = floatFromReal(DoubleFloatRepr, RNA, $7)
+  % 69:13
+  $54 = floatFromReal(HalfFloatRepr, RTP, $8)
+  % 70:13
+  $55 = floatFromReal(DoubleDoubleFloatRepr, RTN, $6)
+  % 71:13
+  $56 = floatFromReal(X86_80FloatRepr, RTZ, $7)
+  % 73:13
+  $57 = emptyApp()
+  % 73:5
+  return $57
+  % no postdom

From f51836fb3aa13deca2b6c863e1cb42e2025f4e5a Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Thu, 4 Apr 2019 17:15:51 -0700
Subject: [PATCH 4/8] Add a new convenience `println` statement to the crucible
 concrete syntax. It simply appends a newline to the string to be printed.

---
 crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs    | 3 ++-
 crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs | 9 +++++++--
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs
index d0a280759..640e13c84 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs
@@ -65,7 +65,7 @@ data Keyword = Defun | DefBlock | DefGlobal
              | VectorGetEntry_ | VectorSetEntry_ | VectorCons_
              | Deref | Ref | EmptyRef
              | Jump_ | Return_ | Branch_ | MaybeBranch_ | TailCall_ | Error_ | Output_ | Case
-             | Print_
+             | Print_ | PrintLn_
              | Let | Fresh
              | Assert_ | Assume_
              | SetRegister
@@ -104,6 +104,7 @@ keywords =
   , ("error", Error_)
   , ("output", Output_)
   , ("print" , Print_)
+  , ("println" , PrintLn_)
   , ("Ref", RefT)
   , ("deref", Deref)
   , ("ref", Ref)
diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
index 2828421a0..2e1aec0ea 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
@@ -1331,17 +1331,22 @@ normStmt' :: forall h s m
            . (MonadWriter [Posd (Stmt () s)] m, MonadSyntax Atomic m, MonadState (SyntaxState h s) m, MonadST h m) =>
              m ()
 normStmt' =
-  call (printStmt <|> letStmt <|> (void funcall) <|>
+  call (printStmt <|> printLnStmt <|> letStmt <|> (void funcall) <|>
         setGlobal <|> setReg <|> setRef <|> dropRef <|>
         assertion <|> assumption)
 
   where
-    printStmt, letStmt, setGlobal, setReg, setRef, dropRef, assertion :: m ()
+    printStmt, printLnStmt, letStmt, setGlobal, setReg, setRef, dropRef, assertion :: m ()
     printStmt =
       do Posd loc e <- unary Print_ (located $ reading $ check StringRepr)
          strAtom <- eval loc e
          tell [Posd loc (Print strAtom)]
 
+    printLnStmt =
+      do Posd loc e <- unary PrintLn_ (located $ reading $ check StringRepr)
+         strAtom <- eval loc (EApp (AppendString e (EApp (TextLit "\n"))))
+         tell [Posd loc (Print strAtom)]
+
     letStmt =
       followedBy (kw Let) $
       depCons uniqueAtom $

From 82f1e485c854b3fb11c099f4b0395390d5e0dcb8 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Wed, 10 Apr 2019 10:46:07 -0700
Subject: [PATCH 5/8] Provide additional support for floats in
 `crucible-syntax` (equality, if/then/else, show), and improve error messages
 for float casts that fail type-checking.

---
 .../src/Lang/Crucible/Syntax/Concrete.hs      | 64 ++++++++++---------
 .../test-data/parser-tests/floats.cbl         |  3 +
 .../test-data/parser-tests/floats.out.good    | 14 ++--
 crucible/src/Lang/Crucible/CFG/Expr.hs        |  5 ++
 .../src/Lang/Crucible/Simulator/Evaluation.hs |  3 +
 5 files changed, 56 insertions(+), 33 deletions(-)

diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
index 2e1aec0ea..1810f863f 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
@@ -562,12 +562,14 @@ synthExpr typeHint =
       do (e1, e2) <- describe "equality test" $ binary Equalp synth' synth'
          matchingExprs Nothing e1 e2 $ \tp e1' e2' ->
           case tp of
+            FloatRepr _fi ->
+              return $ SomeE BoolRepr $ EApp $ FloatEq e1' e2'
             ReferenceRepr rtp ->
               return $ SomeE BoolRepr $ EApp $ ReferenceEq rtp e1' e2'
             (asBaseType -> AsBaseType bt) ->
               return $ SomeE BoolRepr $ EApp $ BaseIsEq bt e1' e2'
             _ ->
-              later $ describe ("a base type or reference type (got " <> T.pack (show tp) <> ")") empty
+              later $ describe ("a base type or floating point type or reference type (got " <> T.pack (show tp) <> ")") empty
 
     compareBV ::
       Keyword ->
@@ -682,7 +684,7 @@ synthExpr typeHint =
                Just (Some idx) ->
                  do let ty = MaybeRepr (ts^.ixF' idx)
                     return $ SomeE ty $ EApp $ ProjectVariant ts idx e
-           _ -> describe ("expecting variant type (got " <> T.pack (show t) <> ")") empty
+           _ -> describe ("variant type (got " <> T.pack (show t) <> ")") empty
 
     injection :: m (SomeExpr s)
     injection =
@@ -700,18 +702,18 @@ synthExpr typeHint =
            Just (Some t) ->
              describe ("context expecting variant type (got " <> T.pack (show t) <> ")") empty
            Nothing ->
-             describe ("expected unambiguous variant") empty
+             describe ("unambiguous variant") empty
 
     fpToBinary :: m (SomeExpr s)
     fpToBinary =
        kw FPToBinary_ `followedBy`
-       (depCons synth $ \(Pair tp x) ->
+       (depConsCond synth $ \(Pair tp x) ->
          case tp of
            FloatRepr fpi
              | BaseBVRepr w <- floatInfoToBVTypeRepr fpi
              , Just LeqProof <- isPosNat w ->
-                 emptyList $> (SomeE (BVRepr w) $ EApp $ FloatToBinary fpi x)
-           _ -> empty)
+                 emptyList $> (Right $ SomeE (BVRepr w) $ EApp $ FloatToBinary fpi x)
+           _ -> pure $ Left $ "floating-point value")
 
     binaryToFp :: m (SomeExpr s)
     binaryToFp =
@@ -723,10 +725,10 @@ synthExpr typeHint =
     fpToReal :: m (SomeExpr s)
     fpToReal =
        kw FPToReal_ `followedBy`
-       (depCons synth $ \(Pair tp x) ->
+       (depConsCond synth $ \(Pair tp x) ->
          case tp of
-           FloatRepr _fpi -> emptyList $> (SomeE RealValRepr $ EApp $ FloatToReal x)
-           _ -> empty)
+           FloatRepr _fpi -> emptyList $> (Right $ SomeE RealValRepr $ EApp $ FloatToReal x)
+           _ -> pure $ Left "floating-point value")
 
     realToFp :: m (SomeExpr s)
     realToFp =
@@ -741,11 +743,11 @@ synthExpr typeHint =
        kw UBVToFP_ `followedBy`
        (depCons fpinfo $ \(Some fpi) ->
         depCons roundingMode $ \rm ->
-        depCons synth $ \(Pair tp x) ->
+        depConsCond synth $ \(Pair tp x) ->
           case tp of
             BVRepr _w ->
-              emptyList $> (SomeE (FloatRepr fpi) $ EApp $ FloatFromBV fpi rm x)
-            _ -> empty
+              emptyList $> (Right $ SomeE (FloatRepr fpi) $ EApp $ FloatFromBV fpi rm x)
+            _ -> pure $ Left $ "bitvector value"
         )
 
     sbvToFloat :: m (SomeExpr s)
@@ -753,11 +755,11 @@ synthExpr typeHint =
        kw SBVToFP_ `followedBy`
        (depCons fpinfo $ \(Some fpi) ->
         depCons roundingMode $ \rm ->
-        depCons synth $ \(Pair tp x) ->
+        depConsCond synth $ \(Pair tp x) ->
           case tp of
             BVRepr _w ->
-              emptyList $> (SomeE (FloatRepr fpi) $ EApp $ FloatFromSBV fpi rm x)
-            _ -> empty
+              emptyList $> (Right $ SomeE (FloatRepr fpi) $ EApp $ FloatFromSBV fpi rm x)
+            _ -> pure $ Left $ "bitvector value"
        )
 
     floatToUBV :: m (SomeExpr s)
@@ -765,22 +767,22 @@ synthExpr typeHint =
        kw FPToUBV_ `followedBy`
        (depCons posNat $ \(BoundedNat w) ->
         depCons roundingMode $ \rm ->
-        depCons synth $ \(Pair tp x) ->
+        depConsCond synth $ \(Pair tp x) ->
           case tp of
             FloatRepr _fpi ->
-              emptyList $> (SomeE (BVRepr w) $ EApp $ FloatToBV w rm x)
-            _ -> empty)
+              emptyList $> (Right $ SomeE (BVRepr w) $ EApp $ FloatToBV w rm x)
+            _ -> pure $ Left $ "floating-point value")
 
     floatToSBV :: m (SomeExpr s)
     floatToSBV =
        kw FPToSBV_ `followedBy`
        (depCons posNat $ \(BoundedNat w) ->
         depCons roundingMode $ \rm ->
-        depCons synth $ \(Pair tp x) ->
+        depConsCond synth $ \(Pair tp x) ->
           case tp of
             FloatRepr _fpi ->
-              emptyList $> (SomeE (BVRepr w) $ EApp $ FloatToSBV w rm x)
-            _ -> empty)
+              emptyList $> (Right $ SomeE (BVRepr w) $ EApp $ FloatToSBV w rm x)
+            _ -> pure $ Left $ "floating-point value")
 
     ite :: m (SomeExpr s)
     ite =
@@ -791,14 +793,16 @@ synthExpr typeHint =
            cons (synthExpr typeHint) $
            emptyList
          matchingExprs typeHint et ef $ \tp t f ->
-           case asBaseType tp of
-             NotBaseType ->
-               let msg = T.concat [ "conditional where branches have base type (got "
+          case tp of
+            FloatRepr fi ->
+               return $ SomeE tp $ EApp $ FloatIte fi c t f
+            (asBaseType -> AsBaseType bty) ->
+               return $ SomeE tp $ EApp $ BaseIte bty c t f
+            _ ->
+               let msg = T.concat [ "conditional where branches have base or floating point type (got "
                                   , T.pack (show tp)
                                   ]
                in later $ describe msg empty
-             AsBaseType bty ->
-               return $ SomeE tp $ EApp $ BaseIte bty c t f
 
     toAny =
       do Pair tp e <- unary ToAny synth
@@ -887,10 +891,12 @@ synthExpr typeHint =
     showExpr :: m (SomeExpr s)
     showExpr =
       do Pair t1 e <- unary Show synth
-         case asBaseType t1 of
-           NotBaseType -> describe ("base type, but got " <> T.pack (show t1)) empty
-           AsBaseType bt ->
+         case t1 of
+           FloatRepr fi ->
+             return $ SomeE StringRepr $ EApp $ ShowFloat fi e
+           _ | AsBaseType bt <- asBaseType t1 ->
              return $ SomeE StringRepr $ EApp $ ShowValue bt e
+           _ -> describe ("base or floating point type, but got " <> T.pack (show t1)) empty
 
 data NatHint
   = NoHint
diff --git a/crucible-syntax/test-data/parser-tests/floats.cbl b/crucible-syntax/test-data/parser-tests/floats.cbl
index b954e2abd..1f29b06d1 100644
--- a/crucible-syntax/test-data/parser-tests/floats.cbl
+++ b/crucible-syntax/test-data/parser-tests/floats.cbl
@@ -70,5 +70,8 @@
     (let q4 (real-to-fp DoubleDouble rtn r1))
     (let q5 (real-to-fp X86_80 rtz r2))
 
+    (let b (fresh Bool))
+    (let ite (if b u3 q2))
+
     (return ()))
 )
diff --git a/crucible-syntax/test-data/parser-tests/floats.out.good b/crucible-syntax/test-data/parser-tests/floats.out.good
index bcb07df22..30acc0f69 100644
--- a/crucible-syntax/test-data/parser-tests/floats.out.good
+++ b/crucible-syntax/test-data/parser-tests/floats.out.good
@@ -57,6 +57,8 @@
       (let q3 (real-to-fp Half rtp r3))
       (let q4 (real-to-fp DoubleDouble rtn r1))
       (let q5 (real-to-fp X86_80 rtz r2))
+      (let b (fresh Bool))
+      (let ite (if b u3 q2))
       (return ())))
 
 test-float
@@ -175,8 +177,12 @@ test-float
   $55 = floatFromReal(DoubleDoubleFloatRepr, RTN, $6)
   % 71:13
   $56 = floatFromReal(X86_80FloatRepr, RTZ, $7)
-  % 73:13
-  $57 = emptyApp()
-  % 73:5
-  return $57
+  % 73:12
+  $57 = fresh BaseBoolRepr b
+  % 74:14
+  $58 = floatIte(DoubleFloatRepr, $57, $28, $53)
+  % 76:13
+  $59 = emptyApp()
+  % 76:5
+  return $59
   % no postdom
diff --git a/crucible/src/Lang/Crucible/CFG/Expr.hs b/crucible/src/Lang/Crucible/CFG/Expr.hs
index 1d14ca6d8..ee144e60b 100644
--- a/crucible/src/Lang/Crucible/CFG/Expr.hs
+++ b/crucible/src/Lang/Crucible/CFG/Expr.hs
@@ -923,6 +923,10 @@ data App (ext :: Type) (f :: CrucibleType -> Type) (tp :: CrucibleType) where
             -> !(f (BaseToType bt))
             -> App ext f StringType
 
+  ShowFloat :: !(FloatInfoRepr fi)
+            -> !(f (FloatType fi))
+            -> App ext f StringType
+
   AppendString :: !(f StringType)
                -> !(f StringType)
                -> App ext f StringType
@@ -1203,6 +1207,7 @@ instance TypeApp (ExprExtension ext) => TypeApp (App ext) where
 
     TextLit{} -> knownRepr
     ShowValue{} -> knownRepr
+    ShowFloat{} -> knownRepr
     AppendString{} -> knownRepr
 
     ------------------------------------------------------------------------
diff --git a/crucible/src/Lang/Crucible/Simulator/Evaluation.hs b/crucible/src/Lang/Crucible/Simulator/Evaluation.hs
index 224bc4e4e..0ddecb8dc 100644
--- a/crucible/src/Lang/Crucible/Simulator/Evaluation.hs
+++ b/crucible/src/Lang/Crucible/Simulator/Evaluation.hs
@@ -923,6 +923,9 @@ evalApp sym itefns _logFn evalExt (evalSub :: forall tp. f tp -> IO (RegValue sy
     ShowValue _bt x_expr -> do
       x <- evalSub x_expr
       stringLit sym (Text.pack (show (printSymExpr x)))
+    ShowFloat _fi x_expr -> do
+      x <- evalSub x_expr
+      stringLit sym (Text.pack (show (printSymExpr x)))
     AppendString x y -> do
       x' <- evalSub x
       y' <- evalSub y

From f93e44a1282332fbc03aff1d232e5a1d66fdc945 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Wed, 10 Apr 2019 11:45:30 -0700
Subject: [PATCH 6/8] Tweak error message

---
 crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
index 1810f863f..7088f188d 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
@@ -896,7 +896,7 @@ synthExpr typeHint =
              return $ SomeE StringRepr $ EApp $ ShowFloat fi e
            _ | AsBaseType bt <- asBaseType t1 ->
              return $ SomeE StringRepr $ EApp $ ShowValue bt e
-           _ -> describe ("base or floating point type, but got " <> T.pack (show t1)) empty
+           _ -> later $ describe ("base or floating point type, but got " <> T.pack (show t1)) empty
 
 data NatHint
   = NoHint

From d986943d347634b18cfaa3cff6ad27bb4b3b9910 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Wed, 10 Apr 2019 11:46:29 -0700
Subject: [PATCH 7/8] Have the simulator tests in crucible-syntax attempt to
 discharge each proof obligation, and print the result (PROVED,
 COUNTEREXAMPLE, or UNKNOWN).

Fix up the test golden files to match.

In addition, add a test exercising floating-point conversions.
---
 .../src/Lang/Crucible/Syntax/Prog.hs          | 19 ++++++++++---
 .../test-data/simulator-tests/assert.out.good |  1 +
 .../simulator-tests/assume-merge.out.good     |  2 ++
 .../simulator-tests/assume-merge2.out.good    |  1 +
 .../test-data/simulator-tests/assume.out.good |  1 +
 .../test-data/simulator-tests/branch.out.good |  1 +
 .../test-data/simulator-tests/calls.cbl       |  2 ++
 .../test-data/simulator-tests/calls.out.good  |  5 +++-
 .../simulator-tests/double-branch.out.good    |  1 +
 .../test-data/simulator-tests/float-cast.cbl  | 27 +++++++++++++++++++
 .../simulator-tests/float-cast.out.good       | 25 +++++++++++++++++
 .../simulator-tests/from-maybe.out.good       |  2 ++
 .../simulator-tests/loop-err.out.good         |  4 +++
 .../test-data/simulator-tests/loop.out.good   |  1 +
 .../simulator-tests/override-test.out.good    |  1 +
 .../simulator-tests/override-test2.out.good   |  2 ++
 16 files changed, 91 insertions(+), 4 deletions(-)
 create mode 100644 crucible-syntax/test-data/simulator-tests/float-cast.cbl
 create mode 100644 crucible-syntax/test-data/simulator-tests/float-cast.out.good

diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
index f7b508853..a8a3a5d3a 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
@@ -5,9 +5,11 @@
 
 module Lang.Crucible.Syntax.Prog where
 
+import Control.Lens (view)
 import Control.Monad.ST
 import Control.Monad
 
+import Data.Foldable (toList)
 import Data.List (find)
 import Data.Text (Text)
 import Data.String (IsString(..))
@@ -18,7 +20,7 @@ import System.Exit
 import Text.Megaparsec as MP
 
 import Data.Parameterized.Nonce
-import Data.Parameterized.Context as Ctx
+import qualified Data.Parameterized.Context as Ctx
 import Data.Parameterized.Some (Some(Some))
 
 import qualified Lang.Crucible.CFG.Core as C
@@ -39,9 +41,11 @@ import Lang.Crucible.Simulator
 import Lang.Crucible.Simulator.Profiling
 
 import What4.Config
-import What4.Interface (getConfiguration)
+import What4.Interface (getConfiguration,notPred)
 import What4.Expr.Builder (Flags, FloatIEEE, ExprBuilder)
 import What4.ProgramLoc
+import What4.SatResult
+import What4.Solver (defaultLogData, runZ3InOverride)
 
 
 -- | The main loop body, useful for both the program and for testing.
@@ -132,7 +136,16 @@ simulateProgram fn theInput outh profh opts setup =
                          Nothing -> hPutStrLn outh "==== No proof obligations ===="
                          Just gs ->
                            do hPutStrLn outh "==== Proof obligations ===="
-                              mapM_ (hPrint outh . ppProofObligation sym) (goalsToList gs)
+                              forM_ (goalsToList gs) (\g ->
+                                do hPrint outh (ppProofObligation sym g)
+                                   neggoal <- notPred sym (view labeledPred (proofGoal g))
+                                   let bs = neggoal : map (view labeledPred) (toList (proofAssumptions g))
+                                   runZ3InOverride sym defaultLogData bs (\case
+                                     Sat _   -> hPutStrLn outh "COUNTEREXAMPLE"
+                                     Unsat _ -> hPutStrLn outh "PROVED"
+                                     Unknown -> hPutStrLn outh "UNKNOWN"
+                                     )
+                                )
 
                   _ -> hPutStrLn outh "No suitable main function found"
 
diff --git a/crucible-syntax/test-data/simulator-tests/assert.out.good b/crucible-syntax/test-data/simulator-tests/assert.out.good
index cb2b469d8..d1475f490 100644
--- a/crucible-syntax/test-data/simulator-tests/assert.out.good
+++ b/crucible-syntax/test-data/simulator-tests/assert.out.good
@@ -7,3 +7,4 @@ Prove:
   x is true
   in main at test-data/simulator-tests/assert.cbl:4:5
   cx@2:b
+COUNTEREXAMPLE
diff --git a/crucible-syntax/test-data/simulator-tests/assume-merge.out.good b/crucible-syntax/test-data/simulator-tests/assume-merge.out.good
index c5e80b7db..5ea5e604e 100644
--- a/crucible-syntax/test-data/simulator-tests/assume-merge.out.good
+++ b/crucible-syntax/test-data/simulator-tests/assume-merge.out.good
@@ -11,6 +11,7 @@ Prove:
   oopsie!
   in main at test-data/simulator-tests/assume-merge.cbl:12:5
   false
+COUNTEREXAMPLE
 Assuming:
 * The branch in main from test-data/simulator-tests/assume-merge.cbl:4:5 to test-data/simulator-tests/assume-merge.cbl:9:14
     boolNot (intLe 0 cx@2:i)
@@ -20,3 +21,4 @@ Prove:
   oopsie!
   in main at test-data/simulator-tests/assume-merge.cbl:12:5
   false
+COUNTEREXAMPLE
diff --git a/crucible-syntax/test-data/simulator-tests/assume-merge2.out.good b/crucible-syntax/test-data/simulator-tests/assume-merge2.out.good
index ca2f667fa..b9042a6fb 100644
--- a/crucible-syntax/test-data/simulator-tests/assume-merge2.out.good
+++ b/crucible-syntax/test-data/simulator-tests/assume-merge2.out.good
@@ -15,3 +15,4 @@ Prove:
   oopsie!
   in main at test-data/simulator-tests/assume-merge2.cbl:12:5
   false
+COUNTEREXAMPLE
diff --git a/crucible-syntax/test-data/simulator-tests/assume.out.good b/crucible-syntax/test-data/simulator-tests/assume.out.good
index e8ad18c8c..587850126 100644
--- a/crucible-syntax/test-data/simulator-tests/assume.out.good
+++ b/crucible-syntax/test-data/simulator-tests/assume.out.good
@@ -9,3 +9,4 @@ Prove:
   error statement
   in main at test-data/simulator-tests/assume.cbl:5:5
   false
+COUNTEREXAMPLE
diff --git a/crucible-syntax/test-data/simulator-tests/branch.out.good b/crucible-syntax/test-data/simulator-tests/branch.out.good
index 19641ad87..a887d3aa4 100644
--- a/crucible-syntax/test-data/simulator-tests/branch.out.good
+++ b/crucible-syntax/test-data/simulator-tests/branch.out.good
@@ -7,3 +7,4 @@ Prove:
   bogus condition
   in main at test-data/simulator-tests/branch.cbl:11:5
   boolAnd (intEq 42 cx@3:i) cp@2:b
+COUNTEREXAMPLE
diff --git a/crucible-syntax/test-data/simulator-tests/calls.cbl b/crucible-syntax/test-data/simulator-tests/calls.cbl
index b684a5439..25097cd01 100644
--- a/crucible-syntax/test-data/simulator-tests/calls.cbl
+++ b/crucible-syntax/test-data/simulator-tests/calls.cbl
@@ -2,6 +2,8 @@
   (start start:
     (let x (fresh Integer))
     (let y (funcall @f x))
+    (println (show x))
+    (println (show y))
     (assert! (equal? x y) "bogus")
     (return ())))
 
diff --git a/crucible-syntax/test-data/simulator-tests/calls.out.good b/crucible-syntax/test-data/simulator-tests/calls.out.good
index 203b6da7a..309832b90 100644
--- a/crucible-syntax/test-data/simulator-tests/calls.out.good
+++ b/crucible-syntax/test-data/simulator-tests/calls.out.good
@@ -1,9 +1,12 @@
 ==== Begin Simulation ====
+cx@2:i
+intSum cx@2:i 42
 
 ==== Finish Simulation ====
 ==== Proof obligations ====
 
 Prove:
   bogus
-  in main at test-data/simulator-tests/calls.cbl:5:5
+  in main at test-data/simulator-tests/calls.cbl:7:5
   false
+COUNTEREXAMPLE
diff --git a/crucible-syntax/test-data/simulator-tests/double-branch.out.good b/crucible-syntax/test-data/simulator-tests/double-branch.out.good
index e397d385c..9de04c3cf 100644
--- a/crucible-syntax/test-data/simulator-tests/double-branch.out.good
+++ b/crucible-syntax/test-data/simulator-tests/double-branch.out.good
@@ -11,3 +11,4 @@ Prove:
   assert
   in main at test-data/simulator-tests/double-branch.cbl:9:5
   intEq 5 ca@2:i
+PROVED
diff --git a/crucible-syntax/test-data/simulator-tests/float-cast.cbl b/crucible-syntax/test-data/simulator-tests/float-cast.cbl
new file mode 100644
index 000000000..93febcee9
--- /dev/null
+++ b/crucible-syntax/test-data/simulator-tests/float-cast.cbl
@@ -0,0 +1,27 @@
+
+(defun @main () Unit
+  (start start:
+    (let a (fresh (FP Double)))
+    (let b (fp-to-binary a))   
+    (let c (binary-to-fp Double b))
+
+    (println (show b))
+    (println (show c))
+
+    (let x (fresh (Bitvector 64)))
+    (let y (binary-to-fp Double x))
+    (let z (fp-to-binary y))
+
+    (println (show y))
+    (println (show z))
+
+    (let u (fp-to-ubv 64 rne a))
+    (println (show u))
+    (assert! (equal? a (ubv-to-fp Double rne u)) "bad unsigned round trip")
+
+    (let s (fp-to-sbv 64 rne a))
+    (println (show s))
+    (assert! (equal? a (sbv-to-fp Double rne s)) "bad signed round trip")
+
+    (return ()))
+)
diff --git a/crucible-syntax/test-data/simulator-tests/float-cast.out.good b/crucible-syntax/test-data/simulator-tests/float-cast.out.good
new file mode 100644
index 000000000..3974189db
--- /dev/null
+++ b/crucible-syntax/test-data/simulator-tests/float-cast.out.good
@@ -0,0 +1,25 @@
+==== Begin Simulation ====
+floatToBinary ca@2:f
+ca@2:f
+floatFromBinary cx@4:bv
+floatToBinary (floatFromBinary cx@4:bv)
+floatToBV RNE ca@2:f
+floatToSBV RNE ca@2:f
+
+==== Finish Simulation ====
+==== Proof obligations ====
+
+Prove:
+  bad unsigned round trip
+  in main at test-data/simulator-tests/float-cast.cbl:20:5
+  floatEq ca@2:f (bvToFloat RNE (floatToBV RNE ca@2:f))
+COUNTEREXAMPLE
+Assuming:
+* bad unsigned round trip
+    in main at test-data/simulator-tests/float-cast.cbl:20:5
+    floatEq ca@2:f (bvToFloat RNE (floatToBV RNE ca@2:f))
+Prove:
+  bad signed round trip
+  in main at test-data/simulator-tests/float-cast.cbl:24:5
+  floatEq ca@2:f (sbvToFloat RNE (floatToSBV RNE ca@2:f))
+COUNTEREXAMPLE
diff --git a/crucible-syntax/test-data/simulator-tests/from-maybe.out.good b/crucible-syntax/test-data/simulator-tests/from-maybe.out.good
index 1b2e08cd5..05c025cbc 100644
--- a/crucible-syntax/test-data/simulator-tests/from-maybe.out.good
+++ b/crucible-syntax/test-data/simulator-tests/from-maybe.out.good
@@ -7,6 +7,7 @@ Prove:
   OK to project z
   in main at test-data/simulator-tests/from-maybe.cbl:11:12
   cp@2:b
+COUNTEREXAMPLE
 Assuming:
 * OK to project z
     in main at test-data/simulator-tests/from-maybe.cbl:11:12
@@ -15,3 +16,4 @@ Prove:
   from-just eq (bogus)
   in main at test-data/simulator-tests/from-maybe.cbl:12:5
   false
+COUNTEREXAMPLE
diff --git a/crucible-syntax/test-data/simulator-tests/loop-err.out.good b/crucible-syntax/test-data/simulator-tests/loop-err.out.good
index 8540d5754..529575bdf 100644
--- a/crucible-syntax/test-data/simulator-tests/loop-err.out.good
+++ b/crucible-syntax/test-data/simulator-tests/loop-err.out.good
@@ -11,6 +11,7 @@ Prove:
   oopsie!
   in main at test-data/simulator-tests/loop-err.cbl:27:5
   false
+COUNTEREXAMPLE
 Assuming:
 * in main test-data/simulator-tests/loop-err.cbl:10:5: nonzero start
     boolNot (natEq 0 cx@2:n)
@@ -22,6 +23,7 @@ Prove:
   oopsie!
   in main at test-data/simulator-tests/loop-err.cbl:27:5
   false
+PROVED
 Assuming:
 * in main test-data/simulator-tests/loop-err.cbl:10:5: nonzero start
     boolNot (natEq 0 cx@2:n)
@@ -35,6 +37,7 @@ Prove:
   oopsie!
   in main at test-data/simulator-tests/loop-err.cbl:27:5
   false
+PROVED
 Assuming:
 * in main test-data/simulator-tests/loop-err.cbl:10:5: nonzero start
     boolNot (natEq 0 cx@2:n)
@@ -48,3 +51,4 @@ Prove:
   nonzero
   in main at test-data/simulator-tests/loop-err.cbl:23:5
   boolNot (natLe (natSum 8* cx@2:n) 0)
+PROVED
diff --git a/crucible-syntax/test-data/simulator-tests/loop.out.good b/crucible-syntax/test-data/simulator-tests/loop.out.good
index 9a0223cda..d17b43d8c 100644
--- a/crucible-syntax/test-data/simulator-tests/loop.out.good
+++ b/crucible-syntax/test-data/simulator-tests/loop.out.good
@@ -9,3 +9,4 @@ Prove:
   nonzero
   in main at test-data/simulator-tests/loop.cbl:19:5
   boolNot (natLe (natSum 8* cx@2:n) 0)
+PROVED
diff --git a/crucible-syntax/test-data/simulator-tests/override-test.out.good b/crucible-syntax/test-data/simulator-tests/override-test.out.good
index f71cbadc8..a6e64eeb9 100644
--- a/crucible-syntax/test-data/simulator-tests/override-test.out.good
+++ b/crucible-syntax/test-data/simulator-tests/override-test.out.good
@@ -7,3 +7,4 @@ Prove:
   should be true!
   in main at test-data/simulator-tests/override-test.cbl:7:5
   intEq (intIte cp@2:b cx@3:i cy@4:i) (intIte cp@2:b cx@3:i cy@4:i)
+PROVED
diff --git a/crucible-syntax/test-data/simulator-tests/override-test2.out.good b/crucible-syntax/test-data/simulator-tests/override-test2.out.good
index e3479d419..3652d066c 100644
--- a/crucible-syntax/test-data/simulator-tests/override-test2.out.good
+++ b/crucible-syntax/test-data/simulator-tests/override-test2.out.good
@@ -13,6 +13,7 @@ Prove:
   fall-through branch
   in symbolicBranchesTest at default branch
   false
+COUNTEREXAMPLE
 Assuming:
 * The branch in symbolicBranchesTest from after branch 1 to third branch
     let -- default branch
@@ -24,3 +25,4 @@ Prove:
   let -- default branch
       v23 = intSum 2* cx@2:i (intIte (intEq 2 cx@2:i) 0 cy@3:i)
    in intEq (intIte (intEq 1 cx@2:i) cy@3:i v23) cx@2:i
+COUNTEREXAMPLE

From 743cb8689c0235d12d87fc055b2282bc14a791bd Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Thu, 11 Apr 2019 09:13:33 -0700
Subject: [PATCH 8/8] Minor tweak to error message, and code style

---
 crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
index 7088f188d..7febf2bf8 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
@@ -799,7 +799,7 @@ synthExpr typeHint =
             (asBaseType -> AsBaseType bty) ->
                return $ SomeE tp $ EApp $ BaseIte bty c t f
             _ ->
-               let msg = T.concat [ "conditional where branches have base or floating point type (got "
+               let msg = T.concat [ "conditional where branches have base or floating point type, but got "
                                   , T.pack (show tp)
                                   ]
                in later $ describe msg empty
@@ -894,7 +894,7 @@ synthExpr typeHint =
          case t1 of
            FloatRepr fi ->
              return $ SomeE StringRepr $ EApp $ ShowFloat fi e
-           _ | AsBaseType bt <- asBaseType t1 ->
+           (asBaseType -> AsBaseType bt) ->
              return $ SomeE StringRepr $ EApp $ ShowValue bt e
            _ -> later $ describe ("base or floating point type, but got " <> T.pack (show t1)) empty