WG211/M16Blazy - Revision history

Sandrine at 10:23, 14 June 2016

2016-06-14T10:23:44Z

← Older revision		Revision as of 12:23, 14 June 2016
Line 1:		Line 1:
	The CompCert C compiler guarantees that the target program behaves as the source program. Yet, source programs without a defined semantics do not benefit from this guarantee and could therefore be miscompiled. To reduce the possibility of a miscompilation, we propose a novel memory model for CompCert which gives a defined semantics to challenging features such as bitwise pointer arithmetics and access to uninitialised data.		The CompCert C compiler guarantees that the target program behaves as the source program. Yet, source programs without a defined semantics do not benefit from this guarantee and could therefore be miscompiled. To reduce the possibility of a miscompilation, we propose a novel memory model for CompCert which gives a defined semantics to challenging features such as bitwise pointer arithmetics and access to uninitialised data.

	We evaluate our memory model both theoretically and experimentally. In our experiments, we identify pervasive low-level C idioms that require the additional expressiveness provided by our memory model. We also show that our memory model provably subsumes the existing CompCert memory model thus cross-validating both semantics.		We evaluate our memory model both theoretically and experimentally. In our experiments, we identify pervasive low-level C idioms that require the additional expressiveness provided by our memory model. We also show that our memory model provably subsumes the existing CompCert memory model thus cross-validating both semantics.

	Our memory model relies on the core concepts of symbolic value and normalisation. A symbolic value models a delayed computation and the normalisation turns, when possible, a symbolic value into a genuine value. We show how to tame the expressive power of the normalisation so that the memory model fits the proof framework of CompCert. We also adapt the proofs of correctness of the compiler passes performed by CompCert, thus demonstrating that our model is well-suited for proving compiler transformations.		Our memory model relies on the core concepts of symbolic value and normalisation. A symbolic value models a delayed computation and the normalisation turns, when possible, a symbolic value into a genuine value. We show how to tame the expressive power of the normalisation so that the memory model fits the proof framework of CompCert. We also adapt the proofs of correctness of the compiler passes performed by CompCert, thus demonstrating that our model is well-suited for proving compiler transformations.

Sandrine at 10:23, 14 June 2016

2016-06-14T10:23:20Z

← Older revision		Revision as of 12:23, 14 June 2016
Line 1:		Line 1:
	The CompCert C compiler guarantees that the target program behaves as the source program. Yet, source		The CompCert C compiler guarantees that the target program behaves as the source program. Yet, source programs without a defined semantics do not benefit from this guarantee and could therefore be miscompiled. To reduce the possibility of a miscompilation, we propose a novel memory model for CompCert which gives a defined semantics to challenging features such as bitwise pointer arithmetics and access to uninitialised data.
	programs without a defined semantics do not benefit from this guarantee and could therefore be miscompiled.
	To reduce the possibility of a miscompilation, we propose a novel memory model for CompCert which gives a
	defined semantics to challenging features such as bitwise pointer arithmetics and access to uninitialised data.

	We evaluate our memory model both theoretically and experimentally. In our experiments, we identify pervasive		We evaluate our memory model both theoretically and experimentally. In our experiments, we identify pervasive low-level C idioms that require the additional expressiveness provided by our memory model. We also show that our memory model provably subsumes the existing CompCert memory model thus cross-validating both semantics.
	low-level C idioms that require the additional expressiveness provided by our memory model. We also show
	that our memory model provably subsumes the existing CompCert memory model thus cross-validating both semantics.

	Our memory model relies on the core concepts of symbolic value and normalisation. A symbolic value models		Our memory model relies on the core concepts of symbolic value and normalisation. A symbolic value models a delayed computation and the normalisation turns, when possible, a symbolic value into a genuine value. We show how to tame the expressive power of the normalisation so that the memory model fits the proof framework of CompCert. We also adapt the proofs of correctness of the compiler passes performed by CompCert, thus demonstrating that our model is well-suited for proving compiler transformations.
	a delayed computation and the normalisation turns, when possible, a symbolic value into a genuine value.
	We show how to tame the expressive power of the normalisation so that the memory model fits the proof
	framework of CompCert. We also adapt the proofs of correctness of the compiler passes performed by CompCert,
	thus demonstrating that our model is well-suited for proving compiler transformations.

Sandrine: Created page with "The CompCert C compiler guarantees that the target program behaves as the source program. Yet, source programs without a defined semantics do not benefit from this guarantee..."

2016-06-14T10:22:20Z

Created page with "The CompCert C compiler guarantees that the target program behaves as the source program. Yet, source programs without a defined semantics do not benefit from this guarantee..."

New page

The CompCert C compiler guarantees that the target program behaves as the source program. Yet, source
programs without a defined semantics do not benefit from this guarantee and could therefore be miscompiled.
To reduce the possibility of a miscompilation, we propose a novel memory model for CompCert which gives a
defined semantics to challenging features such as bitwise pointer arithmetics and access to uninitialised data.

We evaluate our memory model both theoretically and experimentally. In our experiments, we identify pervasive
low-level C idioms that require the additional expressiveness provided by our memory model. We also show
that our memory model provably subsumes the existing CompCert memory model thus cross-validating both semantics.

Our memory model relies on the core concepts of symbolic value and normalisation. A symbolic value models
a delayed computation and the normalisation turns, when possible, a symbolic value into a genuine value.
We show how to tame the expressive power of the normalisation so that the memory model fits the proof
framework of CompCert. We also adapt the proofs of correctness of the compiler passes performed by CompCert,
thus demonstrating that our model is well-suited for proving compiler transformations.