Skip to content

Commit 962f50e

Browse files
febyejifebyeji
committed
Apply code reviews
1 parent fbfa855 commit 962f50e

File tree

3 files changed

+66
-83
lines changed

3 files changed

+66
-83
lines changed

‎ArchSem/GenPromising.v‎

Lines changed: 10 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -398,33 +398,24 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
398398
st ← mGet;
399399
(* Find out next possible promises or terminating states at the current thread *)
400400
executions ←
401-
for (tid : fin n) in enum (fin n) do
401+
vmapM (λ '(tid, ts),
402402
'(promises_per_tid, tstates_per_tid) ←
403403
mlift $ prom.(enumerate_promises_and_terminal_states)
404-
fuel_per_tid tid (term tid) (initmem st) (tstate tid st) (events st);
405-
mret (map (λ ev, (ev, tid)) promises_per_tid, tstates_per_tid)
406-
end;
407-
404+
fuel_per_tid (fin_to_nat tid) (term tid) (initmem st) ts (events st);
405+
mret (map (.,tid) promises_per_tid, tstates_per_tid)
406+
) (venumerate (tstates st));
408407
(* Compute cartesian products of the possible thread states *)
409-
let tstates_sys :=
410-
fold_left (λ partial_sts tstates_tid,
411-
List.flat_map (λ tstate,
412-
if is_emptyb partial_sts then [[tstate]]
413-
else map (λ partial_st, partial_st ++ [tstate]) partial_sts
414-
) tstates_tid
415-
) (map snd executions) [] in
408+
let tstates_all := cprodn (vmap snd executions) in
416409
let new_finals :=
417410
omap (λ tstates,
418-
if (list_to_vec_n n tstates) is Some tstates_vec then
419-
let st := Make tstates_vec st.(PState.initmem) st.(PState.events) in
420-
if decide $ terminated prom term st is left pt
421-
then Some (make_final st pt)
422-
else None
411+
let st := Make tstates st.(PState.initmem) st.(PState.events) in
412+
if decide $ terminated prom term st is left pt
413+
then Some (make_final st pt)
423414
else None
424-
) tstates_sys in
415+
) tstates_all in
425416

426417
(* Non-deterministically choose the next promise and the tid for pruning *)
427-
let promises_all := List.concat (map fst executions) in
418+
let promises_all := List.concat executions.*1 in
428419
if is_emptyb promises_all then
429420
mret (new_finals ++ finals)
430421
else

‎ArchSemArm/UMPromising.v‎

Lines changed: 25 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -478,10 +478,7 @@ Definition write_mem (tid : nat) (loc : Loc.t) (vdata : view)
478478
mSet $ TState.update_coh loc time;;
479479
mSet $ TState.update TState.vwr time;;
480480
mSet $ TState.update TState.vrel (view_if is_release time);;
481-
mret $ match new_promise with
482-
| true => (mem, time, Some vpre)
483-
| false => (mem, time, None)
484-
end.
481+
mret $ if (new_promise : bool) then (mem, time, Some vpre) else (mem, time, None).
485482

486483
(** Tries to perform a memory write.
487484
@@ -536,11 +533,13 @@ End IIS.
536533
and computation. This can mutate memory because it will append a write at
537534
the end of memory the corresponding event was not already promised. *)
538535
Section RunOutcome.
539-
Context (tid : nat) (initmem : memoryMap).
536+
Context (mem_update : bool).
537+
Context (tid : nat).
538+
Context (initmem : memoryMap).
540539

