Structured assertions

crucible-jvm/src/Lang/Crucible/JVM/Translation.hs

@@ -41,19 +41,19 @@ module Lang.Crucible.JVM.Translation
   where
 
 -- base
-import Data.Maybe (maybeToList)
-import Data.Semigroup(Semigroup(..),(<>))
-import Control.Monad.State.Strict
-import Control.Monad.ST
-import Control.Lens hiding (op, (:>))
-import Data.Int (Int32)
-import Data.Map.Strict (Map)
+import           Data.Maybe (maybeToList)
+import           Data.Semigroup (Semigroup(..),(<>))
+import           Control.Monad.State.Strict
+import           Control.Monad.ST
+import           Control.Lens hiding (op, (:>))
+import           Data.Int (Int32)
+import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
-import Data.String (fromString)
-import Data.List (isPrefixOf)
+import           Data.String (fromString)
+import           Data.List (isPrefixOf)
 
-import System.IO
+import           System.IO
 
 -- jvm-parser
 import qualified Language.JVM.Common as J
@@ -70,6 +70,7 @@ import           Data.Parameterized.NatRepr as NR
 import qualified Lang.Crucible.CFG.Core as C
 import           Lang.Crucible.CFG.Expr
 import           Lang.Crucible.CFG.Generator
+import           Lang.Crucible.CFG.Extension.Safety (pattern PartialExp)
 import           Lang.Crucible.CFG.SSAConversion (toSSA)
 import           Lang.Crucible.FunctionHandle
 import           Lang.Crucible.Types
@@ -78,17 +79,18 @@ import           Lang.Crucible.Panic
 
 import           Lang.Crucible.Utils.MonadVerbosity
 
-import qualified Lang.Crucible.Simulator               as C
-import qualified Lang.Crucible.Simulator.GlobalState   as C
-import qualified Lang.Crucible.Analysis.Postdom        as C
-import qualified Lang.Crucible.Simulator.CallFrame     as C
+import qualified Lang.Crucible.Simulator as C
+import qualified Lang.Crucible.Simulator.GlobalState as C
+import qualified Lang.Crucible.Analysis.Postdom as C
+import qualified Lang.Crucible.Simulator.CallFrame as C
 
 
 -- what4
 import           What4.ProgramLoc (Position(InternalPos))
 import           What4.FunctionName
-import qualified What4.Interface                       as W4
-import qualified What4.Config                          as W4
+import qualified What4.Interface as W4
+import qualified What4.Config as W4
+import qualified What4.Partial.AssertionTree as W4AT
 
 import           What4.Utils.MonadST (liftST)
 
@@ -102,7 +104,7 @@ import           Lang.Crucible.JVM.Overrides
 import qualified Lang.JVM.Codebase as JCB
 
 
