Commit 2c54350f authored by Hai Dang's avatar Hai Dang

add comments to code

parent fb4a36a8
...@@ -7,13 +7,29 @@ Set Default Proof Using "Type". ...@@ -7,13 +7,29 @@ Set Default Proof Using "Type".
(* Assuming x : &mut i32 *) (* Assuming x : &mut i32 *)
Definition ex1_unopt : function := Definition ex1_unopt : function :=
fun: ["i"], 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 ;; 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"] [] ;; Call #[ScFnPtr "f"] [] ;;
(* Write 42 to the cell pointed to by the pointer in "x" *)
*{int} "x" <- #[42] ;; *{int} "x" <- #[42] ;;
Call #[ScFnPtr "g"] [] ;; Call #[ScFnPtr "g"] [] ;;
(* Read the value "v" from the cell pointed to by the pointer in "x" *)
let: "v" := Copy *{int} "x" in let: "v" := Copy *{int} "x" in
(* Free the local variable *)
Free "x" ;; Free "x" ;;
(* Finally, return the read value *)
"v" "v"
. .
...@@ -58,7 +74,7 @@ Proof. ...@@ -58,7 +74,7 @@ Proof.
(* Write local *) (* Write local *)
sim_apply sim_simple_write_local; [solve_sim..|]. sim_apply sim_simple_write_local; [solve_sim..|].
intros s ?. simplify_eq. intros s ?. simplify_eq.
(* Call *) (* Call unknown function *)
sim_apply sim_simple_let=>/=. sim_apply sim_simple_let=>/=.
sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|]. sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
intros rf frs frt ??? ? _ _ FREL. simplify_eq/=. intros rf frs frt ??? ? _ _ FREL. simplify_eq/=.
...@@ -85,7 +101,7 @@ Proof. ...@@ -85,7 +101,7 @@ Proof.
(* We can go back to simple mode! *) (* We can go back to simple mode! *)
eapply (sim_simplify (fun_post_simple c)). { by eauto. } eapply (sim_simplify (fun_post_simple c)). { by eauto. }
simplify_eq/=. clear- AREL FREL LOOK. simplify_eq/=. clear- AREL FREL LOOK.
(* Call *) (* Call unknown function *)
sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|]. sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
intros rf' frs' frt' ??? ? _ _ FREL'. simplify_eq/=. intros rf' frs' frt' ??? ? _ _ FREL'. simplify_eq/=.
apply: sim_simple_result. simpl. apply: sim_simple_result. simpl.
......
...@@ -9,11 +9,23 @@ Set Default Proof Using "Type". ...@@ -9,11 +9,23 @@ Set Default Proof Using "Type".
(* Assuming x : &mut i32 *) (* Assuming x : &mut i32 *)
Definition ex1_down_unopt : function := Definition ex1_down_unopt : function :=
fun: ["i"], 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 ;; 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 let: "v" := Copy *{int} "x" in
(* The unknown code is represented by a call to an unknown function "f" *)
Call #[ScFnPtr "f"] [] ;; Call #[ScFnPtr "f"] [] ;;
(* Free the local variable *)
Free "x" ;; Free "x" ;;
(* Finally, return the read value *)
"v" "v"
. .
......
...@@ -8,11 +8,24 @@ Set Default Proof Using "Type". ...@@ -8,11 +8,24 @@ Set Default Proof Using "Type".
(* Assuming x : & i32 *) (* Assuming x : & i32 *)
Definition ex2_unopt : function := Definition ex2_unopt : function :=
fun: ["i"], fun: ["i"],
(* "x" is the local variable that stores the pointer value "i" *)
let: "x" := new_place (& int) "i" in 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 ;; 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"] ;; 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 let: "v" := Copy *{int} "x" in
(* Free the local variable *)
Free "x" ;; Free "x" ;;
(* Finally, return the read value *)
"v" "v"
. .
......
...@@ -9,11 +9,24 @@ Set Default Proof Using "Type". ...@@ -9,11 +9,24 @@ Set Default Proof Using "Type".
(* Assuming x : & i32 *) (* Assuming x : & i32 *)
Definition ex2_down_unopt : function := Definition ex2_down_unopt : function :=
fun: ["i"], fun: ["i"],
(* "x" is the local variable that stores the pointer value "i" *)
let: "x" := new_place (& int) "i" in 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 ;; 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 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"] ;; Call #[ScFnPtr "f"] [Copy "x"] ;;
(* Free the local variable *)
Free "x" ;; Free "x" ;;
(* Finally, return the read value *)
"v" "v"
. .
......
...@@ -9,12 +9,26 @@ Set Default Proof Using "Type". ...@@ -9,12 +9,26 @@ Set Default Proof Using "Type".
(* Assuming x : &mut i32 *) (* Assuming x : &mut i32 *)
Definition ex3_unopt : function := Definition ex3_unopt : function :=
fun: ["i"], fun: ["i"],
(* "x" is the local variable that stores the pointer value "i" *)
let: "x" := new_place (&mut int) "i" in 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 ;; retag_place "x" (RefPtr Mutable) int FnEntry ;;
(* Write 42 to the cell pointed to by the pointer in "x" *)
*{int} "x" <- #[42] ;; *{int} "x" <- #[42] ;;
(* The unknown code is represented by a call to an unknown function "f" *)
let: "v" := Call #[ScFnPtr "f"] [] in let: "v" := Call #[ScFnPtr "f"] [] in
(* Write 13 to the cell pointed to by the pointer in "x" *)
*{int} "x" <- #[13] ;; *{int} "x" <- #[13] ;;
(* Free the local variable *)
Free "x" ;; Free "x" ;;
(* Finally, return the value *)
"v" "v"
. .
......
...@@ -9,12 +9,26 @@ Set Default Proof Using "Type". ...@@ -9,12 +9,26 @@ Set Default Proof Using "Type".
(* Assuming x : &mut i32 *) (* Assuming x : &mut i32 *)
Definition ex3_down_unopt : function := Definition ex3_down_unopt : function :=
fun: ["i"], fun: ["i"],
(* "x" is the local variable that stores the pointer value "i" *)
let: "x" := new_place (&mut int) "i" in 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 ;; retag_place "x" (RefPtr Mutable) int FnEntry ;;
(* Write 42 to the cell pointed to by the pointer in "x" *)
*{int} "x" <- #[42] ;; *{int} "x" <- #[42] ;;
(* The unknown code is represented by a call to an unknown function "f" *)
let: "v" := Call #[ScFnPtr "f"] [] in let: "v" := Call #[ScFnPtr "f"] [] in
(* Write 13 to the cell pointed to by the pointer in "x" *)
*{int} "x" <- #[13] ;; *{int} "x" <- #[13] ;;
(* Free the local variable *)
Free "x" ;; Free "x" ;;
(* Finally, return the value *)
"v" "v"
. .
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment