diff options
author | Thomas Letan <lthms@soap.coffee> | 2020-12-08 15:08:37 +0100 |
---|---|---|
committer | Thomas Letan <lthms@soap.coffee> | 2020-12-08 15:08:37 +0100 |
commit | 26b5fbf22ef2245f01048dcf2085417030e469b8 (patch) | |
tree | 1d9e957bd1c4c8bce5f1787ada09ec3a14601c68 /site | |
parent | Announce coq-coqffi.1.0.0~beta1 (diff) |
Update to CompCert 3.8
Diffstat (limited to 'site')
-rw-r--r-- | site/posts/ClightIntroduction.v | 44 |
1 files changed, 13 insertions, 31 deletions
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 #<a
- href="http://compcert.inria.fr/doc/index.html">#CompCert documentation#</a>#
- 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 #<a
- href="https://github.com/PrincetonUniversity/VST">#VST#</a># 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 #<a
+ href="http://compcert.inria.fr/doc/index.html">#CompCert
+ documentation#</a># 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 #<a
+ href="https://github.com/PrincetonUniversity/VST">#VST#</a>#
+ project is very interesting, as its main purpose is to provide
+ tools to reason about Clight programs more easily. *)
|