On 3 February 2017 14:46:15 GMT+00:00, Stefan Hajnoczi <stefa...@gmail.com> 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
