I'm simultaneously fascinated and horrified (Did the solver write a counterexample for picorv32?)
SMT solvers write the weirdest programs. Wanna Jump? Simple: Just set the interrupt vector and then execute an illegal instruction.
-
-
-
No, Rocket. But it's a bug in Rockets RVFI implementation, not a bug in the actual core.
End of conversation
New conversation -
-
-
Or: end array at end of a page. Make next page write-only. Run infinite loop over array, using fault handler to end loop. No loop overhead!
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
I understand what an SMT solver is, but in what context do they generate code?
-
Superoptimisers.
- Show replies
New conversation -
-
-
Sounds like something genetic programming would come up with.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
RISC-V ISA. But SMT solvers write weird programs for all ISAs.
-
their constraints are not our constraints
End of conversation
New conversation -
-
-
to be fair, illegal instruction dispatch is how the classic mac os did system calls on the 68k
-
This Tweet is unavailable.
- Show replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.