Code

Heapster array field implications#1459

Code

Merged

eddywestbrook merged 54 commits intomasterGaloisInc/saw-script:masterfrom heapster-array-implsGaloisInc/saw-script:heapster-array-implsCopy head branch name to clipboardSep 17, 2021

+557-242

Commits

Commits on Aug 31, 2021

• fixed the IRT description generation to match the recent change that made the translation of bitvector permissions to just be bitvectors

  

  Eddy Westbrook

  committed
  884b584

  Copy full SHA for 884b584

• Merge branch 'heapster-fix-memcpy-bug' into heapster-bugfix-bitvector-irts

  

  Eddy Westbrook

  committed
  e98bd33

  Copy full SHA for e98bd33

• Merge branch 'master' into heapster-bugfix-bitvector-irts

  

  Eddy Westbrook

  committed
  6387369

  Copy full SHA for 6387369

Commits on Sep 1, 2021

• updated xor_swap_rust example to use the Rust type in the SAW script

  

  Eddy Westbrook

  committed
  5b5f422

  Copy full SHA for 5b5f422

• added a case to the Rust to Heapster translator to handle function types with no return value

  

  Eddy Westbrook

  committed
  7b7709f

  Copy full SHA for 7b7709f

• whoops, forgot to update the bitcode file for xor_swap_rust

  

  Eddy Westbrook

  committed
  c18aec7

  Copy full SHA for c18aec7

• bugfix in the Rust to Heapster translator: empty return types need to be converted to unit, not to the empty struct

  

  Eddy Westbrook

  committed
  5bc366a

  Copy full SHA for 5bc366a

• tweaked the error message for when Rust types do not translate correctly to the expected LLVM type

  

  Eddy Westbrook

  committed
  068b735

  Copy full SHA for 068b735

Commits on Sep 2, 2021

• started adding support for string literals by moving all creation of a HeapsterEnv into a single function which iterates through the globals and adds those it can handle

  

  Eddy Westbrook

  committed
  f63c326

  Copy full SHA for f63c326

Commits on Sep 3, 2021

• added a formatting example in Rust, and started defining the necessary types for it

  

  Eddy Westbrook

  committed
  2720516

  Copy full SHA for 2720516

• started trying to figure out how Rust stores string literals in its generated LLVM files

  

  Eddy Westbrook

  committed
  a6aee80

  Copy full SHA for a6aee80

Commits on Sep 7, 2021

• Merge branch 'master' into heapster-string-literals

  

  Eddy Westbrook

  committed
  cd01dab

  Copy full SHA for cd01dab

• fixed the prtty-printing for constant values

  

  Eddy Westbrook

  committed
  024287e

  Copy full SHA for 024287e

• changed TrueEnum::fmt to use the fmt method rather than the write! macro

  

  Eddy Westbrook

  committed
  917547e

  Copy full SHA for 917547e

• whoops, changed the fmt method for TrueEnum back to using the write! macro, because that seems to be the proper way to do things

  

  Eddy Westbrook

  committed
  389d0d2

  Copy full SHA for 389d0d2

• whoops, forgot to add the repr(u64) pragma to the TrueEnum type

  

  Eddy Westbrook

  committed
  f0ed90b

  Copy full SHA for f0ed90b

• added a type-checking command for TrueEnum::fmt

  

  Eddy Westbrook

  committed
  1d6a5d7

  Copy full SHA for 1d6a5d7

• moved some OpenTerm operators from SAWTranslation.hs to OpenTerm.hs

  

  Eddy Westbrook

  committed
  e987f42

  Copy full SHA for e987f42

Commits on Sep 8, 2021

• added llvmReadBlockOfShape

  

  Eddy Westbrook

  committed
  2752723

  Copy full SHA for 2752723

• more work trying to translate globals

  

  Eddy Westbrook

  committed
  92d04e1

  Copy full SHA for 92d04e1

• got string literals translated, but now there is some translation bug...

  

  Eddy Westbrook

  committed
  4f911f7

  Copy full SHA for 4f911f7

• whoops, translating a shape always yields exactly one term

  

  Eddy Westbrook

  committed
  64d3006

  Copy full SHA for 64d3006

Commits on Sep 9, 2021

• added helper function exprLLVMTypeBytes

  

  Eddy Westbrook

  committed
  01074a9

  Copy full SHA for 01074a9

• added support for Rust slice types

  

  Eddy Westbrook

  committed
  d2b4a22

  Copy full SHA for d2b4a22

• whoops, combined the two cases for translating shared vs mutable references into one

  

  Eddy Westbrook

  committed
  3941cdb

  Copy full SHA for 3941cdb

• updated funPerm3FromArgLayout to handle layouts with existential permissions

  

  Eddy Westbrook

  committed
  2982d1f

  Copy full SHA for 2982d1f

Commits on Sep 13, 2021