541-
Equations run_outcome (out : outcome) (mem_update : bool) :
540+
Equations run_outcome (out : outcome) :
542541
Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out * option view) :=
543-
| RegWrite reg racc val, mem_update =>
542+
| RegWrite reg racc val =>
544543
guard_or "Non trivial reg access types unsupported" (racc = None);;
545544
vreg ← mget (IIS.strict ∘ PPState.iis);
546545
vreg' ←
@@ -554,14 +553,14 @@ Section RunOutcome.
554553
TState.set_reg reg (val, vreg') ts;
555554
msetv PPState.state nts;;
556555
mret ((), None)
557-
| RegRead reg racc, mem_update =>
556+
| RegRead reg racc =>
558557
guard_or "Non trivial reg access types unsupported" (racc = None);;
559558
ts ← mget PPState.state;
560559
'(val, view) ← othrow "Register isn't mapped can't read" $
561560
dmap_lookup reg ts.(TState.regs);
562561
mset PPState.iis $ IIS.add view;;
563562
mret (val, None)
564-
| MemRead (MemReq.make macc addr addr_space 8 0), mem_update =>
563+
| MemRead (MemReq.make macc addr addr_space 8 0) =>
565564
guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
566565
loc ← othrow "PA not supported" $ Loc.from_addr addr;
567566
if is_ifetch macc then
@@ -575,17 +574,17 @@ Section RunOutcome.
575574
mset PPState.iis $ IIS.add view;;
576575
mret (Ok (val, bv_0 0), None)
577576
else mthrow "Read is not explicit or ifetch"
578-
| MemRead (MemReq.make macc addr addr_space 4 0), mem_update => (* ifetch *)
577+
| MemRead (MemReq.make macc addr addr_space 4 0) => (* ifetch *)
579578
guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
580579
let initmem := Memory.initial_from_memMap initmem in
581580
opcode ← Exec.liftSt PPState.mem $ read_mem4 addr macc initmem;
582581
mret (Ok (opcode, 0%bv), None)
583-
| MemRead _, mem_update => mthrow "Memory read of size other than 8 and 4"
584-
| MemWriteAddrAnnounce _, mem_update =>
582+
| MemRead _ => mthrow "Memory read of size other than 8 and 4"
583+
| MemWriteAddrAnnounce _ =>
585584
vaddr ← mget (IIS.strict ∘ PPState.iis);
586585
mset PPState.state $ TState.update TState.vcap vaddr;;
587586
mret ((), None)
588-
| MemWrite (MemReq.make macc addr addr_space 8 0) val tags, mem_update =>
587+
| MemWrite (MemReq.make macc addr addr_space 8 0) val tags =>
589588
guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
590589
addr ← othrow "PA not supported" $ Loc.from_addr addr;
591590
if is_explicit macc then
@@ -596,7 +595,7 @@ Section RunOutcome.
596595
msetv PPState.mem mem;;
597596
mret (Ok (), vpre_opt)
598597
else mthrow "Unsupported non-explicit write"
599-
| Barrier (Barrier_DMB dmb), mem_update => (* dmb *)
598+
| Barrier (Barrier_DMB dmb) => (* dmb *)
600599
ts ← mget PPState.state;
601600
match dmb.(DxB_types) with
602601
| MBReqTypes_All (* dmb sy *) =>
@@ -607,16 +606,16 @@ Section RunOutcome.
607606
mset PPState.state $ TState.update TState.vdmbst ts.(TState.vwr)
608607
end;;
609608
mret ((), None)
610-
| Barrier (Barrier_ISB ()), mem_update => (* isb *)
609+
| Barrier (Barrier_ISB ()) => (* isb *)
611610
ts ← mget PPState.state;
612611
mset PPState.state $ TState.update TState.visb (TState.vcap ts);;
613612
mret ((), None)
614-
| GenericFail s, mem_update => mthrow ("Instruction failure: " ++ s)%string
615-
| _, _ => mthrow "Unsupported outcome".
613+
| GenericFail s => mthrow ("Instruction failure: " ++ s)%string
614+
| _ => mthrow "Unsupported outcome".
616615

617616
Definition run_outcome' (out : outcome) :
618617
Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out) :=
619-
run_outcome out true |$> fst.
618+
run_outcome out |$> fst.
620619
End RunOutcome.
621620

622621
Module CProm.
@@ -655,14 +654,17 @@ Section ComputeProm.
655654
(base : view)
656655
(out : outcome) :
657656
Exec.t (CProm.t * PPState.t TState.t Msg.t IIS.t) string (eff_ret out) :=
658-
'(res, vpre_opt) ← Exec.liftSt snd $ run_outcome tid initmem out true;
657+
'(res, vpre_opt) ← Exec.liftSt snd $ run_outcome true tid initmem out;
659658
if vpre_opt is Some vpre then
660659
mem ← mget (PPState.mem ∘ snd);
661660
mset fst (CProm.add_if mem vpre base);;
662661
mret res
663662
else
664663
mret res.
665664

