The Coq mailing list

[Siddharth Bhat <siddu.druid AT gmail.com>]

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!