what4-1.6.3: Solver-agnostic symbolic values support for issuing queries

Safe Haskell | None
Language | Haskell2010

What4.Protocol.VerilogWriter.AST

Synopsis

- type Identifier = Text
- data Binop (inTp :: BaseType) (outTp :: BaseType) where
  - And :: Binop 'BaseBoolType 'BaseBoolType
  - Or :: Binop 'BaseBoolType 'BaseBoolType
  - Xor :: Binop 'BaseBoolType 'BaseBoolType
  - Eq :: forall (inTp :: BaseType). Binop inTp 'BaseBoolType
  - Ne :: forall (inTp :: BaseType). Binop inTp 'BaseBoolType
  - Lt :: forall (w :: Nat). Binop ('BaseBVType w) 'BaseBoolType
  - Le :: forall (w :: Nat). Binop ('BaseBVType w) 'BaseBoolType
  - BVAnd :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w)
  - BVOr :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w)
  - BVXor :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w)
  - BVAdd :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w)
  - BVSub :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w)
  - BVMul :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w)
  - BVDiv :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w)
  - BVRem :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w)
  - BVPow :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w)
  - BVShiftL :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w)
  - BVShiftR :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w)
  - BVShiftRA :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w)
- binopType :: forall (inTp :: BaseType) (outTp :: BaseType). Binop inTp outTp -> BaseTypeRepr inTp -> BaseTypeRepr outTp
- data Unop (tp :: BaseType) where
  - Not :: Unop 'BaseBoolType
  - BVNot :: forall (w :: Nat). Unop ('BaseBVType w)
- data IExp (tp :: BaseType) where
  - Ident :: forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
- iexpType :: forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
- data LHS
  - = LHS Identifier
  - | LHSBit Identifier Integer
- data Exp (tp :: BaseType) where
  - IExp :: forall (tp :: BaseType). IExp tp -> Exp tp
  - Binop :: forall (inTp :: BaseType) (tp :: BaseType). Binop inTp tp -> IExp inTp -> IExp inTp -> Exp tp
  - Unop :: forall (tp :: BaseType). Unop tp -> IExp tp -> Exp tp
  - BVRotateL :: forall (w :: Nat) (tp :: BaseType). NatRepr w -> IExp tp -> BV w -> Exp tp
  - BVRotateR :: forall (w :: Nat) (tp :: BaseType). NatRepr w -> IExp tp -> BV w -> Exp tp
  - Mux :: forall (tp :: BaseType). IExp BaseBoolType -> IExp tp -> IExp tp -> Exp tp
  - Bit :: forall (w :: Nat). IExp (BaseBVType w) -> Integer -> Exp 'BaseBoolType
  - BitSelect :: forall (len :: Natural) (start :: Natural) (w :: Natural). (1 <= len, (start + len) <= w) => IExp (BaseBVType w) -> NatRepr start -> NatRepr len -> Exp ('BaseBVType len)
  - Concat :: forall (w :: Natural). 1 <= w => NatRepr w -> [Some IExp] -> Exp ('BaseBVType w)
  - BVLit :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> Exp ('BaseBVType w)
  - BoolLit :: Bool -> Exp 'BaseBoolType
- expType :: forall (tp :: BaseType). Exp tp -> BaseTypeRepr tp
- mkLet :: forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
- signed :: forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
- binop :: forall (inTp :: BaseType) (outTp :: BaseType) sym n. Binop inTp outTp -> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
- scalMult :: forall (w :: Natural) sym n. 1 <= w => NatRepr w -> Binop (BaseBVType w) (BaseBVType w) -> BV w -> IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
- data BVConst = BVConst (Pair NatRepr BV)
- litBV :: forall (w :: Natural) sym n. 1 <= w => NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
- litBool :: Bool -> VerilogM sym n (IExp BaseBoolType)
- unop :: forall (tp :: BaseType) sym n. Unop tp -> IExp tp -> VerilogM sym n (IExp tp)
- mux :: forall (tp :: BaseType) sym n. IExp BaseBoolType -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
- bit :: forall (w :: Nat) sym n. IExp (BaseBVType w) -> Integer -> VerilogM sym n (IExp BaseBoolType)
- bitSelect :: forall (len :: Natural) (idx :: Natural) (w :: Natural) sym n. (1 <= len, (idx + len) <= w) => IExp (BaseBVType w) -> NatRepr idx -> NatRepr len -> VerilogM sym n (IExp (BaseBVType len))
- concat2 :: forall (w :: Natural) (w1 :: Natural) (w2 :: Natural) sym n. (w ~ (w1 + w2), 1 <= w) => NatRepr w -> IExp (BaseBVType w1) -> IExp (BaseBVType w2) -> VerilogM sym n (IExp (BaseBVType w))
- data Item where
  - Input :: forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> Item
  - Output :: forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> Item
  - Wire :: forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> Item
  - Assign :: forall (tp :: BaseType). LHS -> Exp tp -> Item
- data ModuleState sym n = ModuleState {
  - vsInputs :: [(Word64, Some BaseTypeRepr, Identifier)]
  - vsOutputs :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
  - vsWires :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
  - vsSeenNonces :: Map Word64 Identifier
  - vsUsedIdentifiers :: Set Identifier
  - vsExpCache :: IdxCache n IExp
  - vsBVCache :: Map BVConst Identifier
  - vsBoolCache :: Map Bool Identifier
  - vsSym :: sym
  }
- newtype VerilogM sym n a = VerilogM (StateT (ModuleState sym n) (ExceptT String IO) a)
- newtype Module sym n = Module (ModuleState sym n)
- mkModule :: sym -> [(Some (Expr n), Text)] -> [VerilogM sym n (Some IExp)] -> ExceptT String IO (Module sym n)
- initModuleState :: sym -> IO (ModuleState sym n)
- runVerilogM :: VerilogM sym n a -> ModuleState sym n -> ExceptT String IO (a, ModuleState sym n)
- execVerilogM :: sym -> VerilogM sym n a -> ExceptT String IO (ModuleState sym n)
- addBoundInput :: forall n (tp :: BaseType) sym. ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier
- addFreshInput :: Some (Nonce n :: k -> Type) -> Some BaseTypeRepr -> Identifier -> VerilogM sym n Identifier
- addOutput :: forall (tp :: BaseType) sym n. BaseTypeRepr tp -> Identifier -> Exp tp -> VerilogM sym n ()
- addWire :: forall (tp :: BaseType) sym n. BaseTypeRepr tp -> Bool -> Identifier -> Exp tp -> VerilogM sym n ()
- freshIdentifier :: Text -> VerilogM sym n Identifier
- addFreshWire :: forall (tp :: BaseType) sym n. BaseTypeRepr tp -> Bool -> Text -> Exp tp -> VerilogM sym n Identifier

# Documentation

type Identifier = Text Source #

data Binop (inTp :: BaseType) (outTp :: BaseType) where Source #

A type for Verilog binary operators that enforces well-typedness, including bitvector size constraints.

Constructors

And :: Binop 'BaseBoolType 'BaseBoolType |
Or :: Binop 'BaseBoolType 'BaseBoolType |
Xor :: Binop 'BaseBoolType 'BaseBoolType |
Eq :: forall (inTp :: BaseType). Binop inTp 'BaseBoolType |
Ne :: forall (inTp :: BaseType). Binop inTp 'BaseBoolType |
Lt :: forall (w :: Nat). Binop ('BaseBVType w) 'BaseBoolType |
Le :: forall (w :: Nat). Binop ('BaseBVType w) 'BaseBoolType |
BVAnd :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w) |
BVOr :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w) |
BVXor :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w) |
BVAdd :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w) |
BVSub :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w) |
BVMul :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w) |
BVDiv :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w) |
BVRem :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w) |
BVPow :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w) |
BVShiftL :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w) |
BVShiftR :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w) |
BVShiftRA :: forall (w :: Nat). Binop ('BaseBVType w) ('BaseBVType w) |

