symbolic-syntax: Remove fresh-vec

It's not part of the Macaw syntax, but rather an operation that's useful when hand-writing CFGs. This should instead be supported by parser extensions downstream.
2024-11-25 21:54:51 +03:00 · 2023-11-02 16:39:22 -04:00 · 2023-11-02 16:39:22 -04:00 · 0b9c4730d8
commit 0b9c4730d8
parent 8be115c859
5 changed files with 36 additions and 134 deletions
--- a/symbolic-syntax/README.md
+++ b/symbolic-syntax/README.md
@ -28,7 +28,6 @@ There are a few wrappers around `Bitvector` types for portability and convenienc
 The extra operations are:

 - `bv-typed-literal :: Type -> Integer -> Bitvector w` where the first argument is a `Bitvector` type alias (see the Types section), the second argument is the value the `Bitvector` should contain, and `w` is the number of bits in the returned `Bitvector` (will match the width of the `Type` argument). This is useful because `(bv <width> ...)` only works when you know the exact value of width as a numeral, and types like `SizeT` map to different widths depending on your architecture.
- `fresh-vec :: String Unicode -> forall (t :: Type) -> Nat -> Vector t`, where `(fresh-vec s t n)` generates a length-`n` vector where each element is a fresh constant of type `t` with the name `<s>_<i>` (for each `i` between `0` and `<n> - 1`). Note that `t` must be a scalar type (e.g., no nested `Vector`\ s), and `s` and `n` must both be concrete values.
 - `pointer-make-null :: Pointer` returns a null pointer.
 - `pointer-add :: Pointer -> Bitvector w -> Pointer` where `w` is the number of bits in a pointer (usually 32 or 64).
 - `pointer-diff :: Pointer -> Pointer -> Bitvector w` where `w` is the number of bits in a pointer (usually 32 or 64).
--- a/symbolic-syntax/src/Data/Macaw/Symbolic/Syntax.hs
+++ b/symbolic-syntax/src/Data/Macaw/Symbolic/Syntax.hs
@ -31,10 +31,7 @@ import qualified Data.Map.Strict as Map
 import qualified Data.Parameterized.Context as Ctx
 import qualified Data.Parameterized.NatRepr as PN
 import           Data.Parameterized.Some ( Some(..) )
-import qualified Data.Text as DT
-import qualified Data.Vector as DV
 import           GHC.TypeNats ( KnownNat, type (<=) )
-import           Numeric.Natural ( Natural )

 import qualified Data.Macaw.CFG as DMC
 import qualified Data.Macaw.Memory as DMM
@ -207,15 +204,6 @@ extensionParser wrappers hooks =
            LCT.BVRepr{} ->
              go (SomeExtensionWrapper (buildBvTypedLitWrapper tp))
            _ -> empty
-      LCSA.AtomName "fresh-vec" -> do
-        -- Generating fresh vectors are a special case. We must parse the
-        -- name and length arguments separately due to their need to be
-        -- concrete, and we must parse the type argument separately before we
-        -- can know the return type.
-        LCSE.depCons LCSC.string $ \nmPrefix ->
-          LCSE.depCons LCSC.isType $ \(Some tp) ->
-            LCSE.depCons LCSC.nat $ \len ->
-            go (SomeExtensionWrapper (buildFreshVecWrapper nmPrefix tp len))
      _ ->
        case Map.lookup name wrappers of
          Nothing -> empty
@ -518,56 +506,6 @@ bvTypedLit :: forall s ext w m
          -> m (LCCR.AtomValue ext s (LCT.BVType w))
 bvTypedLit (LCT.BVRepr w) val = return (LCCR.EvalApp (LCE.IntegerToBV w val))