• updated the rust_data example to use string literals

  

  Eddy Westbrook

  committed
  281d602

  Copy full SHA for 281d602

Commits on Sep 14, 2021

• added mapM and mapBVVecM

  

  Eddy Westbrook

  committed
  dbb2b9f

  Copy full SHA for dbb2b9f

• added support for proving array permissions from other array permissions with different fields using the SImpl_LLVMArrayContents rule; to get the translation of the SImpl_LLVMArrayContents to work …

  Show description for 9ae8f75
  

  Eddy Westbrook

  committed
  9ae8f75

  Copy full SHA for 9ae8f75

• added more definitions to the arrays example now that the implication prover can map array permission contents

  

  Eddy Westbrook

  committed
  8caa577

  Copy full SHA for 8caa577

• moved the LLVM globals code to a new file LLVMGlobalConst.hs

  

  Eddy Westbrook

  committed
  f0e36a1

  Copy full SHA for f0e36a1

• fixed the translation of LLVM array constants to generate SAW core BVVecs instead of SAW core Vecs

  

  Eddy Westbrook

  committed
  1eb2323

  Copy full SHA for 1eb2323

• regenerated Coq files for saw-core-coq

  

  Eddy Westbrook

  committed
  9347756

  Copy full SHA for 9347756

• added support for the Crucible BVZext and BVTrunc instructions, and fixed up that for BVSext

  

  Eddy Westbrook

  committed
  6a62a56

  Copy full SHA for 6a62a56

Commits on Sep 15, 2021

• added heapster_init_env_debug and heapster_init_env_from_file_debug commands

  

  Eddy Westbrook

  committed
  0b6bf9d

  Copy full SHA for 0b6bf9d

• small tweaks to rust_data.saw to get it to work

  

  Eddy Westbrook

  committed
  495e958

  Copy full SHA for 495e958

• added another formatting example that we cannot handle yet...

  

  Eddy Westbrook

  committed
  7e94ba7

  Copy full SHA for 7e94ba7

• Merge branch 'master' into heapster-string-literals

  

  Eddy Westbrook

  committed
  84639a6

  Copy full SHA for 84639a6

• Merge branch 'heapster-string-literals' into heapster-array-impls

  

  Eddy Westbrook

  committed
  b4bcb74

  Copy full SHA for b4bcb74

• RecurseFlag to Permissions.hs; added requireNamedPerm

  

  Eddy Westbrook

  committed
  f7e53a9

  Copy full SHA for f7e53a9

• widening now unfolds defined and recursive permissions

  

  Eddy Westbrook

  committed
  9823bc0

  Copy full SHA for 9823bc0

• whoops, forgot to insert a bindM into the translation of SImpl_LLVMArrayContents

  

  Eddy Westbrook

  committed
  d91b753

  Copy full SHA for d91b753

• removed the old gen_block_perms hints that are no longer used anyway from arrays.saw

  

  Eddy Westbrook

  committed
  899cf70

  Copy full SHA for 899cf70

• Merge branch 'master' into heapster-array-impls

  

  Eddy Westbrook

  committed
  c77c095

  Copy full SHA for c77c095

• changed tupleTypeTrans to no longer having the trailing unit type on tuples of 2 or more types; updated foldList and unfoldList in the SAW core Prelude to fit this new approach; regenerated the res…

  Show description for f213fbd
  

  Eddy Westbrook

  committed
  f213fbd

  Copy full SHA for f213fbd

• Merge branch 'master' into heapster-array-impls

  

  Eddy Westbrook

  committed
  909d1a1

  Copy full SHA for 909d1a1

Commits on Sep 16, 2021

• small tweak to the expression type-checker to type-check the bodies of existential shapes as arbitrary expressions

  

  Eddy Westbrook

  committed
  fe25d91

  Copy full SHA for fe25d91

• expanded the translation of Rust slices to allow multiple fields

  

  Eddy Westbrook

  committed
  eef2cbf

  Copy full SHA for eef2cbf

• updated mbox proof script to work with the recent changes, though not all the mbox proofs work...

  

  Eddy Westbrook

  committed
  60bad84

  Copy full SHA for 60bad84

• started updating the mbox proofs, but I got stuck...

  

  Eddy Westbrook

  committed
  13e6b21

  Copy full SHA for 13e6b21

• moved formatting-related types in the rust_data example to their own section

  

  Eddy Westbrook

  committed
  e327986

  Copy full SHA for e327986

• finished updating mbox proofs

  

  Eddy Westbrook

  committed
  0eef2f0

  Copy full SHA for 0eef2f0

• updated examples to match the change to the SAW translation

  

  Eddy Westbrook

  committed
  db7a743

  Copy full SHA for db7a743

• updated the IRT translation to match the updates to the SAW translation

  

  Eddy Westbrook

  committed
  15b7d19

  Copy full SHA for 15b7d19