binopType :: forall (inTp :: BaseType) (outTp :: BaseType). Binop inTp outTp -> BaseTypeRepr inTp -> BaseTypeRepr outTp Source #

data Unop (tp :: BaseType) where Source #

A type for Verilog unary operators that enforces well-typedness.

Constructors

Not :: Unop 'BaseBoolType |
BVNot :: forall (w :: Nat). Unop ('BaseBVType w) |

data IExp (tp :: BaseType) where Source #

A type for Verilog expression names that enforces well-typedness. This type exists essentially to pair a name and type to avoid needing to repeat them and ensure that all uses of the name are well-typed.

Constructors

Ident :: forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp |

iexpType :: forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp Source #

data LHS Source #

Constructors

LHS Identifier |
LHSBit Identifier Integer |

data Exp (tp :: BaseType) where Source #

A type for Verilog expressions that enforces well-typedness, including bitvector size constraints.

Constructors

IExp :: forall (tp :: BaseType). IExp tp -> Exp tp |
Binop :: forall (inTp :: BaseType) (tp :: BaseType). Binop inTp tp -> IExp inTp -> IExp inTp -> Exp tp |
Unop :: forall (tp :: BaseType). Unop tp -> IExp tp -> Exp tp |
BVRotateL :: forall (w :: Nat) (tp :: BaseType). NatRepr w -> IExp tp -> BV w -> Exp tp |
BVRotateR :: forall (w :: Nat) (tp :: BaseType). NatRepr w -> IExp tp -> BV w -> Exp tp |
Mux :: forall (tp :: BaseType). IExp BaseBoolType -> IExp tp -> IExp tp -> Exp tp |
Bit :: forall (w :: Nat). IExp (BaseBVType w) -> Integer -> Exp 'BaseBoolType |
BitSelect :: forall (len :: Natural) (start :: Natural) (w :: Natural). (1 <= len, (start + len) <= w) => IExp (BaseBVType w) -> NatRepr start -> NatRepr len -> Exp ('BaseBVType len) |
Concat :: forall (w :: Natural). 1 <= w => NatRepr w -> [Some IExp] -> Exp ('BaseBVType w) |
BVLit :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> Exp ('BaseBVType w) |
BoolLit :: Bool -> Exp 'BaseBoolType |

expType :: forall (tp :: BaseType). Exp tp -> BaseTypeRepr tp Source #

mkLet :: forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp) Source #

Create a let binding, associating a name with an expression. In Verilog, this is a new "wire".

signed :: forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp) Source #

Indicate than an expression name is signed. This causes arithmetic operations involving this name to be interpreted as signed operations.

binop :: forall (inTp :: BaseType) (outTp :: BaseType) sym n. Binop inTp outTp -> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp) Source #

Apply a binary operation to two expressions and bind the result to a new, returned name.

scalMult :: forall (w :: Natural) sym n. 1 <= w => NatRepr w -> Binop (BaseBVType w) (BaseBVType w) -> BV w -> IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w)) Source #

A special binary operation for scalar multiplication. This avoids the need to call `litBV` at every call site.

data BVConst Source #

A wrapper around the BV type allowing it to be put into a map or set. We use this to make sure we generate only one instance of each distinct constant.

Constructors

BVConst (Pair NatRepr BV) |

#### Instances

Instances details

Eq BVConst Source # |
Instance details Defined in What4.Protocol.VerilogWriter.AST Methods (==) :: BVConst -> BVConst -> Bool Source # (/=) :: BVConst -> BVConst -> Bool Source #
Ord BVConst Source # |
Instance details Defined in What4.Protocol.VerilogWriter.AST Methods compare :: BVConst -> BVConst -> Ordering Source # (<) :: BVConst -> BVConst -> Bool Source # (<=) :: BVConst -> BVConst -> Bool Source # (>) :: BVConst -> BVConst -> Bool Source # (>=) :: BVConst -> BVConst -> Bool Source # max :: BVConst -> BVConst -> BVConst Source # min :: BVConst -> BVConst -> BVConst Source #

litBV :: forall (w :: Natural) sym n. 1 <= w => NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w)) Source #

Return the (possibly-cached) name for a literal bitvector value.

litBool :: Bool -> VerilogM sym n (IExp BaseBoolType) Source #

Return the (possibly-cached) name for a literal Boolean value.

