Code

Compositional crux-mir support#659

Code

Merged

spernsteiner merged 19 commits intomasterGaloisInc/crucible:masterfrom sp/crux-mir-compGaloisInc/crucible:sp/crux-mir-compCopy head branch name to clipboardApr 21, 2021

+632-58

Commits

Commits on Apr 15, 2021

• crux-mir.cabal: move all module into exposed-modules

  spernsteiner

  committed
  efffd2e

• crux-mir: add mainWithExtraOverrides entry point

  spernsteiner

  committed
  bbc792c

• crux-mir: add MethodSpec and MethodSpecBuilder intrinsics

  spernsteiner

  committed
  a5ec4eb

• crux-mir: TransTy: add isUnsized

  spernsteiner

  committed
  57dcde9

• crux-mir: add functions for manipulating MirRefs within IO/OverrideSim monad

  spernsteiner

  committed
  ccc62d9

• crux-mir: add mirRef_eqIO

  spernsteiner

  committed
  8b10cfc

• crux-mir: pass MIR CollectionState to overrides

  spernsteiner

  committed
  259e086

• crux-mir: add _Wrapped lens for Substs

  spernsteiner

  committed
  25bab3f

• crux-mir: expose sym ~ W4.ExprBuilder ... constraint in BindExtraOverridesFn

  spernsteiner

  committed
  619b365

• add mirFail stubs for construction of MethodSpec{,Builder}

  spernsteiner

  committed
  4f42945

• let test suites override the default mir-json -L search path

  spernsteiner

  committed
  46aa87f

• crux-mir: add CTyUnsafeCell pattern

  spernsteiner

  committed
  607c33c

• update golden test files for line number change

  spernsteiner

  committed
  f23e141

• crux-mir: add crucible::method_spec::clobber_globals function

  spernsteiner

  committed
  529f038

• Mir.Intrinsics: add mirRef_overlaps

  spernsteiner

  committed
  42f151e

• minor improvements to mirRef_overlaps

  spernsteiner

  committed
  d29d5aa

• more doc comments explaining the crux-mir/crux-mir-comp split

  spernsteiner

  committed
  155fa0f

• add mirRef_indexAndLenSim

  spernsteiner

  committed
  44c8aeb

Commits on Apr 21, 2021

• don't require Crux.Model personality for mirRef_indexAndLenSim

  spernsteiner

  committed
  c6b5472