-- | Wrapper for generating a vector of the given length, where each element is
-- a fresh constant of the supplied type whose name is derived from the given
-- string. This is a convenience for users who wish to quickly generate
-- symbolic data (e.g., for use with @write-bytes@).
--
-- > fresh-vec string type integer
-buildFreshVecWrapper ::
-     DT.Text
-  -> LCT.TypeRepr tp
-  -> Natural
-  -> ExtensionWrapper arch
-                      Ctx.EmptyCtx
-                      (LCT.VectorType tp)
-buildFreshVecWrapper nmPrefix tp len = ExtensionWrapper
-  { extName = LCSA.AtomName "fresh-vec"
-  , extArgTypes = Ctx.empty
-  , extWrapper = \_ -> freshVec nmPrefix tp len }
-
-- | Generate a vector of the given length, where each element is a fresh
-- constant of the supplied type whose name is derived from the given string.
-freshVec :: forall s ext tp m.
-            ExtensionParser m ext s
-         => DT.Text
-         -> LCT.TypeRepr tp
-         -> Natural
-         -> m (LCCR.AtomValue ext s (LCT.VectorType tp))
-freshVec nmPrefix tp len = do
-  case tp of
-    LCT.FloatRepr fi ->
-      mkVec (LCCR.FreshFloat fi)
-    LCT.NatRepr ->
-      mkVec LCCR.FreshNat
-    _ | LCT.AsBaseType bt <- LCT.asBaseType tp ->
-          mkVec (LCCR.FreshConstant bt)
-      | otherwise ->
-          empty
-  where
-    -- Construct an expression that looks roughly like:
-    --
-    --   (vector <tp> (fresh <s>_0) ... (fresh <s>_<n-1>))
-    --
-    -- Where the implementation of `fresh` is determined by the first argument.
-    mkVec :: (Maybe WI.SolverSymbol -> LCCR.AtomValue ext s tp)
-          -> m (LCCR.AtomValue ext s (LCT.VectorType tp))
-    mkVec mkFresh = do
-      vec <- DV.generateM (fromIntegral len) $ \i ->
-        LCSC.freshAtom WP.InternalPos $ mkFresh $ Just $ WI.safeSymbol $
-        DT.unpack nmPrefix ++ "_" ++ show i
-      pure $ LCCR.EvalApp $ LCE.VectorLit tp vec
-
 -- | Syntax extension wrappers
 extensionWrappers
  :: (w ~ DMC.ArchAddrWidth arch, 1 <= w, KnownNat w, DMC.MemWidth w)
