Easier symbolic variables and output readiability

[ghost]

I wanted to broaden the ways that users can make symbolic variables and provide more readable output.

The result is a helper crate with a function mksym, that takes any Sized variable and fills it with symbolic bytes. Usage looks like

let mut t = MyStruct { a: 0, b: 0 };
seer_helper::mksym(&mut t);
if t.a == 123 && t.b == 321 {
    panic!();
}

I did two things to make the output easier to read:

• separate the variables so it clear what data corresponds to which variable in the program
• replace the [u8] representation with the Debug representation for the type

The result looks like this:

ExecutionComplete { input: [stdin: [], t: "MyStruct { a: 123, b: 321 }"], result: Err(...) }
hit an error. halting

In implementation, seer_helper::mksym is an empty function, but Seer intercepts calls to it and overwrites the memory of the argument with (so far unconstrained) abstract bytes. In order to improve the output, the name and type of the argument is stored in the ConstraintContext. For formatting, the idea is to evaluate a call to a generic formatting function that returns a String in a fresh EvalContext (see format_executor.rs). I had some trouble finding DefIds for functions in the helper crate, so I resorted to making the client crate use an init macro that defines the function inside the client crate.

[dwrensha]

Thanks! I should have some time within the next week to take a look at this.

[dwrensha]

This looks cool!

I tried running the new example seer/example/seer-helper-user, and expected it to find a panic, but got:

$ RUSTFLAGS="-Z always-encode-mir" xargo seer
   Compiling seer-user v0.1.0 (file:///home/dwrensha/src/seer/seer/example/seer-helper-user)
ExecutionComplete { input: [], result: Ok(()) }
as string: Ok("")
    Finished dev [unoptimized + debuginfo] target(s) in 0.14s

Do you have any idea what might be going wrong here?

[dwrensha]

What is the reasoning behind creating this new seer/ subdirectory and moving everything into it? I would prefer to avoid all of the file renaming in this pull request, if possible.

[ghost]

I moved seer to a subdirectory to keep it separate from the helper crate. Since my extensions to Seer rely on the contents of the helper crate, it makes sense to me to keep them in the same repository. Maybe it would be better to make the seer-helper crate a sibling of seer's Cargo.toml?

For the broken example, my first guess is that an old cargo-seer/seer executable runs. Then the mksym call would end up as a no-op and you would get no symbolic variables. Then the panic case would never happen. I would try cargo install --force --path . in the seer/ subdirectory.

[dwrensha]

For the broken example, my first guess is that an old cargo-seer/seer executable runs

Oops. You are correct. Now I'm seeing:

ExecutionComplete { input: [stdin: [], t: "MyStruct { a: 123, b: 321 }"], result: Err(NoMirFor("std::sys::unix::fast_thread_local::register_dtor::::__cxa_thread_atexit_impl")) }

which seems less wrong.

[dwrensha]

Maybe it would be better to make the seer-helper crate a sibling of seer's Cargo.toml

Yeah, I think it would work totally fine to keep src where it currently is on master, and to add the subdirectory seer-helper with the new crate. I believe that cargo is smart enough that it will avoid including the seer-helper subdirectory when packaging the main seer crate.

[ghost]

I think the Err(NoMirFor("std::sys::unix::fast_thread_local::register_dtor::::__cxa_thread_atexit_impl")) comes from a separate bug. If I run the base64 example with MIR for std, I get the same error. I'll open an issue for it.

[dwrensha]

what's going on with this new example/example/capnp/src/packing.rs file?

[ghost]

Looks like I made a mistake in moving. I'll move it back where it belongs.

[dwrensha]

Thanks!