Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

RFC: crucible-llvm: Parameterize over memory and pointer types #1194

Closed

Commits on Apr 2, 2024

  1. crucible-llvm: Parameterize over memory and pointer types

    The idea is that we have a lot of big changes we'd potentially like to
    make to the memory model:
    
    - Issue no. 917: Decouple memory from control flow
    - Issue no. 404: Improve underlying symbolic type for pointer representation
    - Issue no. 399: Refactoring the memory model
    - Issue no. 366: Bit-level undef/poison
    
    The problem is that these are all very hard to get started on, because
    they would involve sweeping changes across Crucible-LLVM and all
    downstream packages.
    
    We could also consider alternative memory models for different
    use-cases:
    
    - A "flat" model based on a single SMT array with a bump allocator, to
      let the SMT solver handle more of the hairy details
    - A "lazy" model in the style of UC-KLEE for under-constrained symbolic
      execution
    - A "fresh" model that always returns fresh symbolic constants when read
    
    All of these would have interesting trade-offs, but can't effectively be
    explored at the moment.
    
    This commit is the first step in making it easier to run such
    experiments. The goal is to parameterize Crucible-LLVM over a typeclass
    that provides (Crucible and Haskell) types and operations on memory and
    pointers.
    
    To that end, it introduces a new `mem` type variable. At the moment, a
    lot of places in the code add the abstraction-breaking `mem ~ Mem`
    constraint. The goal would be to gradually add operations to the `Mem`
    class and remove such equality constraints.
    
    Some notable downsides:
    
    - Increased complexity. See e.g., the pattern matches in
      `Translation.Instruction`, which I couldn't figure out how to
      adequately replace. Counterpoint: programming against an well-defined
      interface (i.e., a typeclass) can reduce mental complexity by
      abstracting superfluous detail.
    - Code churn within Crucible
    - API churn for consumers
    
    Mostly done with:
    
        mogglo-haskell \
          '${{ focus:kind() == "type" and not string.find(focus:parent():parent():text(), "mem") and focus:text() == "LLVM" }}' \
          --replace '${{ "(LLVM mem)" }}'\
          --confirm path/to/file.hs
    langston-barrett committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    b58a28f View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    7a730c2 View commit details
    Browse the repository at this point in the history
  3. crucible-llvm: Parameterize translation over pointer type

    Evaluation just assumes `mem ~ Mem`, but translation doesn't need very
    many operations.
    langston-barrett committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    5261098 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    5aa5b16 View commit details
    Browse the repository at this point in the history

Commits on Apr 4, 2024

  1. Configuration menu
    Copy the full SHA
    66373cb View commit details
    Browse the repository at this point in the history

Commits on Apr 5, 2024

  1. WIP: fix formatting

    langston-barrett committed Apr 5, 2024
    Configuration menu
    Copy the full SHA
    a28a867 View commit details
    Browse the repository at this point in the history