rme-what4 (empty) → 0.1

raw patch · 4 files changed

+480/−0 lines, 4 filesdep +basedep +bv-sizeddep +containers

Dependencies added: base, bv-sized, containers, parameterized-utils, rme, vector, what4

Files

CHANGELOG.md +5/−0
LICENSE +29/−0
rme-what4.cabal +37/−0
src/Data/RME/What4.hs +409/−0

+ CHANGELOG.md view

@@ -0,0 +1,5 @@+# Revision history for rme-what4++## 0.1 -- TBA++* First version.

+ LICENSE view

@@ -0,0 +1,29 @@+Copyright (c) 2025, Galois+++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of the copyright holder nor the names of its+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ rme-what4.cabal view

@@ -0,0 +1,37 @@+cabal-version:      3.0+name:               rme-what4+version:            0.1+synopsis:           What4 adapter for the RME solver+license:            BSD-3-Clause+license-file:       LICENSE+author:             Eric Mertens+maintainer:         emertens@galois.com+build-type:         Simple+extra-doc-files:    CHANGELOG.md+copyright:          2025 Galois+description:+    This package provides an adapter for what4 to support+    solving boolean and bit-vector goals using the RME+    representation.++source-repository head+  type:     git+  location: https://github.com/GaloisInc/rme+  subdir:   rme-what4++common warnings+    ghc-options: -Wall++library+    import:           warnings+    exposed-modules:  Data.RME.What4+    hs-source-dirs:   src+    default-language: Haskell2010+    build-depends:+        base                    ^>= {4.17, 4.18, 4.19, 4.20, 4.21},+        what4                   ^>= 1.7,+        vector                  ^>= 0.13,+        rme                     ^>= 0.1,+        parameterized-utils     ^>= {2.0, 2.1},+        containers              ^>= {0.5, 0.6},+        bv-sized                ^>= 1.0,

+ src/Data/RME/What4.hs view

