Re: [Qemu-devel] TCG semantics

[Ed Robbins]

On 3 February 2017 14:46:15 GMT+00:00, Stefan Hajnoczi <address@hidden> wrote:
>On Thu, Feb 02, 2017 at 12:09:02PM +0000, E.Robbins wrote:
>> I having been looking for prior work on a formalised semantics for
>the TCG language. I have seen passing references, and wondered if
>anyone can provide any pointers?
>> 
>> If this is the wrong list for this question, apologies, please direct
>me elsewhere.
>
>This is the right list.  Welcome!
>

Thanks!

>Have you seen tcg/README?  It describes the TCG ops.
>

Yes, but was hoping for something a bit more precise, with a memory model etc. 
However, it isn't too much work to build one from the readme.

>If it's out of date or missing information, then improving the document
>seems worthwhile.

It seems pretty good. I was surprised that call instructions can have 
arguments/return specified, and wonder if those are normally just empty, so 
that emulation of the target stack/registers just carries the args/return in 
the background. Otherwise TCG must be detecting the target's arguments/return 
for each call which would need a clever dataflow analysis, or to follow calling 
convention and just hope, right?

I also am not clear about the precise operation of the byte swap instruction, 
but guess it follows the x86 bswap semantics.

I expect I can answer these questions by looking at some TCG output or checking 
the code, though (I don't want to waste anyone's time with that).

Thanks,
Ed