unop :: forall (tp :: BaseType) sym n. Unop tp -> IExp tp -> VerilogM sym n (IExp tp) Source #

Apply a unary operation to an expression and bind the result to a new, returned name.

mux :: forall (tp :: BaseType) sym n. IExp BaseBoolType -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp) Source #

Create a conditional, with the given condition, true, and false branches, and bind the result to a new, returned name.

bit :: forall (w :: Nat) sym n. IExp (BaseBVType w) -> Integer -> VerilogM sym n (IExp BaseBoolType) Source #

Extract a single bit from a bit vector and bind the result to a new, returned name.

bitSelect :: forall (len :: Natural) (idx :: Natural) (w :: Natural) sym n. (1 <= len, (idx + len) <= w) => IExp (BaseBVType w) -> NatRepr idx -> NatRepr len -> VerilogM sym n (IExp (BaseBVType len)) Source #

Extract a range of bits from a bit vector and bind the result to a new, returned name. The two `NatRepr` values are the starting index and the number of bits to extract, respectively.

concat2 :: forall (w :: Natural) (w1 :: Natural) (w2 :: Natural) sym n. (w ~ (w1 + w2), 1 <= w) => NatRepr w -> IExp (BaseBVType w1) -> IExp (BaseBVType w2) -> VerilogM sym n (IExp (BaseBVType w)) Source #

Concatenate two bit vectors and bind the result to a new, returned name.

data Item where Source #

A data type for items that may show up in a Verilog module.

Constructors

Input :: forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> Item |
Output :: forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> Item |
Wire :: forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> Item |
Assign :: forall (tp :: BaseType). LHS -> Exp tp -> Item |

data ModuleState sym n Source #

Necessary monadic operations

Constructors

ModuleState |

Fields

- vsInputs :: [(Word64, Some BaseTypeRepr, Identifier)]

  All module inputs, in reverse order. We use Word64 for Nonces to avoid GHC bugs. For more detail: https://gitlab.haskell.org/ghc/ghc/-/issues/2595 https://gitlab.haskell.org/ghc/ghc/-/issues/10856 https://gitlab.haskell.org/ghc/ghc/-/issues/16501

- vsOutputs :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]

  All module outputs, in reverse order. Includes the type, signedness, name, and initializer of each.

- vsWires :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]

  All internal wires, in reverse order. Includes the type, signedness, name, and initializer of each.

- vsSeenNonces :: Map Word64 Identifier

  A map from the identifier nonces seen so far to their identifier names. These nonces exist for identifiers from the original term, but not intermediate Verilog variables.

- vsUsedIdentifiers :: Set Identifier

  A set of all the identifiers used so far, including intermediate Verilog variables.

- vsExpCache :: IdxCache n IExp

  An expression cache to preserve sharing present in the What4 representation.

- vsBVCache :: Map BVConst Identifier

  A cache of bit vector constants, to avoid duplicating constant declarations.

- vsBoolCache :: Map Bool Identifier

  A cache of Boolean constants, to avoid duplicating constant declarations.

- vsSym :: sym

  The What4 symbolic backend to use with `vsBVCache`.

#### Instances

Instances details

MonadState (ModuleState sym n) (VerilogM sym n) Source # |
Instance details Defined in What4.Protocol.VerilogWriter.AST Methods get :: VerilogM sym n (ModuleState sym n) Source # put :: ModuleState sym n -> VerilogM sym n () Source # state :: (ModuleState sym n -> (a, ModuleState sym n)) -> VerilogM sym n a Source #

newtype VerilogM sym n a Source #

Constructors

VerilogM (StateT (ModuleState sym n) (ExceptT String IO) a) |

#### Instances

Instances details

MonadError String (VerilogM sym n) Source # |
Instance details Defined in What4.Protocol.VerilogWriter.AST Methods throwError :: String -> VerilogM sym n a Source # catchError :: VerilogM sym n a -> (String -> VerilogM sym n a) -> VerilogM sym n a Source #
MonadIO (VerilogM sym n) Source # |
Instance details Defined in What4.Protocol.VerilogWriter.AST Methods liftIO :: IO a -> VerilogM sym n a Source #
Applicative (VerilogM sym n) Source # |

Instance details

Defined in What4.Protocol.VerilogWriter.AST

Methods

pure :: a -> VerilogM sym n a Source #

(<*>) :: VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b Source #

liftA2 :: (a -> b -> c) -> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c Source #

(*>) :: VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b Source #

(<*) :: VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a Source #

Functor (VerilogM sym n) Source # |
Instance details Defined in What4.Protocol.VerilogWriter.AST Methods fmap :: (a -> b) -> VerilogM sym n a -> VerilogM sym n b Source # (<$) :: a -> VerilogM sym n b -> VerilogM sym n a Source #
Monad (VerilogM sym n) Source # |
Instance details Defined in What4.Protocol.VerilogWriter.AST Methods (>>=) :: VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b Source # (>>) :: VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b Source # return :: a -> VerilogM sym n a Source #
MonadState (ModuleState sym n) (VerilogM sym n) Source # |
Instance details Defined in What4.Protocol.VerilogWriter.AST Methods get :: VerilogM sym n (ModuleState sym n) Source # put :: ModuleState sym n -> VerilogM sym n () Source # state :: (ModuleState sym n -> (a, ModuleState sym n)) -> VerilogM sym n a Source #

newtype Module sym n Source #

Constructors

Module (ModuleState sym n) |

mkModule :: sym -> [(Some (Expr n), Text)] -> [VerilogM sym n (Some IExp)] -> ExceptT String IO (Module sym n) Source #

Create a Verilog module in the context of a given What4 symbolic backend and a monadic computation that returns an expression name that corresponds to the module's output.

initModuleState :: sym -> IO (ModuleState sym n) Source #

runVerilogM :: VerilogM sym n a -> ModuleState sym n -> ExceptT String IO (a, ModuleState sym n) Source #

execVerilogM :: sym -> VerilogM sym n a -> ExceptT String IO (ModuleState sym n) Source #

addBoundInput :: forall n (tp :: BaseType) sym. ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier Source #

addFreshInput :: Some (Nonce n :: k -> Type) -> Some BaseTypeRepr -> Identifier -> VerilogM sym n Identifier Source #

Returns and records a fresh input with the given type and with a name constructed from the given base.

addOutput :: forall (tp :: BaseType) sym n. BaseTypeRepr tp -> Identifier -> Exp tp -> VerilogM sym n () Source #

Add an output to the current Verilog module state, given a type, a name, and an initializer expression.

addWire :: forall (tp :: BaseType) sym n. BaseTypeRepr tp -> Bool -> Identifier -> Exp tp -> VerilogM sym n () Source #

Add a new wire to the current Verilog module state, given a type, a signedness flag, a name, and an initializer expression.

freshIdentifier :: Text -> VerilogM sym n Identifier Source #

Create a fresh identifier by concatenating the given base with the current fresh identifier counter.

addFreshWire :: forall (tp :: BaseType) sym n. BaseTypeRepr tp -> Bool -> Text -> Exp tp -> VerilogM sym n Identifier Source #

Add a new wire to the current Verilog module state, given a type, a signedness flag, the prefix of a name, and an initializer expression. The name prefix will be freshened by appending current value of the fresh variable counter.