The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi Siddharth,

Regarding CompCert, the optimisations are mostly performed over the RTL
language i.e RTL -> RTL transformation. 
Compared to LLVM, this is true that invariants are not embedded into
the language and that the program semantics is fixed : it looks like a
good thing to compose transformations.
BTW, there are passes (among others) performing liveness, (local) value
numbering. The proofs do not exhibit, as you propose, a non-standard
semantics but the properties are directly embedded in the soundness
proof.

You may also look at the Vellvm project 
http://www.cis.upenn.edu/~stevez/vellvm/

Best,
--
Frédéric

On Wed, 2018-06-20 at 14:59 +0200, Siddharth Bhat wrote:
> Hello everyone,
> 
> I've been looking around codebases related to programming languages
> in Coq
> (mostly CompCert), and have done some reading around the subject.
> 
> I'm trying to design the semantics for a mini-language which has
> loops and
> control flow, and I would like a nice way to write analyses over this
> language
> and reason about the operational semantics.
> 
> In general, the way to "perform analysis" within the formal
> verification
> community seems to be to translate between languages which contain
> different
> information, along with a soundness proof.
> 
> However, coming from an LLVM perspective, the general way of
> structuring this
> is to provide analyses over the same IR, which provides information
> about the
> IR.
> 
> So, I would like to design some model which "changes" the operational
> semantics
> based on available information. I give examples of what I have in
> mind below:
> 
> 
> 1. Consider an LLVM-like IR, where the operational semantics in the
> zero
> information case will step through loop execution on the instruction
> level. But
> on being provided with loop information, will "step through" loop
> iterations at
> a higher level.
> 
> 2. On performing liveness analysis, the operational semantics would
> "skip" dead
> instructions.
> 
> 3. With global value numbering, the operational semantics would
> lookup the
> value number table, and use the precomputed value from this table if
> an
> instruction has been pre-computed.
> 
> 4. On having scalar evolution, the value of an instruction which has
> scalar
> evolution information attached to it would be computed using the SCEV
> formuation, and not the instruction's semantics.
> 
> So, if one defines their operational semantics as an inductive or
> coinductive
> function, is there some nice way to "compose" / "use" the extra
> analysis
> information to "drive" the operational semantics in different ways?
> How would I
> design such a system for my IR?
> 
> I understand the question is broad / high level, so I'd appreciate
> any
> references to prior art. If not, is this kind of design interesting
> to the
> community as a whole?
> 
> Thanks, Siddharth
> 
> -- 
> Sending this from my phone, please excuse any typos!