rems-project / sail

Sail architecture definition language
Other
617 stars 112 forks source link

Debuggability of SAIL code #141

Open abukharmeh opened 3 years ago

abukharmeh commented 3 years ago

Hi,

I am wondering if you have any hints on how to debug / go through big SAIL code ? I am thinking maybe attaching GDB to the generated C code might help, but also maybe if SAIL compiler adds line number macro it would be possible to make GDB auto follow the original code ? https://gcc.gnu.org/onlinedocs/cpp/Line-Control.html

Kind regards, Ibrahim

martinberger commented 2 years ago

Attaching a low-level debugger is one option, but I wonder if it could be augmented, in a systematic way, by something more high-level that more directly helps observing processor state. The question of observing the internals execution of the Sail model is the top request I get. (E.g. what's the state of register 17 after the 52309th execution step?)

I wonder if we could augment the Sail compiler so it has an additional compilation mode, call it

   -c_observable

that does a kind of CPS-transform that lets the user of the C model plug in arbitrary observation code from the outside, but without changing the Sail model at all. I'm not 100% of how best to set this up.