665+
(* Run the thread state until termination, collecting certifiable promises.
666+
Returns true if termination occurs within the given fuel,
667+
false otherwise. *)
666668
Fixpoint run_to_termination_promise
667669
(isem : iMon ())
668670
(fuel : nat)
@@ -694,12 +696,6 @@ Section ComputeProm.
694696
(∀ r ∈ res, r.2 = true);;
695697
mret $ (CProm.proms (union_list res.*1.*1), []).
696698

697-
Definition run_outcome_with_no_promise
698-
(out : outcome) :
699-
Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out) :=
700-
'(res, _) ← run_outcome tid initmem out false;
701-
mret res.
702-
703699
Fixpoint run_to_termination_no_promise
704700
(isem : iMon ())
705701
(fuel : nat) :
@@ -709,7 +705,7 @@ Section ComputeProm.
709705
ts ← mget PPState.state;
710706
mret (term (TState.reg_map ts))
711707
| S fuel =>
712-
let handler := run_outcome_with_no_promise in
708+
let handler := run_outcome' false tid initmem in
713709
cinterp handler isem;;
714710
ts ← mget PPState.state;
715711
if term (TState.reg_map ts) then
@@ -755,7 +751,7 @@ Definition UMPromising_nocert' : PromisingModel :=
755751
iis_init := IIS.init;
756752
address_space := PAS_NonSecure;
757753
mEvent := Msg.t;
758-
handler := run_outcome';
754+
handler := run_outcome' true;
759755
allowed_promises := allowed_promises_nocert;
760756
emit_promise := λ tid initmem mem msg, TState.promise (length mem);
761757
memory_snapshot :=
@@ -770,7 +766,7 @@ Definition UMPromising_nocert isem :=
770766

771767
Definition seq_step (isem : iMon ()) (tid : nat) (initmem : memoryMap)
772768
: relation (TState.t * Memory.t) :=
773-
let handler := run_outcome' tid initmem in
769+
let handler := run_outcome' true tid initmem in
774770
λ '(ts, mem) '(ts', mem'),
775771
(ts', mem') ∈
776772
PPState.state ×× PPState.mem
@@ -795,7 +791,7 @@ Definition UMPromising_cert' (isem : iMon ()) : PromisingModel :=
795791
iis_init := IIS.init;
796792
address_space := PAS_NonSecure;
797793
mEvent := Msg.t;
798-
handler := run_outcome';
794+
handler := run_outcome' true;
799795
allowed_promises := allowed_promises_cert isem;
800796
emit_promise := λ tid initmem mem msg, TState.promise (length mem);
801797
memory_snapshot :=

‎ArchSemArm/VMPromising.v‎

Lines changed: 31 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1588,10 +1588,7 @@ Definition write_mem (tid : nat) (loc : Loc.t) (viio : view)
15881588
mset fst $ TState.update_coh loc time;;
15891589
mset fst $ TState.update TState.vwr time;;
15901590
mset fst $ TState.update TState.vrel (view_if is_release time);;
1591-
match new_promise with
1592-
| true => mret (time, Some vpre)
1593-
| false => mret (time, None)
1594-
end.
1591+
mret $ if (new_promise : bool) then (time, Some vpre) else (time, None).
15951592

