Skip to content

Commit

Permalink
in progress
Browse files Browse the repository at this point in the history
  • Loading branch information
@songyahui
songyahui committed May 9, 2024
1 parent 79ea5b3 commit 50abc19
Show file tree
Hide file tree
Showing 4 changed files with 50 additions and 49 deletions.
27 changes: 20 additions & 7 deletions parsing/forward_rules.ml
View file
Expand Up @@ -479,12 +479,14 @@ let rec resolveInnerTryCatches typ env (match_summary:tryCatchLemma option) (spe
in

let spec_body'= normalize_spec (NormalReturn(pi, heap)::spec_body) in
(*
print_endline ("--------\n spec_body' " ^ string_of_normalisedStagedSpec spec_body');
print_endline ("\n handler:' " ^ string_of_handlingcases (h_n, h_eff)^"\n");

*)
let phi1, _ = handling_spec typ env match_summary spec_body' h_n h_eff in
(*
print_endline ("--------\n phi1 " ^ string_of_disj_spec phi1 ^"\n");

*)
let res =
List.map
(fun phi1_spec_body ->
Expand All @@ -502,10 +504,13 @@ let rec resolveInnerTryCatches typ env (match_summary:tryCatchLemma option) (spe
in


print_endline ("returns are " ^ string_of_term ret ^ " " ^ string_of_term ret');

let phi1_spec_body' = (NormalReturn (Atomic(EQ, ret,ret' ), EmptyHeap)) :: phi1_spec_body in
(*
print_endline ("returns are " ^ string_of_term ret ^ " " ^ string_of_term ret');
print_endline ("--------\n phi1' " ^ string_of_spec phi1_spec_body' ^"\n");
*)

phi1_spec_body'
)
Expand Down Expand Up @@ -578,7 +583,9 @@ and handling_spec typ env (match_summary:tryCatchLemma option) (scr_spec:normali

| (TryCatchStage _) :: _ ->

(*
print_endline ("unresolved try catch");
*)
let prefix = effectStage2Spec scr_eff_stages in
let ret = verifier_getAfreeVar "res" in
let (stage:stagedSpec) = TryCatch(True, EmptyHeap, (prefix, (h_norm, h_ops)), Var ret) in
Expand Down Expand Up @@ -652,8 +659,9 @@ and handling_spec typ env (match_summary:tryCatchLemma option) (scr_spec:normali
*)
let bindings = bindFormalNActual (effFormalArg) (effActualArg@[x.e_ret]) in

(*
print_endline (string_of_effHOTryCatchStages (EffHOStage x) ^ " # " ^ string_of_spec_list handledContinuation);

*)
let contiRet = findTheActualArg4Acc_x_e_ret x.e_ret handledContinuation in


Expand All @@ -665,12 +673,13 @@ and handling_spec typ env (match_summary:tryCatchLemma option) (scr_spec:normali



(*
print_endline ("\nhandling_spec " ^ (string_of_spec (normalisedStagedSpec2Spec scr_spec)));
print_endline ("prefix: \n" ^ string_of_spec (normalStage2Spec norm) ^"\n");
print_endline ("Final results lower case: \n" ^ string_of_spec_list instantiate_tcl_summary ^"\n");

*)

instantiate_tcl_summary, env

Expand All @@ -682,7 +691,9 @@ and handling_spec typ env (match_summary:tryCatchLemma option) (scr_spec:normali
if String.compare label "continue" == 0 then [(normalisedStagedSpec2Spec scr_spec)], env
else
(
(*
print_endline ("no lemma provided for " ^ label );
*)
let prefix = effectStage2Spec scr_eff_stages in
let ret = verifier_getAfreeVar "res" in
let (stage:stagedSpec) = TryCatch(True, EmptyHeap, (prefix, (h_norm, h_ops)), Var ret) in
Expand Down Expand Up @@ -726,8 +737,9 @@ and handling_spec typ env (match_summary:tryCatchLemma option) (scr_spec:normali
let handler_body_specAfterSubstituteK = resolveInnerTryCatches typ env match_summary handler_body_specAfterSubstituteK in


(*
print_endline ("handlerbodyAfterSubstituteK: " ^ string_of_spec_list handler_body_specAfterSubstituteK);

*)

let res = concatenateEventWithSpecs (normalStage2Spec norm) ( handler_body_specAfterSubstituteK) in

Expand Down Expand Up @@ -1036,9 +1048,10 @@ let rec infer_of_expression (env:fvenv) (history:disj_spec) (expr:core_lang): di
in
*)

(*
print_endline (string_of_core_lang scr) ;
(print_endline (string_of_handlingcases (inferred_val_case, inferred_branch_specs)));

*)
let phi1, env = infer_of_expression env [freshNormalReturnSpec] scr in

(*
Expand Down
1 change: 0 additions & 1 deletion src/demo/2_Inductive_Sum.ml
View file
Expand Up @@ -30,7 +30,6 @@ let test1 ()
= handler 5



let test2 ()
(*@ ex i; Norm(i-> 55 /\ res=10, res) @*)
= handler 10
Expand Down
37 changes: 9 additions & 28 deletions src/demo/7_amb.ml
View file
Expand Up @@ -18,29 +18,22 @@ let rec iter (f) (xs)
| [] -> ()
| h::t -> f h; iter f t

(*@ predicate h (a, r) =
Norm (head_r=false)
\/
Norm (head_r=true)
@*)
(*@ predicate h (r) =
Norm (head_r=false) \/ Norm (head_r=true) @*)

(*@ predicate containRetTrue (xs, c, r) =
ex r; Norm(is_nil(xs)=true/\res=r /\ r=false/\ c =0 )
\/ ex r1 h t r; ens head(xs)=h/\tail(xs)=t/\is_cons(xs)=true; Norm(c = 1 /\ head_r=true /\ res=r /\ r=true)
\/ ex r1 h t; ens head(xs)=h/\tail(xs)=t/\is_cons(xs)=true;
Norm(head_r=false); ex r c'; containRetTrue (t,c',r) ; Norm(c = c'+1 /\ res=r)
@*)
Norm(head_r=false); ex r c'; containRetTrue (t,c',r) ; Norm(c = c'+1 /\ res=r) @*)

let helperk hh
(*@
ex hret;
try ex hr2; continue_syh (k, head_r, hr2); ex hr3; Success(emp, hr2, hr3)
(*@ ex hret; try ex hr2; continue_syh (k, head_r, hr2); ex hr3; Success(emp, hr2, hr3)
catch {
x -> Norm(res=())
| (Success x) -> ex hkr; Success(emp, x, hkr)
| (Failure x) -> Norm(res=())
}[hret]
@*)
}[hret] @*)
= match
(*let k = Obj.clone_continuation k in*)
let r1 = h () in
Expand All @@ -52,26 +45,19 @@ let helperk hh
| x -> ()

let aux k xs
(*@
ex r; Failure(xs=[], (404), r)
\/
ex hr;
try
ex h t hret; ens head(xs)=h/\tail(xs)=t/\is_cons(xs)=true;
ex hret;
(*@ ex r; Failure(xs=[], (404), r) \/ ex hr; try
ex h t hret; ens head(xs)=h/\tail(xs)=t/\is_cons(xs)=true; ex hret;
try ex hr2; continue_syh (k, head_r, hr2); ex hr3; Success(emp, hr2, hr3)
catch {
x -> Norm(res=())
| (Success x) -> ex hkr; Success(emp, x, hkr)
| (Failure x) -> Norm(res=())
}[hret]
;
ex r2; iter(helperk, t, r2); ex r; Failure(emp, (404), r)
; ex r2; iter(helperk, t, r2); ex r; Failure(emp, (404), r)
catch {
x -> ens res=x
| (Success r) -> ens res=r
}[hr]
@*)
}[hr] @*)
=
match iter (helperk) xs; perform (Failure 404) with
| effect (Success r) k1 -> r
Expand Down Expand Up @@ -111,11 +97,6 @@ ex r c a r1; req counter -> a; containRetTrue (xs, c, r1); ens counter->a+c /\ r
| x -> x
| effect (Choose xs) k -> aux k xs



(*
*)

(*
let branch_example_generic (xs: (unit -> bool) list) counter : int
= handle xs counter
Expand Down
34 changes: 21 additions & 13 deletions src/demo/8_schduler.ml
View file
Expand Up @@ -15,6 +15,7 @@ let yield ()
(*@ ex r; Yield(emp, r); Norm(res=r) @*)
= perform Yield

(* seperation logic predicates are starting with a ~ *)
(*@ ~predicate any_queue(queue, m)
= ex q; queue->q /\ effNo(q) = m /\ m>=0 @*)

Expand All @@ -24,18 +25,29 @@ let yield ()
(*@ ~predicate empty_queue(queue)
= ex q; queue->q /\ effNo(q) = 0 @*)


let queue_create () = ref ([], [])

let queue_push ele queue
(*@ ex mm mm' w inter; req any_queue(queue, mm);
Norm(non_empty_queue(queue, mm') /\ effNo(ele)=w /\ w >0 /\ mm'=mm+w /\ res=inter /\ inter=()) @*)
(*@
ex m m' q q'; req queue->q /\ effNo(q) = m /\ m>=0;
ens queue->q' /\ effNo(q') = m' /\ m'>0 /\ effNo(ele)=w /\ w >0 /\ m'=m+w /\ res=()
@*)
= let (front, back) = !queue in
queue := (front, ele::back)

(* ex mm mm' w inter; req any_queue(queue, mm);
Norm(non_empty_queue(queue, mm') /\ effNo(ele)=w /\ w >0 /\ mm'=mm+w /\ res=inter /\ inter=()) *)
let enqueue ele queue
(*@
ex m m' q q'; req queue->q /\ effNo(q) = m /\ m>=0;
ens queue->q' /\ effNo(q') = m' /\ m'>0 /\ effNo(ele)=w /\ w >0 /\ m'=m+w /\ res=()
@*)
= queue_push ele queue

(*
let queue_is_empty queue
(*@ ex inter; req empty_queue(queue); Norm(empty_queue(queue) /\ res=inter /\ inter=true)
\/ ex m inter; req non_empty_queue(queue, m); Norm(non_empty_queue(queue, m) /\ res=inter /\ inter=false) @*)
(*@ ex inter; req empty_queue(queue); Norm(empty_queue(queue) /\ res=true /\ inter=true)
\/ ex m inter; req non_empty_queue(queue, m); Norm(non_empty_queue(queue, m) /\ res=false) @*)
= let (front, back) = !queue in
List.length front = 0 && List.length back = 0
Expand All @@ -61,17 +73,14 @@ let queue_pop queue
queue := (newfront, []);
h)
let enqueue f run_q
(*@ ex r; queue_push(f, run_q, r); Norm(res=r) @*)
= queue_push f run_q

let wrapPop run_q
(*@ ex f; queue_pop (run_q, f); Norm (res=f)@*)
= queue_pop run_q
let dequeue run_q
(*@ queue_is_empty(run_q, true); Norm(res=())
\/ ex m m' w f cr; req non_empty_queue(run_q, m);
\/ queue_is_empty(run_q, false);
ex m m' w f cr; req non_empty_queue(run_q, m);
Norm(any_queue(run_q, m') /\ effNo(f) =w /\ w >0 /\ m'+w=m );
continue (f, (), cr); Norm(res=cr)
@*)
Expand All @@ -81,7 +90,6 @@ let dequeue run_q
continue f ()

(*@ predicate f(arg) =
ex r; Norm(effNo(f) = 0 /\ r = () /\ res=r)
\/
Expand Down Expand Up @@ -110,7 +118,8 @@ let rec spawn f run_q
enqueue k run_q;
spawn f' run_q

*)
(*
(* A concurrent round-robin scheduler *)
let run main
(*@ ex queue q r; Norm (queue->q /\ effNo(q)=0 /\ res = r /\ r = ()) @*)
Expand All @@ -124,7 +133,6 @@ let task name () =
Printf.printf "ending %s\n%!" name;
()
(*
let main () =
(*let pa = fork (task "a") in
let _pb = fork (task "b") in
Expand Down

0 comments on commit 50abc19

Please sign in to comment.