Code

Heapster string literals#1456

Code

Merged

eddywestbrook merged 35 commits intomasterGaloisInc/saw-script:masterfrom heapster-string-literalsGaloisInc/saw-script:heapster-string-literalsCopy head branch name to clipboardSep 15, 2021

+567-84

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

• 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