15961593
(** Tries to perform a memory write.
15971594
@@ -1834,32 +1831,34 @@ Definition run_take_exception (fault : exn) (vmax_t : view) :
18341831

18351832
(** Runs an outcome. *)
18361833
Section RunOutcome.
1837-
Context (tid : nat) (initmem : memoryMap).
1834+
Context (mem_update : bool).
1835+
Context (tid : nat).
1836+
Context (initmem : memoryMap).
18381837

1839-
Equations run_outcome (out : outcome) (mem_update : bool) :
1838+
Equations run_outcome (out : outcome) :
18401839
Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out * option view) :=
1841-
| RegRead reg racc, mem_update =>
1840+
| RegRead reg racc =>
18421841
val ← Exec.liftSt (PPState.state ×× PPState.iis) $ (run_reg_read reg racc);
18431842
mret (val, None)
1844-
| RegWrite reg racc val, mem_update =>
1843+
| RegWrite reg racc val =>
18451844
run_reg_write reg racc val;;
18461845
mret ((), None)
1847-
| MemRead (MemReq.make macc addr addr_space 8 0), mem_update =>
1846+
| MemRead (MemReq.make macc addr addr_space 8 0) =>
18481847
guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
18491848
let initmem := Memory.initial_from_memMap initmem in
18501849
val ← run_mem_read addr macc initmem;
18511850
mret (Ok (val, 0%bv), None)
1852-
| MemRead (MemReq.make macc addr addr_space 4 0), mem_update => (* ifetch *)
1851+
| MemRead (MemReq.make macc addr addr_space 4 0) => (* ifetch *)
18531852
guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
18541853
let initmem := Memory.initial_from_memMap initmem in
18551854
opcode ← Exec.liftSt PPState.mem $ run_mem_read4 addr macc initmem;
18561855
mret (Ok (opcode, 0%bv), None)
1857-
| MemRead _, mem_update => mthrow "Memory read of size other than 8 or 4, or with tags"
1858-
| MemWriteAddrAnnounce _, mem_update =>
1856+
| MemRead _ => mthrow "Memory read of size other than 8 or 4, or with tags"
1857+
| MemWriteAddrAnnounce _ =>
18591858
vaddr ← mget (IIS.strict ∘ PPState.iis);
18601859
mset PPState.state $ TState.update TState.vspec vaddr;;
18611860
mret ((), None)
1862-
| MemWrite (MemReq.make macc addr addr_space 8 0) val _, mem_update =>
1861+
| MemWrite (MemReq.make macc addr addr_space 8 0) val _ =>
18631862
guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
18641863
addr ← othrow "Address not supported" $ Loc.from_addr addr;
18651864
viio ← mget (IIS.strict ∘ PPState.iis);
@@ -1871,36 +1870,36 @@ Section RunOutcome.
18711870
write_mem_xcl tid addr viio invalidation macc val mem_update;
18721871
mret (Ok (), vpre_opt)
18731872
else mthrow "Unsupported non-explicit write"
1874-
| MemWrite _ _ _, mem_update => mthrow "Memory write of size other than 8, or with tags"
1875-
| Barrier barrier, mem_update =>
1873+
| MemWrite _ _ _ => mthrow "Memory write of size other than 8, or with tags"
1874+
| Barrier barrier =>
18761875
mem ← mget PPState.mem;
18771876
Exec.liftSt (PPState.state ×× PPState.iis) $ run_barrier barrier (length mem);;
18781877
mret ((), None)
1879-
| TlbOp tlbi, mem_update =>
1878+
| TlbOp tlbi =>
18801879
viio ← mget (IIS.strict ∘ PPState.iis);
18811880
run_tlbi tid viio tlbi;;
18821881
mret ((), None)
1883-
| ReturnException, mem_update =>
1882+
| ReturnException =>
18841883
mem ← mget PPState.mem;
18851884
Exec.liftSt (PPState.state ×× PPState.iis) $ run_cse (length mem);;
18861885
mret ((), None)
1887-
| TranslationStart trans_start, mem_update =>
1886+
| TranslationStart trans_start =>
18881887
let initmem := Memory.initial_from_memMap initmem in
18891888
run_trans_start trans_start tid initmem;;
18901889
mret ((), None)
1891-
| TranslationEnd trans_end, mem_update =>
1890+
| TranslationEnd trans_end =>
18921891
Exec.liftSt (PPState.state ×× PPState.iis) $ run_trans_end trans_end;;
18931892
mret ((), None)
1894-
| GenericFail s, mem_update => mthrow ("Instruction failure: " ++ s)%string
1895-
| TakeException fault, mem_update =>
1893+
| GenericFail s => mthrow ("Instruction failure: " ++ s)%string
1894+
| TakeException fault =>
18961895
mem ← mget PPState.mem;
18971896
Exec.liftSt (PPState.state ×× PPState.iis) $ run_take_exception fault (length mem);;
18981897
mret ((), None)
1899-
| _, mem_update => mthrow "Unsupported outcome".
1898+
| _ => mthrow "Unsupported outcome".
19001899

