Code

Compositional crux-mir#1117

Code

Merged

spernsteiner merged 35 commits intomasterGaloisInc/saw-script:masterfrom sp/crux-mir-compGaloisInc/saw-script:sp/crux-mir-compCopy head branch name to clipboardApr 26, 2021

+3,474-40

Commits

Commits on Apr 21, 2021

• add crux-mir-comp package

  spernsteiner

  committed
  c37a096

  Copy full SHA for c37a096

• allow customizing sym type in OverrideMatcher

  spernsteiner

  committed
  1eb0f7f

  Copy full SHA for 1eb0f7f

• MethodSpec: allow Pointer type to depend on sym

  spernsteiner

  committed
  6842933

  Copy full SHA for 6842933

• crux-mir-comp: add overrides for MethodSpec API calls

  spernsteiner

  committed
  563420f

  Copy full SHA for 563420f

• crux-mir-comp: implement MethodSpecBuilder API

  spernsteiner

  committed
  bc849d8

  Copy full SHA for bc849d8

• crux-mir: pass MIR CollectionState to overrides

  spernsteiner

  committed
  07929a0

  Copy full SHA for 07929a0

• crux-mir-comp: implement MethodSpecBuilder constructor

  spernsteiner

  committed
  13ef444

  Copy full SHA for 13ef444

• crux-mir-comp: implement MethodSpec API

  spernsteiner

  committed
  26d1662

  Copy full SHA for 26d1662

• crux-mir-comp: implement MethodSpec construction via MethodSpecBuilder finish method

  spernsteiner

  committed
  c25243a

  Copy full SHA for c25243a

• fix executable name: crux-mir -> crux-mir-comp

  spernsteiner

  committed
  a7b8c15

  Copy full SHA for a7b8c15

• crucible bump to fix errors building MethodSpec{,Builder} structs

  spernsteiner

  committed
  e268d8a

  Copy full SHA for e268d8a

• finish incomplete update to new saw-core-what4 APIs

  spernsteiner

  committed
  86d38a2

  Copy full SHA for 86d38a2

• add simple tests for compositional reasoning

  spernsteiner

  committed
  0c90161

  Copy full SHA for 0c90161

• implement clobbering of UnsafeCell contents behind immutable refs

  spernsteiner

  committed
  a2249b3

  Copy full SHA for a2249b3

• remove duplicate copy of visitRegValueExprs

  spernsteiner

  committed
  e7622b4

  Copy full SHA for e7622b4

• bump crucible for crux-mir test fixes

  spernsteiner

  committed
  e9b6307

  Copy full SHA for e9b6307

• move clobberSymbolic and related functions into a separate module

  spernsteiner

  committed
  4e67674

  Copy full SHA for 4e67674

• implement clobber_globals intrinsic

  spernsteiner

  committed
  070c27e

  Copy full SHA for 070c27e

• clobber globals when running a methodspec override

  spernsteiner

  committed
  36224fd

  Copy full SHA for 36224fd

• add test case for clobber_globals behavior

  spernsteiner

  committed
  1d64a7c

  Copy full SHA for 1d64a7c

• fix warnings

  spernsteiner

  committed
  4872930

  Copy full SHA for 4872930

• add clobber_globals calls to existing spec_*.rs tests

  spernsteiner

  committed
  d0ecfd2

  Copy full SHA for d0ecfd2

• check that all vars and allocs are bound in methodspec override call

  spernsteiner

  committed
  5aab1b8

  Copy full SHA for 5aab1b8

• check disjointness of refs when running methodspec override

  spernsteiner

  committed
  09df51c

  Copy full SHA for 09df51c

• add test cases for reference aliasing/overlap

  spernsteiner

  committed
  02837d9

  Copy full SHA for 02837d9

• add a test to ensure each test can choose its overrides independently

  spernsteiner

  committed
  b2e4015

  Copy full SHA for b2e4015

• refactor: use datatypes instead of tuple/Pair for AllocSpec & Pointer'

  spernsteiner

  committed
  4f59470

  Copy full SHA for 4f59470

• refactor: use datatype instead of tuple for allocs found during addArg

  spernsteiner

  committed
  37c0601

  Copy full SHA for 37c0601

Commits on Apr 26, 2021

• crux-mir-comp: Builder: record the dereferenceable region around each pointer

  spernsteiner

  committed
  369cb21

  Copy full SHA for 369cb21

• make OverrideMatcher' generic over the underlying monad

  spernsteiner

  committed
  e73bc9c

  Copy full SHA for e73bc9c

• crux-mir-comp: Override: check dereferenceable region around each pointer

  spernsteiner

  committed
  6f5ebdf

  Copy full SHA for 6f5ebdf

• crux-mir-comp: allow multiple array elements in PointsTo

  spernsteiner

  committed
  6d8e601

  Copy full SHA for 6d8e601

• crux-mir-comp: add DESIGN.md

  spernsteiner

  committed
  2853a5a

  Copy full SHA for 2853a5a

• remove outdated comment

  spernsteiner

  committed
  1342765

  Copy full SHA for 1342765

• Merge branch 'master' into sp/crux-mir-comp

  spernsteiner

  committed
  5806e0c

  Copy full SHA for 5806e0c