Implement an API for hooks and breakpoints. Perhaps it is better to implement these as a part of esil-rs as other applications that use esil-rs will probably need some hooking functionality too.

Check for path feasibility before dequeue to avoid taking impossible paths

RuneContext currently cannot handle symbolic jumps. Some amount of refactoring is needed in order to implement this feature efficiently.

Implement From<R2Stream> for FileStream in order to convert R2Stream into
a FileStream. This allows radare2 to be closed and additionally provides a
way to construct files that can be reused for further tests wihtout depending
on radare2.

• Handle Memory Read / Write
• Update esil vars

• Setup Travis CI
• Setup coveralls

• stash unexplored path options for future exploration

• Point Cargo.toml to use non-local dependencies

write implementation for RuneContext does not check if the size of destination and source are correct. This will lead to generation of invalid constraints which cannot be solved by the solver. A simple example where this can occus is in x86 instruction such as:
mov rax, ax

Current implementation of context uses SMTLIB2 directly. This is not scalable on the long run as we do not perform any optimizations on the constraints that are generated before feeding it into the backend SMT solver.
This can be fixed by leveraging radeco IL from radeco IL and performing static analysis / optimizations before feeding the constraints to a solver.

As an added part of this task, concrete values must be treated differently from symbolic values. This reduces unnecessary constraints from being generated in the first place.

Right now, the user requires to type in a long command to set up a session. This makes it a little cumbersome since a single error in the command would require them to fix the command again. It would be ideal if we could have a default context setup and then the user could interact in the console to set those values.

Example:

krypt0@chinmaydd: runec ./a.out
[+] Loading default context values
>> set zf=1
>> set break=0x8000
>> run
[+] Halted at 0x8000

• Load breakpoints from flags in r2
• Load start address based on current seek in r2 (unless the start flag is set)
• Load register values set from r2.
• Raw commands to radare2

From here. This will highly improve performance on repeated querying.

This would require feature additions and modifications in libsmt.rs.

• Interactive explorer
• rune binary that parses command line options and sets up rune
• Interactive shell to query for constraints

• Formalize and document the Rune engine semantics. Currently, it seems a bit arcane and maybe missing all the needed functionality.
• Document and extend RuneControl functionality.
• Generalize Rune to accept instruction in any format (as opposed to the current limitation of LOpInfo).
• Generalize Rune to emit constraints in any form (as opposed to being restricted to QF_AUBV_Fn now).

Similar to define_const that is currently present but for defining symbolic variables

• Add a README
• Add a LICENSE
• Logo

• Use Into

Add support for symbolic memory access in rune.

One simple way to solve this issue is to solve for the symbolic variable and spawn an instance of rune to work on each of these solutions.

• Fix warnings in build
• Fix warnings after enabling rust_clippy to ensure better rust practices