summaryrefslogtreecommitdiffstats
path: root/site/posts
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-12-08 15:08:37 +0100
committerThomas Letan <lthms@soap.coffee>2020-12-08 15:08:37 +0100
commit26b5fbf22ef2245f01048dcf2085417030e469b8 (patch)
tree1d9e957bd1c4c8bce5f1787ada09ec3a14601c68 /site/posts
parentc42518f0b23529e432f007ce37c83615eab14d8f (diff)
Update to CompCert 3.8
Diffstat (limited to 'site/posts')
-rw-r--r--site/posts/ClightIntroduction.v44
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. *)