Code

Heapster Array Prover Redux#1617

Code

Merged

eddywestbrook merged 30 commits intomasterGaloisInc/saw-script:masterfrom array-proverGaloisInc/saw-script:array-proverCopy head branch name to clipboardMar 28, 2022

+675-164

Commits

Commits on Mar 24, 2022

• WIP checkin, basic cases of array prover rewrite working.

  abakst

  committed
  9cb7e4d

  Copy full SHA for 9cb7e4d

• Add unit tests for implication prover

  abakst

  committed
  46debc3

  Copy full SHA for 46debc3

• WIP checkin - array implication prover

  abakst

  committed
  60c7438

  Copy full SHA for 60c7438

• Fix bug in skeletonArray range gathering

  abakst

  committed
  51649d3

  Copy full SHA for 51649d3

• Reorg test main

  abakst

  committed
  fa5a209

  Copy full SHA for fa5a209

• Add some symbolic tests

  abakst

  committed
  63377f7

  Copy full SHA for 63377f7

• Add some tests over fields

  abakst

  committed
  2bcc587

  Copy full SHA for 2bcc587

• goo begone

  abakst

  committed
  bd3f363

  Copy full SHA for bd3f363

• Some clean up of array reimplementation

  abakst

  committed
  c87ac9d

  Copy full SHA for c87ac9d

• clean up array prover impl

  abakst

  committed
  bd0f660

  Copy full SHA for bd0f660

• more testing

  abakst

  committed
  9f23f02

  Copy full SHA for 9f23f02

• Revert changed examples

  abakst

  committed
  8fc06f9

  Copy full SHA for 8fc06f9

• Add comment to last successful case of proveVarLLVMArrayH

  abakst

  committed
  fa39897

  Copy full SHA for fa39897

• Revert _CoqProject changes

  abakst

  committed
  8f6edcf

  Copy full SHA for 8f6edcf

• Revert arrays.saw changes

  abakst

  committed
  e9a1a2a

  Copy full SHA for e9a1a2a

• WIP checkin, bug fix

  abakst

  committed
  bf5945e

  Copy full SHA for bf5945e

• Finish cleanup

  abakst

  committed
  657282e

  Copy full SHA for 657282e

• Refactor proveSomeBlockM

  abakst

  committed
  fa2cdeb

  Copy full SHA for fa2cdeb

• Refactor gatherRangesForArray

  abakst

  committed
  fe46a41

  Copy full SHA for fe46a41

• Better docs on SImpl_LLVMArrayBorrowed.

  abakst

  committed
  72825cf

  Copy full SHA for 72825cf

• Fix errors in refactor

  abakst

  committed
  d54a799

  Copy full SHA for d54a799

• Eliminate array-shaped blocks in proveVarLLVMArrayH.

  abakst

  committed
  6217b34

  Copy full SHA for 6217b34

• Check totally-borrowed side condition of SImpl_LLVMArrayBorrowed in simplImplIn.

  abakst

  committed
  3876eda

  Copy full SHA for 3876eda

• Make llvmAtomicPermCouldOverlapRange docs more precise

  abakst

  committed
  232e92a

  Copy full SHA for 232e92a

• Missing haddocks

  abakst

  committed
  7ded6f3

  Copy full SHA for 7ded6f3

• Remove commented-out code

  abakst

  committed
  a415019

  Copy full SHA for a415019

• Remove unused function.

  abakst

  committed
  590265a

  Copy full SHA for 590265a

• Don't throw away rhs borrows.

  abakst

  committed
  1f9375f

  Copy full SHA for 1f9375f

Commits on Mar 25, 2022

• Don't depend on ordering when checking an array is completely borrowed

  abakst

  committed
  2e4c48c

  Copy full SHA for 2e4c48c

Commits on Mar 28, 2022

• Merge branch 'master' into array-prover

  

  Eddy Westbrook

  authored
  7e6b6a8

  Copy full SHA for 7e6b6a8