Code

Structured assertions#151

Code

Merged

robdockins merged 60 commits intoGaloisInc:masterGaloisInc/crucible:masterfrom langston-barrett:partllvmval-rebasedlangston-barrett/crucible:partllvmval-rebasedCopy head branch name to clipboardMar 4, 2019

+3,764-1,847

Commits

Commits on Jan 30, 2019

• [WIP]: PartLLVMVal refactor

  langston-barrett

  committed
  672ffee

  Copy full SHA for 672ffee

• [WIP] More partial value refactor: the code compiles! (readMemSet')

  langston-barrett

  committed
  d783edf

  Copy full SHA for d783edf

• [WIP] all readMem* functions

  langston-barrett

  committed
  a84e130

  Copy full SHA for a84e130

• Simplifying and pretty-printing PartLLVMVal'

  langston-barrett

  committed
  0dd76bb

  Copy full SHA for 0dd76bb

• Start putting stuff in Crucible and What4

  langston-barrett

  committed
  887d434

  Copy full SHA for 887d434

• HasSafetyAssertions

  langston-barrett

  committed
  67a9979

  Copy full SHA for 67a9979

• Start folding in new Crucible SafetyAssertion stuff in crucible-llvm

  langston-barrett

  committed
  4a7e188

  Copy full SHA for 4a7e188

• Hold structured, relevant information in UB and Poison constructors

  langston-barrett

  committed
  395dddb

  Copy full SHA for 395dddb

• remove old-style partllvmval functions

  langston-barrett

  committed
  621e23b

  Copy full SHA for 621e23b

• a few more operations

  langston-barrett

  committed
  97e2741

  Copy full SHA for 97e2741

• what4: add second type parameter to AssertionTree

  langston-barrett

  committed
  21be286

  Copy full SHA for 21be286

• No more type errors in MemModel.Generic

  langston-barrett

  committed
  88f604c

  Copy full SHA for 88f604c

• fewer type errors in MemModel.hs

  langston-barrett

  committed
  f49ef41

  Copy full SHA for f49ef41

• Add appropriate arguments to Poison constructors

  langston-barrett

  committed
  e53cf2d

  Copy full SHA for e53cf2d

• [WIP]

  langston-barrett

  committed
  f14732c

  Copy full SHA for f14732c

• Fix rebase mistakes

  langston-barrett

  committed
  626b882

  Copy full SHA for 626b882

Commits on Jan 31, 2019

• Complete implementation of SafetyAssertion family in Crucible

  langston-barrett

  committed
  eef5c75

  Copy full SHA for eef5c75

• crucible: More specific imports

  langston-barrett

  committed
  329f110

  Copy full SHA for 329f110

• remove accidentally-committed files

  langston-barrett

  committed
  e433311

  Copy full SHA for e433311

• Progress on porting crucible-llvm to structured assertions

  langston-barrett

  committed
  c2248a0

  Copy full SHA for c2248a0

Commits on Feb 1, 2019

• explainTree and assertSafe

  langston-barrett

  committed
  d9eda84

  Copy full SHA for d9eda84

• testequality bug

  langston-barrett

  committed
  6ccc738

  Copy full SHA for 6ccc738

Commits on Feb 2, 2019

• OrdF -> OrdC

  langston-barrett

  committed
  8504882

  Copy full SHA for 8504882

• instance TestEqualityC Poison

  langston-barrett

  committed
  40b24b3

  Copy full SHA for 40b24b3

Commits on Feb 4, 2019

• change kind of SafetyAssertion

  langston-barrett

  committed
  a4b1b46

  Copy full SHA for a4b1b46

• Finish changing the kind of SafetyAssertion

  langston-barrett

  committed
  3230581

  Copy full SHA for 3230581

• Approach based on AssertionClassifier and PartialExpr

  langston-barrett

  committed
  7ce2c12

  Copy full SHA for 7ce2c12

Commits on Feb 5, 2019

• Use *C classes again, port crucible-llvm to new stuff

  langston-barrett

  committed
  4d907a5

  Copy full SHA for 4d907a5

• progress on aspects of crucible-llvm

  langston-barrett

  committed
  b665ecd

  Copy full SHA for b665ecd

• Finish up Instruction

  langston-barrett

  committed
  6994e6a

  Copy full SHA for 6994e6a

• AssertionTree instances: Eq1, Eq2, .., Ord2, Bifunctor, Bitraversable

  langston-barrett

  committed
  a805739

  Copy full SHA for a805739

Commits on Feb 6, 2019

• some Template Haskell *(F|C) instances

  langston-barrett

  committed
  ac69598

  Copy full SHA for ac69598

• even more TH instances

  langston-barrett

  committed
  98812eb

  Copy full SHA for 98812eb

• evaluation of withassertion

  langston-barrett

  committed
  fc77f59

  Copy full SHA for fc77f59

• Complete OrdFC instance for PartialExpr

  langston-barrett

  committed
  98b12c1

  Copy full SHA for 98b12c1

• llvm HasStructuredAssertions instance

  langston-barrett

  committed
  29d8959

  Copy full SHA for 29d8959

• Clean up imports/exports in LLVM.Extension

  langston-barrett

  committed
  a7a6460

  Copy full SHA for a7a6460

Commits on Feb 7, 2019

• general cleanup

  langston-barrett

  committed
  b932d87

  Copy full SHA for b932d87

• crucible-jvm: structured assertions

  Show description for 56be0c1
  langston-barrett

  committed
  56be0c1

  Copy full SHA for 56be0c1

• Fix haddock comments on GADT constructors

  Show description for e3de18b
  langston-barrett

  committed
  e3de18b

  Copy full SHA for e3de18b

• Fix one more GADT constructor's haddock

  langston-barrett

  committed
  fbd050e

  Copy full SHA for fbd050e

Commits on Feb 8, 2019

• Fix undefined and incomplete pattern match

  langston-barrett

  committed
  eb356e8

  Copy full SHA for eb356e8

• fix typo

  langston-barrett

  committed
  9471aaf

  Copy full SHA for 9471aaf

• Standards.hs is Safe Haskell

  langston-barrett

  committed
  28b1692

  Copy full SHA for 28b1692

• Remove UndefinedBehavior.Config

  Show description for ca064ff
  langston-barrett

  committed
  ca064ff

  Copy full SHA for ca064ff

• Remove old code wrapped in a block comment

  langston-barrett

  committed
  4db0cca

  Copy full SHA for 4db0cca

• Merge branch 'master' into HEAD

  robdockins

  committed
  78b071c

  Copy full SHA for 78b071c

• bump submodule

  robdockins

  committed
  8bfcdb1

  Copy full SHA for 8bfcdb1

• Fixup merge

  robdockins

  committed
  b0b94a0

  Copy full SHA for b0b94a0

• Introduce the Partial type, reorganize What4.Partial

  langston-barrett

  committed
  d51693c

  Copy full SHA for d51693c

• What4: merge Partial and PartExpr into one module/representation

  langston-barrett

  committed
  724fec5

  Copy full SHA for 724fec5

• crucible: fix partexpr imports

  langston-barrett

  committed
  f58a070

  Copy full SHA for f58a070

• Merge remote-tracking branch 'upstream/partllvmval' into partllvmval-rebased

  langston-barrett

  committed
  9b55c2a

  Copy full SHA for 9b55c2a

• Remove ubiquitous PartLLVMVal suffices from functions

  Show description for 5520636
  langston-barrett

  committed
  5520636

  Copy full SHA for 5520636

• MemoryModel.Partial: more structured type errors

  langston-barrett

  committed
  c03edc6

  Copy full SHA for c03edc6

Commits on Feb 9, 2019

• propagate structured errors through memory model operations

  langston-barrett

  committed
  7f0b7f8

  Copy full SHA for 7f0b7f8

Commits on Feb 11, 2019

• more progress on merge

  langston-barrett

  committed
  644c5bc

  Copy full SHA for 644c5bc

• update crucible-jvm

  langston-barrett

  committed
  02a4db1

  Copy full SHA for 02a4db1

Commits on Feb 13, 2019

• Merge remote-tracking branch 'upstream/master' into partllvmval-rebased

  langston-barrett

  committed
  64dfa14

  Copy full SHA for 64dfa14

Commits on Mar 4, 2019

• Merge remote-tracking branch 'upstream/master' into partllvmval-rebased

  langston-barrett

  committed
  ac97d5d

  Copy full SHA for ac97d5d