search

rems-project / sail

Sail architecture definition language
Other
617 stars 112 forks source link

Are `decode` and `execute` keywords in Sail? #76

Open martinberger opened 4 years ago

martinberger commented 4 years ago

Just to double check: the functions decode and execute are not keywords in Sail? I'm asking, because I want to know if there is a purely syntactic way of distinguishing the definitions of instruction description and instruction behaviour.

PeterSewell commented 4 years ago

They're not special in the language itself, but the backends presumably know those names - Alasdair?

Peter

On Thu, 9 Jul 2020 at 13:59, Martin Berger notifications@github.com wrote:

Just to double check: the functions decode and execute are not keywords in Sail? I'm asking, because I want to know if there is a purely syntactic way of distinguishing the definitions of instruction description and instruction behaviour.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/rems-project/sail/issues/76, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZUR765GLSW4HXSHYHDR2W5MPANCNFSM4OVSOEAQ .

martinberger commented 4 years ago

Any news on this by any chance? Presumably the generator that creates the C and Ocaml emulators needs to know what's decoding and what's instruction semantics. Is this handled on an ad-hoc basis or somehow hardcoded?

Alasdair commented 4 years ago

The only thing special about decode and execute as function identifiers within Sail is that they are considered roots when we do dead-code elimination, so they will always be preserved.

It's mostly just convention, although we have found useful to have a separate decode and execute function with an intermediate instruction type. Not all our specs strictly follow this however, like the ARM spec follows the ARM ASL in having a decode64 and decode32 function that directly execute the decoded instruction.

martinberger commented 4 years ago

Thanks. So if I wrote an ISA interpreter and called the relevant functions giraffe and elephant how would that affect the generated emulators?

Alasdair commented 4 years ago

It would not affect them.

I think the theorem prover backends will try to split up any function called execute into multiple execute_clause functions, because some theorem provers struggle if you give them really large definitions, but other than that I don't think there is any special behavior.