crucible 0.8.0.0 → 0.9

raw patch · 3 files changed

+120/−1 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

CHANGELOG.md +2/−0
crucible.cabal +5/−1
src/Lang/Crucible/README.hs +113/−0

CHANGELOG.md view

@@ -1,3 +1,5 @@+# 0.9 -- 2026-01-29+ # 0.8.0 -- 2025-11-09  * Add `setExecResultContext`, `setExecStateContext`

crucible.cabal view

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crucible-Version:       0.8.0.0+Version:       0.9 Author:        Galois Inc. Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com Copyright:     (c) Galois, Inc 2014-2022@@ -14,6 +14,9 @@   (SSA) form control flow graphs, and a symbolic simulation engine for executing   programs expressed in this format.  It also provides support for communicating with   a variety of SAT and SMT solvers, including Z3, CVC4, Yices, STP, and dReal.+  .+  For an overview of Crucible please have a look at "Lang.Crucible.README"+   extra-doc-files: CHANGELOG.md  source-repository head@@ -101,6 +104,7 @@     Lang.Crucible.CFG.SSAConversion     Lang.Crucible.CFG.EarlyMergeLoops     Lang.Crucible.FunctionHandle+    Lang.Crucible.README     Lang.Crucible.Simulator     Lang.Crucible.Simulator.Breakpoint     Lang.Crucible.Simulator.BoundedExec

+ src/Lang/Crucible/README.hs view

@@ -0,0 +1,113 @@+{- | This module is only for documentation purposes, and provides a high+level overview of Crucible aimed at developers. -}+{-# OPTIONS_GHC -Wno-unused-imports #-}+module Lang.Crucible.README where++import What4.Interface+import What4.Expr.App+import What4.BaseTypes+import Lang.Crucible.Backend++import Lang.Crucible.Types+import Lang.Crucible.CFG.Expr+import Lang.Crucible.CFG.Core hiding (Expr)+import Lang.Crucible.CFG.SSAConversion++import Lang.Crucible.Simulator.RegValue+import Lang.Crucible.Simulator.RegMap+import Lang.Crucible.Simulator.ExecutionTree+import Lang.Crucible.Simulator.EvalStmt+import Lang.Crucible.Simulator.Evaluation+import Lang.Crucible.Simulator.Intrinsics++++-- * Crucible Types++{- $+The types of the Crucible language are defined in "Lang.Crucible.Types".+Types are encoded using [singletons](https://github.com/Galoisinc/parameterized-utils?tab=readme-ov-file#parameterized-types-motivation):++* 'CrucibleType' is the Haskell type-level description of all Crucible types+* 'TypeRepr' are the associated value-level singletons, which+  are used when we pass around types, or store them in data structures.+-}++-- * Crucible Values++{- $+The inhabitants of each type are specified via the type function 'RegValue'.+We also have 'RegValue'' which is just a @newtype@ wrapper around 'RegValue',+because in Haskell type families may not be partially applied but @newtype@s can.++An important subset of the Crucible types are the base types (see 'BaseToType'),+which is for the symbolic expression we can construct+(see 'SymExpr' in [what4](https://github.com/Galoisinc/what4)).+Only these types may contain variables. In practice, we always use @what4@'s+'Expr' type to represent symbolic expressions.++Also, in some cases we use 'RegEntry' which+is just a pair of a 'RegValue' and its associated 'TypeRepr'.++There's also 'BaseTerm', which is similar to 'RegEntry' but+for base types---it contains a @what4@'s 'BaseTypeRepr' and a value of the corresponding+base type (usually;  the type is parameterized on exactly what we package+with the type).+-}+  +-- * Crucible Programs+  +{- $+The program executed by the simulator is in the form of a control flow+graph (CFG).  A typical way to construct them is as follows:++  1. use the functions in "Lang.Crucible.CFG.Generator" to produce a CFG with +     assignments ("Lang.Crucible.CFG.Reg")+  2. use 'toSSA' to translate this to a CFG without assignments+     ("Lang.Crucible.CFG.Core")++The core 'CFG' contains basic blocks with 'Stmt's and terminated+by 'TermStmt'.  The expression language for the core 'Core.CFG' is+the type 'App'.+-}+  +-- * Symbolic Simulator+  +{- $+The state of a running simulator is described in "Lang.Crucible.Simulator.ExecutionTree":++  * 'ExecState' is the current state of execution.+     We start with 'InitialState', and keep performing steps until we get+     to a 'ResultState'.+  * As the simulator executes, it keeps track of its state in 'SimState',+    which is stored in the current `ExecState`.+  * 'SimContext' is the part of the state that persists across branches+    (e.g, after we explore the @then@ part of an @if@ statement, we'll+    roll back some of the state changes before simulating the @else@ part,+    but the data in 'SimContext's persists).  An important part of the+    'SimContext' is the simulator's backend ('_ctxBackend'), which is how the+    simulator communicates with a solver, and builds symbolic expressions+    ('IsSymBackend').+++To evaluate a 'CFG' we evaluate the statements as described in+"Lang.Crucible.Simulator.EvalStmt" (details in 'stepStmt', 'stepTerm').+Details about expressions evaluation are in 'evalApp' in "Lang.Crucible.Simulator.Evaluation".++A lot of useful functionality relevant to the simulator can be accessed+from module "Lang.Crucible.Simulator".++The simulator supports mutable global variables.  Our tools use one such+global to store a language specific memory model, which records information+about various memory operations.+-}++-- * Intrinsics++{- $++Crucible type may be extended using 'IntrinsicType's.  An intrinsic type is+a type-level string, which can be given meaning by making an instance of+'IntrinsicClass'.+-}+