19011900
Definition run_outcome' (out : outcome) :
19021901
Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
1903-
run_outcome out true |$> fst.
1902+
run_outcome out |$> fst.
19041903
End RunOutcome.
19051904

19061905
Module CProm.
@@ -1939,14 +1938,17 @@ Section ComputeProm.
19391938
(base : view)
19401939
(out : outcome) :
19411940
Exec.t (CProm.t * PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
1942-
'(res, vpre_opt) ← Exec.liftSt snd $ run_outcome tid initmem out true;
1941+
'(res, vpre_opt) ← Exec.liftSt snd $ run_outcome true tid initmem out;
19431942
if vpre_opt is Some vpre then
19441943
mem ← mget (PPState.mem ∘ snd);
19451944
mset fst (CProm.add_if mem vpre base);;
19461945
mret res
19471946
else
19481947
mret res.
19491948

1949+
(* Run the thread state until termination, collecting certifiable promises.
1950+
Returns true if termination occurs within the given fuel,
1951+
false otherwise. *)
19501952
Fixpoint run_to_termination_promise
19511953
(isem : iMon ())
19521954
(fuel : nat)
@@ -1978,12 +1980,6 @@ Section ComputeProm.
19781980
(∀ r ∈ res, r.2 = true);;
19791981
mret $ (CProm.proms (union_list res.*1.*1), []).
19801982

1981-
Definition run_outcome_with_no_promise
1982-
(out : outcome) :
1983-
Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
1984-
'(res, _) ← run_outcome tid initmem out false;
1985-
mret res.
1986-
19871983
Fixpoint run_to_termination_no_promise
19881984
(isem : iMon ())
19891985
(fuel : nat) :
@@ -1993,7 +1989,7 @@ Section ComputeProm.
19931989
ts ← mget PPState.state;
19941990
mret (term (TState.reg_map ts))
19951991
| S fuel =>
1996-
let handler := run_outcome_with_no_promise in
1992+
let handler := run_outcome' false tid initmem in
19971993
cinterp handler isem;;
19981994
ts ← mget PPState.state;
19991995
if term (TState.reg_map ts) then
@@ -2040,7 +2036,7 @@ Definition VMPromising_nocert' : PromisingModel :=
20402036
address_space := PAS_NonSecure;
20412037
mEvent := Ev.t;
20422038
allowed_promises := allowed_promises_nocert;
2043-
handler := run_outcome';
2039+
handler := run_outcome' true;
20442040
emit_promise := λ tid initmem mem msg, TState.promise (length mem);
20452041
memory_snapshot :=
20462042
λ initmem, Memory.to_memMap (Memory.initial_from_memMap initmem);
@@ -2051,7 +2047,7 @@ Definition VMPromising_nocert isem :=
20512047

20522048
Definition seq_step (isem : iMon ()) (tid : nat) (initmem : memoryMap)
20532049
: relation (TState.t * Memory.t) :=
2054-
let handler := run_outcome' tid initmem in
2050+
let handler := run_outcome' true tid initmem in
20552051
λ '(ts, mem) '(ts', mem'),
20562052
(ts', mem') ∈
20572053
PPState.state ×× PPState.mem
@@ -2068,7 +2064,7 @@ Definition allowed_promises_cert (isem : iMon ()) tid (initmem : memoryMap)
20682064
]}.
20692065

20702066

2071-
Definition VMPromising_cert' (isem : iMon ()) : PromisingModel :=
2067+
Definition VMPromising_cert' (isem : iMon ()) : PromisingModel :=
20722068
{|tState := TState.t;
20732069
tState_init := λ tid, TState.init;
20742070
tState_regs := TState.reg_map;
@@ -2077,7 +2073,7 @@ Definition VMPromising_cert' (isem : iMon ()) : PromisingModel :=
20772073
iis_init := IIS.init;
20782074
address_space := PAS_NonSecure;
20792075
mEvent := Ev.t;
2080-
handler := run_outcome';
2076+
handler := run_outcome' true;
20812077
allowed_promises := allowed_promises_cert isem;
20822078
emit_promise := λ tid initmem mem msg, TState.promise (length mem);
20832079
memory_snapshot :=

0 commit comments

Comments
 (0)