[Coq-Club] Composable proofs about analysis and operational semantics of programming languages

[Siddharth Bhat]

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

[Frédéric Besson]

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

Post by Siddharth Bhat
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
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!