@@ -0,0 +1,409 @@+{-# Language LambdaCase, GADTs, ImportQualifiedPost, BlockArguments, TypeFamilies, RankNTypes #-}+{-|+Module      : Data.RME.What4+Description : What4 solver adapter for the RME backend.+Copyright   : (c) 2025 Galois+License     : BSD3+Maintainer  : cryptol@galois.com++This module implements a What4 solver adapter that translates What4 expressions+into RME (Reed–Muller expansion) terms and uses the RME backend for+symbolic reasoning.++Reference:+  * https://en.wikipedia.org/wiki/Reed–Muller_expansion++-}+module Data.RME.What4 (rmeAdapter) where++import Control.Monad (replicateM, ap, (<$!>))+import Data.BitVector.Sized qualified as BV+import Data.IntSet (IntSet)+import Data.IntSet qualified as IntSet+import Data.Parameterized.Map qualified as MapF+import Data.Parameterized.NatRepr ( NatRepr(..) )+import Data.Parameterized.Nonce qualified as Nonce+import Data.RME+import Data.Vector qualified as V+import What4.Expr.App qualified as W4+import What4.Expr.BoolMap qualified as W4+import What4.Expr.Builder qualified as W4+import What4.Expr.GroundEval qualified as W4+import What4.Expr.WeightedSum qualified as Sum+import What4.Expr.UnaryBV qualified as UnaryBV+import What4.Interface qualified as W4+import What4.SatResult qualified as W4+import What4.SemiRing qualified as W4+import What4.Solver++rmeAdapter :: SolverAdapter st+rmeAdapter =+  SolverAdapter+  { solver_adapter_name = "RME"+  , solver_adapter_config_options = []+  , solver_adapter_check_sat = rmeAdapterCheckSat+  , solver_adapter_write_smt2 = \_ _ _ -> pure ()+  }++rmeAdapterCheckSat ::+  W4.ExprBuilder t st fs ->+  LogData ->+  [W4.BoolExpr t] ->+  (SatResult (W4.GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) ->+  IO a+rmeAdapterCheckSat _ logger asserts k =+ do logCallback logger "Starting RME"+    let m = foldl conj true <$!> traverse evalExpr asserts+    case runM m of+      Left e ->+       do logCallback logger e+          putStrLn e+          k W4.Unknown+      Right (rme, s) ->+        case sat rme of+          Nothing -> k (W4.Unsat ())+          Just model ->+            let trueVars = IntSet.fromList [i | (i, True) <- model]+            in k (W4.Sat (W4.GroundEvalFn (groundEval trueVars (nonceCache s)), Nothing))++-- | Ground evaluation function. Given a satisfying assignment (set of true variables)+-- this function will used the cached results to evaluate an expression.+groundEval :: IntSet -> MapF.MapF (Nonce.Nonce t) SomeR -> W4.Expr t tp -> IO (W4.GroundValue tp)+groundEval trueVars nonces e =+  let t = W4.exprType e+      ev x = eval x (`IntSet.member` trueVars)+  in+  case flip MapF.lookup nonces =<< W4.exprMaybeId e of+    Just (SomeR n)+      | W4.BaseBoolRepr <- t -> pure $! ev n+      | W4.BaseBVRepr w <- t -> pure $! bitsToBV w (fmap ev n)+    _ -> W4.evalGroundExpr (groundEval trueVars nonces) e++bitsToBV :: Foldable f => NatRepr w -> f Bool -> BV.BV w+bitsToBV w bs = BV.mkBV w (foldl (\acc x -> if x then 1 + acc*2 else acc*2) 0 bs)++newtype M t a = M { unM :: forall k. S t -> (String -> k) -> (a -> S t -> k) -> k }++runM :: M t a -> Either String (a, S t)+runM m = unM m emptyS Left (curry Right)++instance Functor (M t) where+  fmap f (M m) = M (\s e k -> m s e (k . f))++instance Applicative (M t) where+  pure x = M (\s _ k -> k x s)+  (<*>) = ap++instance Monad (M t) where+  M m1 >>= f = M (\s0 e t -> m1 s0 e (\a s1 -> unM (f a) s1 e t))++instance MonadFail (M t) where+  fail str = M (\_ e _ -> e str)++-- | Get the current evaluation state+get :: M t (S t)+get = M (\s _ t -> t s s)++-- | Set the current evaluation state+set :: S t -> M t ()+set s = M (\_ _ t -> t () s)++-- | The state of evaluating an Expr into an RME term+data S t = S+  { nextVar :: !Int -- ^ next fresh variable to be used with RME lit+  , nonceCache :: !(MapF.MapF (Nonce.Nonce t) SomeR) -- ^ previously translated w4 expressions+  }++-- | The initial evaluation state+emptyS :: S t+emptyS = S+  { nextVar = 0+  , nonceCache = MapF.empty+  }++-- | Produce a fresh RME term+freshRME :: M t RME+freshRME =+ do s <- get+    if nextVar s == maxBound then+      fail "Fresh variables exhausted"+    else do+      set $! s{ nextVar = nextVar s + 1 }+      pure (lit (nextVar s))++-- | Map what4 base types to RME representations+type family R (t :: W4.BaseType) where+  R W4.BaseBoolType = RME+  R (W4.BaseBVType n) = RMEV++-- | Newtype wrapper for 'R' type for use with 'MapF'+newtype SomeR tp = SomeR (R tp)++-- | Representation type use to determine which RME representation is being used+data RMERepr (t :: W4.BaseType) where+  -- | A single RME bit+  BitRepr :: RMERepr W4.BaseBoolType+  -- | A vector of w RME bits+  BVRepr  :: !Int -> RMERepr (W4.BaseBVType w)++-- | Helper for memoizing evaluation. Given a nonced and a way to evaluation+-- action this will either return the cached value for that nonce or+-- evaluate the given action and store it in the cache before returning it.+cached :: Nonce.Nonce t tp -> M t (R tp) -> M t (R tp)+cached nonce gen =+ do mb <- fmap (MapF.lookup nonce . nonceCache) get+    case mb of+      Just (SomeR r) -> pure r+      Nothing ->+       do r <- gen+          s <- get+          set s{ nonceCache = MapF.insert nonce (SomeR r) (nonceCache s) }+          pure r++-- | A version of what4's SemiRingRepr that matches the semi-rings that this backend supports+data SemiRingRepr sr where+  SemiRingRepr :: !(W4.BVFlavorRepr fv) -> !Int -> SemiRingRepr (W4.SemiRingBV fv w)++-- | Converts a BV width into the Int type used by Vector.+-- In the extreme case that the NatRepr is out of range of+-- Int, this operation will fail.+evalWidth :: NatRepr w -> M t Int+evalWidth w =+  let n = natValue w in+  if n > fromIntegral (maxBound :: Int)+    then fail "Bit-vector width too wide!"+    else pure (fromIntegral n)++-- | Convert a generic what4 base type to an RME base-type.+-- Reports an error for unsupported base types.+evalTypeRepr :: W4.BaseTypeRepr tp -> M t (RMERepr tp)+evalTypeRepr = \case+  W4.BaseBoolRepr -> pure BitRepr+  W4.BaseBVRepr w ->+   do w' <- evalWidth w+      pure $! BVRepr w'+  r -> fail ("RME does not support " ++ show r)++-- | Convert a generic what4 semiring type to an RME semiring type.+-- Reports an error for unsupported semiring types.+evalSemiRingRepr :: W4.SemiRingRepr sr -> M t (SemiRingRepr sr)+evalSemiRingRepr = \case+      W4.SemiRingIntegerRepr -> fail "RME does not support integers"+      W4.SemiRingRealRepr -> fail "RME does not support real numbers"+      W4.SemiRingBVRepr flv w ->+       do w' <- evalWidth w+          pure $! SemiRingRepr flv w'++-- | Evaluate an expression, if possible, into an RME term.+evalExpr :: W4.Expr t tp -> M t (R tp)+evalExpr = \case+  W4.BoolExpr x _ -> pure $! constant x+  W4.AppExpr x -> cached (W4.appExprId x) (evalApp (W4.appExprApp x))+  W4.BoundVarExpr x -> cached (W4.bvarId x) (allocateVar =<< evalTypeRepr (W4.bvarType x))+  W4.SemiRingLiteral rpr c _ ->+   do SemiRingRepr _ w <- evalSemiRingRepr rpr+      case c of+        BV.BV ci -> pure $! integer w ci+  W4.FloatExpr{} -> fail "RME does not support floating point numbers"+  W4.StringExpr{} -> fail "RME does not support string literals"+  W4.NonceAppExpr{} -> fail "RME does not support quantifiers"++-- | Allocates an unconstrainted RME term at the given type.+allocateVar :: RMERepr tp -> M t (R tp)+allocateVar = \case+  BitRepr -> freshRME+  BVRepr w -> V.fromList <$!> replicateM w freshRME++-- | Convert a what4 App into an RME term for the operations that the+-- RME backend supports.+evalApp :: W4.App (W4.Expr t) tp -> M t (R tp)+evalApp = \case++  W4.BaseEq rpr x y ->+   do x1 <- evalExpr x+      y1 <- evalExpr y+      r <- evalTypeRepr rpr+      pure $! case r of+        BitRepr -> iff x1 y1+        BVRepr{} -> eq x1 y1++  W4.BaseIte rpr _ b t e ->+   do b1 <- evalExpr b+      t1 <- evalExpr t+      e1 <- evalExpr e+      r <- evalTypeRepr rpr+      pure $! case r of+        BitRepr -> mux b1 t1 e1+        BVRepr{} -> V.zipWith (mux b1) t1 e1++  W4.NotPred x ->+   do x1 <- evalExpr x+      pure $! compl x1++  W4.ConjPred c ->+    case W4.viewConjMap c of+      W4.ConjTrue -> pure true+      W4.ConjFalse -> pure false+      W4.Conjuncts y ->+       do let f (x, W4.Positive) = evalExpr x+              f (x, W4.Negative) = compl <$!> evalExpr x+          foldl1 conj <$!> traverse f y++  W4.BVTestBit i ve ->+   do v <- evalExpr ve+      pure $! v V.! (length v - fromIntegral i - 1) -- little-endian index++  W4.BVSlt x y ->+   do x' <- evalExpr x+      y' <- evalExpr y+      pure $! slt x' y'++  W4.BVUlt x y ->+   do x' <- evalExpr x+      y' <- evalExpr y+      pure $! ult x' y'++  W4.BVConcat _ x y ->+   do x' <- evalExpr x+      y' <- evalExpr y+      pure $! x' <> y'++  W4.BVShl _ x y ->+    do x' <- evalExpr x+       y' <- evalExpr y+       pure $! shl x' y'++  W4.BVCountTrailingZeros _ v -> countTrailingZeros <$!> evalExpr v++  W4.BVCountLeadingZeros _ v -> countLeadingZeros <$!> evalExpr v++  W4.BVPopcount _ v -> popcount <$!> evalExpr v++  W4.BVOrBits w s ->+   do vs <- traverse evalExpr (W4.bvOrToList s)+      w' <- evalWidth w+      pure $! foldl (V.zipWith disj) (V.replicate w' false) vs++  W4.BVSelect i n v ->+   do v' <- evalExpr v+      i' <- evalWidth i+      n' <- evalWidth n+      let start = length v' - n' - i' -- i is given as a little endian index+      pure $! V.take n' (V.drop start v')++  W4.BVFill w b ->+   do w' <- evalWidth w+      b' <- evalExpr b+      pure $! V.replicate w' b'++  W4.BVLshr _ x i ->+   do x' <- evalExpr x+      i' <- evalExpr i+      pure $! lshr x' i'++  W4.BVAshr _ x i ->+   do x' <- evalExpr x+      i' <- evalExpr i+      pure $! ashr x' i'++  W4.BVRol _ x i ->+   do x' <- evalExpr x+      i' <- evalExpr i+      pure $! rol x' i'++  W4.BVRor _ x i ->+   do x' <- evalExpr x+      i' <- evalExpr i+      pure $! ror x' i'++  W4.BVZext w v ->+   do v' <- evalExpr v+      w' <- evalWidth w+      let l = w' - length v'+      pure (V.replicate l false <> v')++  W4.BVSext w v ->+   do v' <- evalExpr v+      w' <- evalWidth w+      let l = w' - length v'+      pure (V.replicate l (V.head v') <> v')++  W4.SemiRingSum s ->+   do SemiRingRepr flv w <- evalSemiRingRepr (Sum.sumRepr s)++      case flv of+        -- modular addition+        W4.BVArithRepr ->+          Sum.evalM+            (\x y -> pure $! add x y)+            (\(BV.BV c) r ->+             do v <- evalExpr r+                pure $! mul v (integer w c))+            (\(BV.BV c) -> pure $! integer w c)+            s++        -- bitwise xor+        W4.BVBitsRepr ->+          Sum.evalM+            (\x y -> pure $! V.zipWith xor x y)+            (\(BV.BV c) r ->+             do v <- evalExpr r+                pure $! V.zipWith conj (integer w c) v)+            (\(BV.BV c) -> pure $! integer w c)+            s++  W4.SemiRingProd p ->+   do SemiRingRepr flv w <- evalSemiRingRepr (Sum.prodRepr p)++      case flv of+      -- arithmetic multiplication+        W4.BVArithRepr ->+         do mb <- Sum.prodEvalM+              (\x y -> pure $! mul x y)+              evalExpr+              p+            pure $! case mb of+              Nothing -> integer w 1+              Just r -> r++        -- bitwise conjunction+        W4.BVBitsRepr ->+         do mb <- Sum.prodEvalM+                  (\x y -> pure $! V.zipWith conj x y)+                  evalExpr+                  p+            pure $! case mb of+              Nothing -> V.replicate w true -- ~0+              Just r -> r++  W4.BVUdiv _ x y ->+   do x' <- evalExpr x+      y' <- evalExpr y+      pure $! udiv x' y'++  W4.BVUrem _ x y ->+   do x' <- evalExpr x+      y' <- evalExpr y+      pure $! urem x' y'++  W4.BVSdiv _ x y ->+   do x' <- evalExpr x+      y' <- evalExpr y+      pure $! sdiv x' y'++  W4.BVSrem _ x y ->+   do x' <- evalExpr x+      y' <- evalExpr y+      pure $! srem x' y'++  W4.BVUnaryTerm u ->+   do let constEval x =+           do x' <- evalExpr x+              case isBool x' of+                Nothing -> fail "Unary term not constant"+                Just r -> pure r+      w' <- evalWidth (UnaryBV.width u)+      u' <- UnaryBV.evaluate constEval u+      pure $! integer w' u'++  e -> fail ("RME does not support " ++ show e)