-import Debug.Trace
+import           Debug.Trace
 
 {-
    This module is in two parts, the first part includes functions for translating
@@ -739,14 +741,8 @@ generateInstruction (pc, instr) =
     J.Iadd  -> binary iPop iPop iPush (\a b -> App (BVAdd w32 a b))
     J.Isub  -> binary iPop iPop iPush (\a b -> App (BVSub w32 a b))
     J.Imul  -> binary iPop iPop iPush (\a b -> App (BVMul w32 a b))
-    J.Idiv  -> binary iPop iPop iPush
-               (\a b -> App (AddSideCondition (BaseBVRepr w32) (App (BVNonzero w32 b))
-                             "java/lang/ArithmeticException"
-                             (App (BVSdiv w32 a b))))
-    J.Irem -> binary iPop iPop iPush
-               (\a b -> App (AddSideCondition (BaseBVRepr w32) (App (BVNonzero w32 b))
-                             "java/lang/ArithmeticException"
-                             (App (BVSrem w32 a b))))
+    J.Idiv  -> binary iPop iPop iPush (\a b -> nonzero w32 b (App (BVSdiv w32 a b)))
+    J.Irem  -> binary iPop iPop iPush (\a b -> nonzero w32 b (App (BVSrem w32 a b)))
     J.Ineg  -> unaryGen iPop iPush iNeg
     J.Iand  -> binary iPop iPop iPush (\a b -> App (BVAnd w32 a b))
     J.Ior   -> binary iPop iPop iPush (\a b -> App (BVOr  w32 a b))
@@ -761,13 +757,8 @@ generateInstruction (pc, instr) =
     J.Ldiv  -> binary lPop lPop lPush -- TODO: why was this lPush an error?
                -- there is also a special case when when dividend is maxlong
                -- and divisor is -1
-               (\a b -> App (AddSideCondition (BaseBVRepr w64) (App (BVNonzero w64 b))
-                             "java/lang/ArithmeticException"
-                             (App (BVSdiv w64 a b))))
-    J.Lrem -> binary lPop lPop lPush
-               (\a b -> App (AddSideCondition (BaseBVRepr w64) (App (BVNonzero w64 b))
-                             "java/lang/ArithmeticException"
-                             (App (BVSrem w64 a b))))
+               (\a b -> nonzero w64 b (App (BVSdiv w64 a b)))
+    J.Lrem  -> binary lPop lPop lPush (\a b -> nonzero w64 b (App (BVSrem w64 a b)))
     J.Land  -> binary lPop lPop lPush (\a b -> App (BVAnd w64 a b))
     J.Lor   -> binary lPop lPop lPush (\a b -> App (BVOr  w64 a b))
     J.Lxor  -> binary lPop lPop lPush (\a b -> App (BVXor w64 a b))
@@ -1089,6 +1080,18 @@ generateInstruction (pc, instr) =
       do void rPop
     J.Nop ->
       do return ()
+  where nonzero :: (1 <= n)
+                => NatRepr n
+                -> Expr JVM s (BVType n)
+                -> Expr JVM s (BVType n)
+                -> Expr JVM s (BVType n)
+
+        nonzero w b expr =
+          let assertion =
+                JVMAssertionClassifier ["java", "lang", "ArithmeticException"]
+                                       (App (BVNonzero w b))
+              partExpr = PartialExp (W4AT.Leaf assertion) expr
+          in App (WithAssertion (BVRepr w) partExpr)
 
 unary ::
   JVMStmtGen h s ret a ->

crucible-jvm/src/Lang/Crucible/JVM/Types.hs

@@ -6,42 +6,64 @@ License          : BSD3
 Maintainer       : [email protected]
 Stability        : provisional
 -}
