Skip to content

Commit

Permalink
Got test2 working in 32-bit mode
Browse files Browse the repository at this point in the history
  • Loading branch information
andrew-appel committed Jul 26, 2024
1 parent 13b0cdf commit 60bb838
Show file tree
Hide file tree
Showing 9 changed files with 179 additions and 188 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/coq-action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ jobs:
make_target: test3
- bit_size: 32
make_target: test4
- bit_size: 64
- bit_size: 32
make_target: test5

steps:
Expand Down
3 changes: 2 additions & 1 deletion progs/dry_mem_lemmas.v
Original file line number Diff line number Diff line change
Expand Up @@ -867,7 +867,8 @@ Definition main_pre_juicy {Z} prog (ora : Z) gv (x' : rmap * {ts : list Type & u
necR (fst x') phi1*) /\ joins (ghost_of (m_phi m)) [Some (ext_ref z, NoneP)]).

Definition xtype_of_option_typ (t: option typ) : xtype :=
match t with Some t => AST.Tret t | None => AST.Tvoid end.
match t with Some t => inj_type t | None => Xvoid end.


Definition main_post_juicy {Z} prog (ora : Z) gv (x' : rmap * {ts : list Type & unit})
(ge_s: extspec.injective_PTree block) (tret : option typ) ret (z : Z) (m : juicy_mem) :=
Expand Down
16 changes: 8 additions & 8 deletions progs/io_combine.v
Original file line number Diff line number Diff line change
Expand Up @@ -118,7 +118,7 @@ Proof.
destruct i1.
destruct (zeq _ _); subst; try discriminate.
destruct (sys_putc_spec _) eqn:Hspec; inv H3.
assert (sig_res (ef_sig e) <> AST.Tvoid).
assert (sig_res (ef_sig e) <> AST.Xvoid).
{ destruct e; inv H2; discriminate. }
eapply sys_putc_correct in Hspec as (? & -> & [? Hpost ?]); eauto.
rewrite Harg. unfold Vubyte. f_equal.
Expand All @@ -130,7 +130,7 @@ Proof.
rewrite if_true in H3 by auto.
unfold sys_getc_wrap_spec in *.
destruct (sys_getc_spec) eqn:Hspec; inv H3.
assert (sig_res (ef_sig e) <> AST.Tvoid).
assert (sig_res (ef_sig e) <> AST.Xvoid).
{ destruct e; inv H4; discriminate. }
eapply (sys_getc_correct _ _ m) in Hspec as (? & -> & [? Hpost ? ?]); eauto.
* split; auto; do 2 eexists; eauto.
Expand Down Expand Up @@ -165,8 +165,8 @@ Definition trace_set := @trace (@io_events.IO_event nat) unit * RData -> Prop.
forall n t (traces : trace_set) z s0 c m e args,
cl_at_external c = Some (e,args) ->
(forall s s' ret m' t' n'
(Hargsty : Val.has_type_list args (sig_args (ef_sig e)))
(Hretty : Builtins0.val_opt_has_xtype ret (sig_res (ef_sig e))),
(Hargsty : Val.has_type_list args (map proj_xtype (sig_args (ef_sig e))))
(Hretty : Builtins0.val_opt_has_rettype ret (sig_res (ef_sig e))),
IO_inj_mem e args m t s ->
IO_ext_sem e args s = Some (s', ret, t') ->
m' = OS_mem e args m s' ->
Expand All @@ -176,8 +176,8 @@ Definition trace_set := @trace (@io_events.IO_event nat) unit * RData -> Prop.
OS_safeN_trace n' (app_trace t t') traces' z' s' c' m' /\
(forall t'' sf, traces' (t'', sf) -> traces (app_trace t' t'', sf))) ->
(forall t1, traces t1 ->
exists s s' ret m' t' n', Val.has_type_list args (sig_args (ef_sig e)) /\
Builtins0.val_opt_has_xtype ret (sig_res (ef_sig e)) /\
exists s s' ret m' t' n', Val.has_type_list args (map proj_xtype (sig_args (ef_sig e))) /\
Builtins0.val_opt_has_rettype ret (sig_res (ef_sig e)) /\
IO_inj_mem e args m t s /\ IO_ext_sem e args s = Some (s', ret, t') /\ m' = OS_mem e args m s' /\
(n' <= n)%nat /\ valid_trace s' /\ exists traces' z' c', consume_trace z z' t' /\
cl_after_external ret c = Some c' /\ OS_safeN_trace n' (app_trace t t') traces' z' s' c' m' /\
Expand Down Expand Up @@ -340,8 +340,8 @@ Local Ltac destruct_spec Hspec :=
- edestruct IHn as (traces' & ? & ?); eauto.
do 2 eexists; eauto.
eapply OS_safeN_trace_step; eauto.
- exists (fun t1 => exists s s' ret m' t' n', Val.has_type_list args (sig_args (ef_sig e)) /\
Builtins0.val_opt_has_xtype ret (sig_res (ef_sig e)) /\
- exists (fun t1 => exists s s' ret m' t' n', Val.has_type_list args (map proj_xtype (sig_args (ef_sig e))) /\
Builtins0.val_opt_has_rettype ret (sig_res (ef_sig e)) /\
IO_inj_mem e args m t s /\ IO_ext_sem e args s = Some (s', ret, t') /\ m' = OS_mem e args m s' /\
(n' <= n0)%nat /\ valid_trace s' /\ exists traces' z' c', consume_trace z z' t' /\
cl_after_external ret q = Some c' /\ OS_safeN_trace n' (app_trace t t') traces' z' s' c' m' /\
Expand Down
4 changes: 2 additions & 2 deletions progs/io_dry.v
Original file line number Diff line number Diff line change
Expand Up @@ -54,11 +54,11 @@ Proof.
+ destruct X as (m0 & _ & w).
destruct X1; [|exact False].
destruct v; [exact False | | exact False | exact False | exact False | exact False].
exact (ot <> AST.Tvoid /\ putchar_post m0 X3 i w X2).
exact (ot <> AST.Xvoid /\ putchar_post m0 X3 i w X2).
+ destruct X as (m0 & _ & w).
destruct X1; [|exact False].
destruct v; [exact False | | exact False | exact False | exact False | exact False].
exact (ot <> AST.Tvoid /\ getchar_post m0 X3 i w X2).
exact (ot <> AST.Xvoid /\ getchar_post m0 X3 i w X2).
- intros; exact True.
Defined.

Expand Down
Loading

0 comments on commit 60bb838

Please sign in to comment.