Nothing Special   »   [go: up one dir, main page]

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

Initial support for AArch32 #987

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

Initial support for AArch32 #987

wants to merge 1 commit into from

Conversation

chameco
Copy link
Contributor
@chameco chameco commented Jan 4, 2021

This PR adds support for 32-bit ARM verification using LLVM specifications, introducing a new top-level function llvm_verify_aarch32 with an interface similar to llvm_verify_x86.

I've marked this as a draft since it's very hacky and fragile right now.
A few things that I'd like to fix before merging:

  • Generalize the utility functions copied from SAWScript.X86 and SAWScript.X86Spec, and use them in both SAWScript.Crucible.LLVM.X86 and SAWScript.Crucible.LLVM.AArch32.
  • Share as much code as possible between the x86_64 and AArch32 support. Ideally, there would be a common interface (at least internally) to all Macaw backends, parameterized by architecture information, ABI, etc.
  • Potentially reuse more code from asl-translator.
  • Add integration tests.

There's also a problem of compile time. Some of the new dependencies take significantly longer to build, which could negatively impact the CI experience.

In the long run, I'd like to make these low-level backends less of a "walled garden". Right now, the llvm_verify_<arch> commands have two (tightly-coupled) steps: translate an LLVM spec to an <arch> spec according to the ABI, and then verify that <arch> spec. It might be nice to decouple these steps a bit to make future development cleaner.

Example usage! I used Zig for a convenient binary because it's really easy to cross compile.

// test.zig
export fn add(a: i32, b: i32) i32 { return a + b; }
pub fn main() void {}

zig build-exe test.zig -target arm-linux --release-fast will build a 32-bit ARM ELF with

add:
    add r0, r1, r0
    bx lr

To test:

// test.c
extern int add(int a, int b);
int main() { return add(1, 0); }

clang -m32 -c -emit-llvm test.c will build some reasonable bitcode that uses add.

// test.saw
enable_experimental;
m <- llvm_load_module "test.bc";
let spec = do {
  a <- crucible_fresh_var "a" (llvm_int 32);
  b <- crucible_fresh_var "b" (llvm_int 32);
  crucible_execute_func [crucible_term a, crucible_term b];
  crucible_return (crucible_term {{ a + b : [32] }});
};
llvm_verify_aarch32 m "test" "add" [] false spec w4;

@andreistefanescu
Copy link
Contributor

cc @travitch

@travitch
Copy link
Contributor
travitch commented Jan 4, 2021

Neat! This is exciting. The compile times are a huge problem generally - I'd love to find some ways to improve them.

Is there anything in particular I can do to support this? It seems like a good opportunity for us to take stock of what shared infrastructure is lacking around the binary analysis symbolic execution backends.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants