From 26b5fbf22ef2245f01048dcf2085417030e469b8 Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Tue, 8 Dec 2020 15:08:37 +0100 Subject: Update to CompCert 3.8 --- site/posts/ClightIntroduction.v | 44 ++++++++++++----------------------------- 1 file changed, 13 insertions(+), 31 deletions(-) (limited to 'site/posts/ClightIntroduction.v') diff --git a/site/posts/ClightIntroduction.v b/site/posts/ClightIntroduction.v index 13bf773..f9feefb 100644 --- a/site/posts/ClightIntroduction.v +++ b/site/posts/ClightIntroduction.v @@ -326,24 +326,9 @@ res_equ : sem_cast res tint tint m1 = Some (Vint z) >> - [res_equ] is the equation which says that the result of [f_add] is - [res], after it has been cast as a [tint] value + [res], after it has been cast as a [tint] value. - Surprisingly, neither [add_op] nor [res_equ] can be reduced easily… After - some digging, I have found that this is because both rely on [Archi.ptr64], - which is basically opaque as far as reduction strategies are concerned. - - Now, there are probably more elegant (idiomatic) way to deal with this - issue, but a working approach is to unfold until [Archi.ptr64] appears, then - use the [Archi.splitlong_ptr32] lemma to replace it with its value - ([false]). *) - - unfold sem_binarith in *. - cbn in *. - unfold sem_cast in *. - cbn in *. - rewrite Archi.splitlong_ptr32 in *; auto. - -(** We can now simplify [add_op] and [res_equ], and this allows us to + We can simplify [add_op] and [res_equ], and this allows us to conclude. *) smart_inv add_op. @@ -353,17 +338,14 @@ Qed. (** ** Conclusion *) -(** The main difficulty of this exercise was the opaqueness of [Archi.ptr64]; - this is surprising, since it means my struggle was technical, not - conceptual. On the contrary, the definitions of Clight are easy to - understand, and the ##CompCert documentation## - is very pleasant to read. - - Understanding Clight and its semantics can be very interesting if you are - working on a language that you want to translate into machine code. However, - proving functional properties of a given C snippet using only CompCert can - quickly become cumbersome. From this perspective, the ##VST## project is very - interesting, as its main purpose is to provide tools to reason about Clight - programs more easily. *) +(** The definitions of Clight are easy to understand, and the ##CompCert + documentation## is very pleasant to read. Understanding + Clight and its semantics can be very interesting if you are + working on a language that you want to translate into machine + code. However, proving functional properties of a given C snippet + using only CompCert can quickly become cumbersome. From this + perspective, the ##VST## + project is very interesting, as its main purpose is to provide + tools to reason about Clight programs more easily. *) -- cgit v1.2.3