--- a/symbolic-syntax/test-data/ops.cbl
+++ b/symbolic-syntax/test-data/ops.cbl
@ -2,7 +2,6 @@
 (defun @ops ((p Pointer) (q Pointer)) Unit
  (start start:
    (let b (bv-typed-literal SizeT 42))
-    (let v (fresh-vec "v" Short 7))
    (let n (pointer-make-null))
    (let d (pointer-diff p q))
    (let r (pointer-add p d))
--- a/symbolic-syntax/test-data/ops.out
+++ b/symbolic-syntax/test-data/ops.out
@ -1,7 +1,6 @@
 (defun @ops ((p Pointer) (q Pointer)) Unit
   (start start:
      (let b (bv-typed-literal SizeT 42))
-      (let v (fresh-vec "v" Short 7))
      (let n (pointer-make-null))
      (let d (pointer-diff p q))
      (let r (pointer-add p d))
@ -17,46 +16,30 @@ ops
  $2 = intLit(42)
  % 4:12
  $3 = integerToBV(64, $2)
-  % internal
-  $4 = fresh BaseBVRepr 16 v_0
-  % internal
-  $5 = fresh BaseBVRepr 16 v_1
-  % internal
-  $6 = fresh BaseBVRepr 16 v_2
-  % internal
-  $7 = fresh BaseBVRepr 16 v_3
-  % internal
-  $8 = fresh BaseBVRepr 16 v_4
-  % internal
-  $9 = fresh BaseBVRepr 16 v_5
-  % internal
-  $10 = fresh BaseBVRepr 16 v_6
  % 5:12
-  $11 = vectorLit(BVRepr 16, [$4, $5, $6, $7, $8, $9, $10])
+  $4 = extensionApp(null_ptr)
+  % internal
+  $5 = (ptr_sub $0 $1)
  % 6:12
-  $12 = extensionApp(null_ptr)
+  $6 = extensionApp((ptr_to_bits_64 $5))
  % internal
-  $13 = (ptr_sub $0 $1)
+  $7 = extensionApp((bits_to_ptr_64 $6))
  % 7:12
-  $14 = extensionApp((ptr_to_bits_64 $13))
-  % internal
-  $15 = extensionApp((bits_to_ptr_64 $14))
-  % 8:12
-  $16 = (ptr_add $0 $15)
+  $8 = (ptr_add $0 $7)
+  % 8:16
+  $9 = (ptr_sub $8 $7)
  % 9:16
-  $17 = (ptr_sub $16 $15)
-  % 10:16
-  $18 = (ptr_eq $17 $0)
+  $10 = (ptr_eq $9 $0)
  % internal
-  $19 = (macawReadMem bvle4 $17)
-  % 11:12
-  $20 = extensionApp((ptr_to_bits_32 $19))
+  $11 = (macawReadMem bvle4 $9)
+  % 10:12
+  $12 = extensionApp((ptr_to_bits_32 $11))
  % internal
-  $21 = extensionApp((bits_to_ptr_64 $3))
+  $13 = extensionApp((bits_to_ptr_64 $3))
+  % 11:5
+  $14 = (macawWriteMem bvle8 $9 $13)
+  % 12:13
+  $15 = emptyApp()
  % 12:5
-  $22 = (macawWriteMem bvle8 $17 $21)
-  % 13:13
-  $23 = emptyApp()
-  % 13:5
-  return $23
+  return $15
  % no postdom
--- a/symbolic-syntax/test-data/ops.out.good
+++ b/symbolic-syntax/test-data/ops.out.good
@ -1,7 +1,6 @@
 (defun @ops ((p Pointer) (q Pointer)) Unit
   (start start:
      (let b (bv-typed-literal SizeT 42))
-      (let v (fresh-vec "v" Short 7))
      (let n (pointer-make-null))
      (let d (pointer-diff p q))
      (let r (pointer-add p d))
@ -17,46 +16,30 @@ ops
  $2 = intLit(42)
  % 4:12
  $3 = integerToBV(64, $2)
-  % internal
-  $4 = fresh BaseBVRepr 16 v_0
-  % internal
-  $5 = fresh BaseBVRepr 16 v_1
-  % internal
-  $6 = fresh BaseBVRepr 16 v_2
-  % internal
-  $7 = fresh BaseBVRepr 16 v_3
-  % internal
-  $8 = fresh BaseBVRepr 16 v_4
-  % internal
-  $9 = fresh BaseBVRepr 16 v_5
-  % internal
-  $10 = fresh BaseBVRepr 16 v_6
  % 5:12
-  $11 = vectorLit(BVRepr 16, [$4, $5, $6, $7, $8, $9, $10])
+  $4 = extensionApp(null_ptr)
+  % internal
+  $5 = (ptr_sub $0 $1)
  % 6:12
-  $12 = extensionApp(null_ptr)
+  $6 = extensionApp((ptr_to_bits_64 $5))
  % internal
-  $13 = (ptr_sub $0 $1)
+  $7 = extensionApp((bits_to_ptr_64 $6))
  % 7:12
-  $14 = extensionApp((ptr_to_bits_64 $13))
-  % internal
-  $15 = extensionApp((bits_to_ptr_64 $14))
-  % 8:12
-  $16 = (ptr_add $0 $15)
+  $8 = (ptr_add $0 $7)
+  % 8:16
+  $9 = (ptr_sub $8 $7)
  % 9:16
-  $17 = (ptr_sub $16 $15)
-  % 10:16
-  $18 = (ptr_eq $17 $0)
+  $10 = (ptr_eq $9 $0)
  % internal
-  $19 = (macawReadMem bvle4 $17)
-  % 11:12
-  $20 = extensionApp((ptr_to_bits_32 $19))
+  $11 = (macawReadMem bvle4 $9)
+  % 10:12
+  $12 = extensionApp((ptr_to_bits_32 $11))
  % internal
-  $21 = extensionApp((bits_to_ptr_64 $3))
+  $13 = extensionApp((bits_to_ptr_64 $3))
+  % 11:5
+  $14 = (macawWriteMem bvle8 $9 $13)
+  % 12:13
+  $15 = emptyApp()
  % 12:5
-  $22 = (macawWriteMem bvle8 $17 $21)
-  % 13:13
-  $23 = emptyApp()
-  % 13:5
-  return $23
+  return $15
  % no postdom