Re: [Haskell-cafe] ANN: powerpc-0.0.1

On Wed, Mar 10, 2010 at 8:07 AM, Warren Henning wrote:

Wow. Quite ambitious.

Was this inspired by work at your current employer like with Atom and some of the other stuff you've released?

Yes, we had an immediate need to debug some machine code. I looked around, but all the emulators I found (PSIM, et al.) were too complicated. I'm also intrigued by the emphasis on software verification at the object code level for aerospace (DO-178). I figure better tools in this area may open the door to using advanced design methods like Atom for avionics. Of course it's unlikely this project will reach that level of maturity, but you never know. -Tom

Warren

On Tue, Mar 9, 2010 at 10:35 PM, Tom Hawkins wrote:

...

Here is a new library for analyzing PowerPC programs [1].  At this point it does instruction set simulation on machine code -- and not all instructions are implemented yet, BTW.

To run a simulation, the user defines an instance of the Memory class [2] to represent both instruction and data memory.  The Memory class declares functions for memory loads and stores, instruction fetches, and reading and writing special purpose registers.  In our test bench, we set up the 'fetch' method to dump out register values so we can see the state of the processor at every step.

A neat feature of the library is the instruction behavior is captured by a little DSL [3].  This makes it easy to add new instructions because the translation from the instruction RTL spec [4] to the DSL is nearly one-to-one.  And with instruction behavior captured symbolically, this opens the door to other types of analysis besides just simulation.

I hope a few folks find it useful.

-Tom

---

Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe