Add MIPS support

[vobst]

I recently had the need for a symbolic execution engine with nice Rust bindings (or even better, written in Rust) and MIPS support. The first thing worked out well here, the second thing required a bit of work, but it now works nicely :)

The main problem with MIPS support was handling of delay slots. I decided to handle them using the existing (but by default disabled) explicit delay-slot related operations in ESIL strings. See for details on my changes on the radare side radareorg/radare2#23307. The other thing was putting the right return address in the backtrace, but this works nicely since the fail address is already delay slot aware. Note that the handling of delay slots is incomplete, in the sense that "likely" instructions are not handled correctly. Those instructions only execute the delay slot if the branch is taken. It should be straight forward to do this properly by changing the ESIL of those instructions to

...,?{,"addr", SETJT, 1, SETD}{4,pc,+,pc,:=}

Also note that currently only a single delay slot is supported. Extending the code to multiple delay slots should be straight forward as well, e.g., by making delay a counter.

However, this patch is everything but clean, thus only a draft PR. Mostly for reference (on what to do do, or not to do) if you, or any other contributor, ever want to add delay slot support. The main blockers are:

• I am quite opinionated about conditional symbolic values -- I thoroughly hate them :) -- and thus I removed them completely. IMHO this makes the code much simpler without any drawbacks, THB I think those values should not exist in symbolic states in the first place, it breaks the whole idea of a symbolic state corresponding to an equivalence class of concrete executions that go down a single path. In fact, without this change I would not have known how to implement delay slots without incredibly awkward code.
• I broke a bunch of features related to stuff that I did not need for my use-case (which was UC symex on bare metal firmware). Those should be easy to fix.
• I added a hack to duplicate the solver on each fork of a state. This was needed since else boolector would abort if two states independently created the same symbolic memory. Since I also don't found a way to check if a variable already exists in a solver (boolector would just abort if it doesn't ...?!?! ... it would probably be an easy change on their side to provide such a method) I introduced this ugly inefficiency.

There are some other things, like adding doc comments, renaming things in a (IMO) descriptive way, which shouldn't me major problems though.

Thanks for creating this great project! If you want to add delay slot support I'd be happy to discuss my experience with you.

Cheers

[aemmitt-ns]

wow this looks amazing! sorry i haven't been paying proper attention to this project. i've wanted to actually support MIPS for a while so this is fantastic. i am still going through all the changes, some of which are things i have wanted to do myself, but hadn't gotten around to.

I am quite opinionated about conditional symbolic values -- I thoroughly hate them :) -- and thus I removed them completely. IMHO this makes the code much simpler without any drawbacks, THB I think those values should not exist in symbolic states in the first place, it breaks the whole idea of a symbolic state corresponding to an equivalence class of concrete executions that go down a single path. In fact, without this change I would not have known how to implement delay slots without incredibly awkward code.

the conditional symbolic values and temporary stacks are a result of the decision i made that forks should not occur within the evaluation of a single instruction, and only occur when actually branching. there are good reasons for doing this, since eg. cset type instructions won't cause forks and so won't contribute to state explosion. but it also has made some things very difficult and frankly gross. really all of processor.rs needs to be refactored. it was one of the first things i wrote and this is my first project written in rust so it is very rough. i am not sure if i will take the approach you have here, though if it is the only (sane) way to support the delay slots then i will. otherwise i will probably go with whatever results in faster solves.

I broke a bunch of features related to stuff that I did not need for my use-case (which was UC symex on bare metal firmware). Those should be easy to fix.

no problem we will get it all sorted out

I added a hack to duplicate the solver on each fork of a state. This was needed since else boolector would abort if two states independently created the same symbolic memory. Since I also don't found a way to check if a variable already exists in a solver (boolector would just abort if it doesn't ...?!?! ... it would probably be an easy change on their side to provide such a method) I introduced this ugly inefficiency.

yeah boolector has some unfortunate design decisions. the solution for this is pretty simple (if a bit redundant) though: we can keep track of all the different labels independently in Solver to ensure that we don't try to re-create existing vars. this is something i have been meaning to do. i will probably do this first.

older versions of radius2 attempted to do parallel processing and so solvers were also duplicated for that, but that led to new issues when attempting to merge states as values which didn't exist at the time of duplication couldn't then be translated to be merged back into the "parent" state... at least it was something like that. i forget the details it was a while ago. so because of that and the fact that the overhead of the parallelism was too high to be worthwhile i ditched all the support for the solver duplication and value translation. unfortunately that probably will remain the case unless we can also swap out boolector with another SMT library, ideally one that supports multiple backend solvers. but last i checked there wasn't anything very mature that could be used easily.

a lot of the weirder looking code is the way it is for my bad parallelism ideas, which were then removed so the code is now just confusing and awful for no reason at all.

also if we refactored the solver stuff we could potentially do real lazy solving with another thread that checks sat while the states advance. i am rambling now though sorry.

There are some other things, like adding doc comments, renaming things in a (IMO) descriptive way, which shouldn't me major problems though.

these are all good changes i will use them.

i will definitely need some time to look over all everything but i am committed to get it all working so that we can support MIPS. I think i will make some proper issues as i go through and understand more thoroughly what needs to be done. ideally i would like to make more minimal changes than some of what has been done here, but realistically a lot of my code is hot garbage and needs to go.

ok i will start looking this all over now. thank you again this is awesome!

[aemmitt-ns]

cant wait to move MIPS from "Supported" Architectures to Supported Architectures!

[vobst]

Hi, no problem, I've been distracted doing other stuff as well. Also the reason why I didn't get to work on the r2 changes needed to support this radareorg/radare2#23307.

Concerning the cond. symbolic values. As I said, I'm quite opinionated on this ... angr is using them as well and it is one of the main reasons why for me doing serious stuff with angr is such a PITA. In principle, instructions like cmov and so on are ITE statements within a single assembly instruction. IMHO IRs like ESIL and Pcode are right to pull this apart into an explicit ITE at the IR level. IMHO it breaks the original "one sybolic state per concrete path through the program" paradigm of symbolic execution and leads to the "leaking" of path constrains into the symbolic store. Furthermore, like this symex is not entirely at the level of the IR, but concepts like instruction boundaries "leak" into it from the assembly.

If performance is the concern here, there are optimizations that could be implemented to lower the cost of forking, and in general to reduce the number of queries to the solver (like 1m of papers on this ^^, I guess you are already aware of those, this might be the more promising path to improve perfomance). Because while it might save you a fork to introduce the cond. sym. val., it comes at the cost of much more complex value formulas which has other implications on solver performance.

I'm happy that you find this work useful! I maintain the cwe_checker (which is Ghidra-based) and my actual goal is to add Pcode symex to it. It might be worthwhile to consider whether we have some common needs, like e.g. a Rust abstraction layer over solvers and implementations of related optimizations.