+
+{-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE BangPatterns #-}
 
 {-# OPTIONS_GHC -haddock #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 
 module Lang.Crucible.JVM.Types where
 
+import           Prelude hiding (pred)
+
+import           GHC.Generics (Generic)
+import           Data.Typeable (Typeable)
+import           Data.Maybe (isJust)
+import           Data.List (intercalate)
+import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+
 -- jvm-parser
 import qualified Language.JVM.Parser as J
 
 -- parameterized-utils
 import qualified Data.Parameterized.Context as Ctx
 import           Data.Parameterized.Some
+import           Data.Parameterized.ClassesC (TestEqualityC(..), OrdC(..))
+import           Data.Parameterized.TraversableF (FunctorF(..), FoldableF(..), TraversableF(..))
+import qualified Data.Parameterized.TraversableF as TF
+import           Data.Parameterized.Classes (toOrdering)
+import qualified Data.Parameterized.TH.GADT as U
 
 -- crucible
 import qualified Lang.Crucible.CFG.Core as C
 import           Lang.Crucible.CFG.Expr
+import           Lang.Crucible.Simulator.RegValue (RegValue'(unRV))
 import           Lang.Crucible.CFG.Generator
+import qualified Lang.Crucible.CFG.Extension.Safety as Safety
 import           Lang.Crucible.Types
 
 ----------------------------------------------------------------------
@@ -50,11 +72,71 @@ import           Lang.Crucible.Types
 newtype JVM = JVM ()
 type instance ExprExtension JVM = EmptyExprExtension
 type instance StmtExtension JVM = EmptyStmtExtension
-instance IsSyntaxExtension JVM
 
+instance IsSyntaxExtension JVM
 
 type Verbosity = Int
 
+----------------------------------------------------------------------
+-- * Structured assertions
+
+data JVMAssertionClassifier (e :: CrucibleType -> *) =
+  JVMAssertionClassifier { exceptionClass :: [String]
+                           -- ^ Class path of the associated exception
+                         , pred :: e BoolType
+                         }
+  deriving (Generic, Typeable)
+
+type instance Safety.AssertionClassifier JVM = JVMAssertionClassifier
+
+-- -----------------------------------------------------------------------
+-- *** Instances
+
+$(return [])
+
+instance TestEqualityC JVMAssertionClassifier where
+  testEqualityC testSubterm (JVMAssertionClassifier cls1 pred1)
+                            (JVMAssertionClassifier cls2 pred2) =
+    and [ isJust (testSubterm pred1 pred2)
+        , cls1 == cls2
+        ]
+
+instance OrdC JVMAssertionClassifier where
+  compareC subterms sa1 sa2 = toOrdering $
+    $(U.structuralTypeOrd [t|JVMAssertionClassifier|]
+       [ ( U.AnyType `U.TypeApp` U.DataArg 0
+         , [| \x y -> fromOrdering (compareC subterms x y) |]
+         )
+       , ( U.DataArg 0 `U.TypeApp` U.AnyType
+         , [| subterms |]
+         )
+       ]
+     ) sa1 sa2
+
+instance FunctorF JVMAssertionClassifier where
+  fmapF f (JVMAssertionClassifier cls pred_) =
+    JVMAssertionClassifier cls (f pred_)
+
+instance FoldableF JVMAssertionClassifier where
+  foldMapF = TF.foldMapFDefault
+
+instance TraversableF JVMAssertionClassifier where
+  traverseF subterms=
+    $(U.structuralTraversal [t|JVMAssertionClassifier|]
+      [ ( U.AnyType `U.TypeApp` U.DataArg 0
+        , [| \_ -> traverseF subterms |]
+        )
+      , ( U.DataArg 0 `U.TypeApp` U.AnyType
+        , [| \_ -> subterms |]
+        )
+      ]
+     ) subterms
+
+instance Safety.HasStructuredAssertions JVM where
+  explain _proxyExt (JVMAssertionClassifier cls _pred) =
+    text ("Exception of class " ++ intercalate "." cls)
+  toPredicate _proxyExt _sym = pure . unRV . pred
+
 ---------------------------------------------------------------------------------
 -- * Type abbreviations for expressions
 

crucible-llvm/crucible-llvm.cabal

@@ -1,5 +1,5 @@
 Name:          crucible-llvm
-Version:       0.2
+Version:       0.3
 Author:        Galois Inc.
 Copyright:     (c) Galois, Inc 2014-2018
 Maintainer:    [email protected]
@@ -17,8 +17,7 @@ library
     attoparsec,
     bytestring,
     containers >= 0.5.8.0,
-    contravariant >= 1,
-    crucible,
+    crucible >= 0.5,
     what4 >= 0.4.1,
     deepseq,
     directory,
@@ -30,7 +29,6 @@ library
     llvm-pretty >= 0.8 && < 0.11,
     mtl,
     parameterized-utils >= 1.0.4 && < 1.1,
-    template-haskell,
     text,
     transformers,
     unordered-containers,
@@ -42,32 +40,38 @@ library
   exposed-modules:
     Lang.Crucible.LLVM
     Lang.Crucible.LLVM.Arch
-    Lang.Crucible.LLVM.Arch.X86
     Lang.Crucible.LLVM.Arch.Util
+    Lang.Crucible.LLVM.Arch.X86
     Lang.Crucible.LLVM.Bytes
     Lang.Crucible.LLVM.Ctors
     Lang.Crucible.LLVM.DataLayout
     Lang.Crucible.LLVM.Extension
-    Lang.Crucible.LLVM.Intrinsics
+    Lang.Crucible.LLVM.Extension.Safety
+    Lang.Crucible.LLVM.Extension.Safety.Poison
+    Lang.Crucible.LLVM.Extension.Safety.UndefinedBehavior
     Lang.Crucible.LLVM.Globals
+    Lang.Crucible.LLVM.Intrinsics
     Lang.Crucible.LLVM.MemModel
     Lang.Crucible.LLVM.MemType
     Lang.Crucible.LLVM.PrettyPrint
     Lang.Crucible.LLVM.Printf
     Lang.Crucible.LLVM.Translation
     Lang.Crucible.LLVM.TypeContext
-    Lang.Crucible.LLVM.UndefinedBehavior
 
   other-modules:
+    Lang.Crucible.LLVM.Extension.Arch
+    Lang.Crucible.LLVM.Extension.Syntax
+    Lang.Crucible.LLVM.Extension.Safety.Standards
     Lang.Crucible.LLVM.Intrinsics.Common
     Lang.Crucible.LLVM.Intrinsics.Libc
     Lang.Crucible.LLVM.Intrinsics.Libcxx
     Lang.Crucible.LLVM.Intrinsics.LLVM
     Lang.Crucible.LLVM.MemModel.Common
     Lang.Crucible.LLVM.MemModel.Generic
-    Lang.Crucible.LLVM.MemModel.Value
+    Lang.Crucible.LLVM.MemModel.Partial
     Lang.Crucible.LLVM.MemModel.Pointer
     Lang.Crucible.LLVM.MemModel.Type
+    Lang.Crucible.LLVM.MemModel.Value
     Lang.Crucible.LLVM.Translation.Constant
     Lang.Crucible.LLVM.Translation.Expr
     Lang.Crucible.LLVM.Translation.Instruction