Vitaly Chipounov

S2E does not currently support this scenario. I suppose you'd have to tweak the state snapshotting mechanism to ignore the globalstate device if it's not present.

You ran that in native KLEE, and 36 seconds is still very slow I would argue. I suggest you try the same in S2E... It's way worse, because that single...

We built a TCI prototype back in 2012, it was about 2-3x slower than native TCG and way faster than KLEE. Unfortunately we never got the time to clean it...

@humeafo I am glad you asked :) I will start working on it probably in July. Before that, I need to do some ground work to make its implementation easier:...

Please attach your trace file.

Also, did S2E terminate properly or was it killed? In the latter case, it won't get a chance to flush the trace so you might have corrupted entries.

I wonder why LinuxMonitor::handleMemMap is not called. Here's where it's called in the guest: https://github.com/S2E/s2e-linux-kernel/blob/2a62845de82979cb8e7240ca51503dd7ffbb5efb/linux-4.9.3/mm/util.c#L318 Perhaps we are missing other places where Linux is allocating memory.

Was handleMemMap called with the stack region?

Yep. The doc is for the old S2E, this feature is missing for now. I remember @VPaulV was working on it.

Not on my side, it would be really nice if someone could do it.