From 2c54350fd517cc4cf614afe5aa3831cc77b18662 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang
Date: Fri, 20 Sep 2019 10:29:53 +0200
Subject: [PATCH] add comments to code
---
theories/opt/ex1.v | 22 +++++++++++++++++++---
theories/opt/ex1_down.v | 14 +++++++++++++-
theories/opt/ex2.v | 13 +++++++++++++
theories/opt/ex2_down.v | 13 +++++++++++++
theories/opt/ex3.v | 14 ++++++++++++++
theories/opt/ex3_down.v | 14 ++++++++++++++
6 files changed, 86 insertions(+), 4 deletions(-)
diff --git a/theories/opt/ex1.v b/theories/opt/ex1.v
index 188aec6..8b917ad 100644
--- a/theories/opt/ex1.v
+++ b/theories/opt/ex1.v
@@ -7,13 +7,29 @@ Set Default Proof Using "Type".
(* Assuming x : &mut i32 *)
Definition ex1_unopt : function :=
fun: ["i"],
- let: "x" := new_place (&mut int) "i" in (* put argument into place *)
+ (* "x" is the local variable that stores the pointer value "i" *)
+ let: "x" := new_place (&mut int) "i" in
+
+ (* retag_place reborrows the pointer value stored in "x" (which is "i"),
+ then updates "x" with the new pointer value *)
retag_place "x" (RefPtr Mutable) int Default ;;
+
+ (* The unknown code is represented by a call to an unknown function "f" or
+ "g" *)
Call #[ScFnPtr "f"] [] ;;
+
+ (* Write 42 to the cell pointed to by the pointer in "x" *)
*{int} "x" <- #[42] ;;
+
Call #[ScFnPtr "g"] [] ;;
+
+ (* Read the value "v" from the cell pointed to by the pointer in "x" *)
let: "v" := Copy *{int} "x" in
+
+ (* Free the local variable *)
Free "x" ;;
+
+ (* Finally, return the read value *)
"v"
.
@@ -58,7 +74,7 @@ Proof.
(* Write local *)
sim_apply sim_simple_write_local; [solve_sim..|].
intros s ?. simplify_eq.
- (* Call *)
+ (* Call unknown function *)
sim_apply sim_simple_let=>/=.
sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
intros rf frs frt ??? ? _ _ FREL. simplify_eq/=.
@@ -85,7 +101,7 @@ Proof.
(* We can go back to simple mode! *)
eapply (sim_simplify (fun_post_simple c)). { by eauto. }
simplify_eq/=. clear- AREL FREL LOOK.
- (* Call *)
+ (* Call unknown function *)
sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
intros rf' frs' frt' ??? ? _ _ FREL'. simplify_eq/=.
apply: sim_simple_result. simpl.
diff --git a/theories/opt/ex1_down.v b/theories/opt/ex1_down.v
index 6ae5e49..44bd8eb 100644
--- a/theories/opt/ex1_down.v
+++ b/theories/opt/ex1_down.v
@@ -9,11 +9,23 @@ Set Default Proof Using "Type".
(* Assuming x : &mut i32 *)
Definition ex1_down_unopt : function :=
fun: ["i"],
- let: "x" := new_place (&mut int) "i" in (* put argument into place *)
+ (* "x" is the local variable that stores the pointer value "i" *)
+ let: "x" := new_place (&mut int) "i" in
+
+ (* retag_place reborrows the pointer value stored in "x" (which is "i"),
+ then updates "x" with the new pointer value *)
retag_place "x" (RefPtr Mutable) int FnEntry ;;
+
+ (* Read the value "v" from the cell pointed to by the pointer in "x" *)
let: "v" := Copy *{int} "x" in
+
+ (* The unknown code is represented by a call to an unknown function "f" *)
Call #[ScFnPtr "f"] [] ;;
+
+ (* Free the local variable *)
Free "x" ;;
+
+ (* Finally, return the read value *)
"v"
.
diff --git a/theories/opt/ex2.v b/theories/opt/ex2.v
index e6310fe..82354e1 100644
--- a/theories/opt/ex2.v
+++ b/theories/opt/ex2.v
@@ -8,11 +8,24 @@ Set Default Proof Using "Type".
(* Assuming x : & i32 *)
Definition ex2_unopt : function :=
fun: ["i"],
+ (* "x" is the local variable that stores the pointer value "i" *)
let: "x" := new_place (& int) "i" in
+
+ (* retag_place reborrows the pointer value stored in "x" (which is "i"),
+ then updates "x" with the new pointer value *)
retag_place "x" (RefPtr Immutable) int Default ;;
+
+ (* The unknown code is represented by a call to an unknown function "f",
+ which does take the pointer value from "x" as an argument. *)
Call #[ScFnPtr "f"] [Copy "x"] ;;
+
+ (* Read the value "v" from the cell pointed to by the pointer in "x" *)
let: "v" := Copy *{int} "x" in
+
+ (* Free the local variable *)
Free "x" ;;
+
+ (* Finally, return the read value *)
"v"
.
diff --git a/theories/opt/ex2_down.v b/theories/opt/ex2_down.v
index fb82160..45c19d8 100644
--- a/theories/opt/ex2_down.v
+++ b/theories/opt/ex2_down.v
@@ -9,11 +9,24 @@ Set Default Proof Using "Type".
(* Assuming x : & i32 *)
Definition ex2_down_unopt : function :=
fun: ["i"],
+ (* "x" is the local variable that stores the pointer value "i" *)
let: "x" := new_place (& int) "i" in
+
+ (* retag_place reborrows the pointer value stored in "x" (which is "i"),
+ then updates "x" with the new pointer value *)
retag_place "x" (RefPtr Immutable) int FnEntry ;;
+
+ (* Read the value "v" from the cell pointed to by the pointer in "x" *)
let: "v" := Copy *{int} "x" in
+
+ (* The unknown code is represented by a call to an unknown function "f",
+ which does take the pointer value from "x" as an argument. *)
Call #[ScFnPtr "f"] [Copy "x"] ;;
+
+ (* Free the local variable *)
Free "x" ;;
+
+ (* Finally, return the read value *)
"v"
.
diff --git a/theories/opt/ex3.v b/theories/opt/ex3.v
index 87f748e..1d9413f 100644
--- a/theories/opt/ex3.v
+++ b/theories/opt/ex3.v
@@ -9,12 +9,26 @@ Set Default Proof Using "Type".
(* Assuming x : &mut i32 *)
Definition ex3_unopt : function :=
fun: ["i"],
+ (* "x" is the local variable that stores the pointer value "i" *)
let: "x" := new_place (&mut int) "i" in
+
+ (* retag_place reborrows the pointer value stored in "x" (which is "i"),
+ then updates "x" with the new pointer value *)
retag_place "x" (RefPtr Mutable) int FnEntry ;;
+
+ (* Write 42 to the cell pointed to by the pointer in "x" *)
*{int} "x" <- #[42] ;;
+
+ (* The unknown code is represented by a call to an unknown function "f" *)
let: "v" := Call #[ScFnPtr "f"] [] in
+
+ (* Write 13 to the cell pointed to by the pointer in "x" *)
*{int} "x" <- #[13] ;;
+
+ (* Free the local variable *)
Free "x" ;;
+
+ (* Finally, return the value *)
"v"
.
diff --git a/theories/opt/ex3_down.v b/theories/opt/ex3_down.v
index e5ef4f0..94d266d 100644
--- a/theories/opt/ex3_down.v
+++ b/theories/opt/ex3_down.v
@@ -9,12 +9,26 @@ Set Default Proof Using "Type".
(* Assuming x : &mut i32 *)
Definition ex3_down_unopt : function :=
fun: ["i"],
+ (* "x" is the local variable that stores the pointer value "i" *)
let: "x" := new_place (&mut int) "i" in
+
+ (* retag_place reborrows the pointer value stored in "x" (which is "i"),
+ then updates "x" with the new pointer value *)
retag_place "x" (RefPtr Mutable) int FnEntry ;;
+
+ (* Write 42 to the cell pointed to by the pointer in "x" *)
*{int} "x" <- #[42] ;;
+
+ (* The unknown code is represented by a call to an unknown function "f" *)
let: "v" := Call #[ScFnPtr "f"] [] in
+
+ (* Write 13 to the cell pointed to by the pointer in "x" *)
*{int} "x" <- #[13] ;;
+
+ (* Free the local variable *)
Free "x" ;;
+
+ (* Finally, return the value *)
"v"
.
--
GitLab