Code

Heapster/exponential code explosion#1528

Code

Merged

eddywestbrook merged 15 commits intomasterGaloisInc/saw-script:masterfrom heapster/exponential-code-explosionGaloisInc/saw-script:heapster/exponential-code-explosionCopy head branch name to clipboardDec 1, 2021

+160-88

Commits

Commits on Nov 23, 2021

• short-circut true BVProp_Neqs in the translation

  m-yac

  committed
  82a4aca

  Copy full SHA for 82a4aca

• fixed a bug in splitLLVMBlockPerm

  

  Eddy Westbrook

  committed
  bc0fd6e

  Copy full SHA for bc0fd6e

• small tweaks to the widening code to make the precise conditions of various cases more clear

  

  Eddy Westbrook

  committed
  0f4e55f

  Copy full SHA for 0f4e55f

• added support for constant propagation through and, or, xor, and not of bitvectors

  

  Eddy Westbrook

  committed
  28da80d

  Copy full SHA for 28da80d

• Merge branch 'heapster/sha512' of github.com:GaloisInc/saw-script into heapster/sha512

  

  Eddy Westbrook

  committed
  a4ed114

  Copy full SHA for a4ed114

Commits on Nov 24, 2021

• optimized implGetLLVMPermForOffset so that it only returns permissions that could actually be used to prove a permission at the given offset

  

  Eddy Westbrook

  committed
  4edb06b

  Copy full SHA for 4edb06b

Commits on Nov 29, 2021

• changed the translation of LLVM globals so that each is translated to its own SAW core definition, rather than having the entire global be copied into each spec when it is used

  

  Eddy Westbrook

  committed
  5db8e70

  Copy full SHA for 5db8e70

• removed no longer needed imports from SAWTranslation.hs

  

  Eddy Westbrook

  committed
  a255e15

  Copy full SHA for a255e15

• added the OpenTerm combinator completeNormOpenTerm to beta-normalize an OpenTerm after it is completed

  

  Eddy Westbrook

  committed
  d6c29b8

  Copy full SHA for d6c29b8

• changed the translation of TypedSetReg to let-bind its output expression translation, to avoid exponential code explosion

  

  Eddy Westbrook

  committed
  db9dfe7

  Copy full SHA for db9dfe7

• changed the translation of lambdas so that their bodies have let-bindings for repeated terms; added a type ascription term to the Coq AST; changed the translation of the unit type to give it an exp…

  Show description for dd9aa83
  

  Eddy Westbrook

  committed
  dd9aa83

  Copy full SHA for dd9aa83

• Merge remote-tracking branch 'origin/saw-core-coq/lets-in-lambda-bodies' into heapster/sha512

  

  Eddy Westbrook

  committed
  3b1c877

  Copy full SHA for 3b1c877

Commits on Nov 30, 2021

• added a dummy translation of BVUndef to the 0 bitvector value

  

  Eddy Westbrook

  committed
  27a845c

  Copy full SHA for 27a845c

• Merge branch 'master' into heapster/sha512

  

  Eddy Westbrook

  committed
  290c303

  Copy full SHA for 290c303

• Merge branch 'master' into heapster/sha512

  

  Eddy Westbrook

  committed
  4c12a9d

  Copy full SHA for 4c12a9d