aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/Asmexpand.ml2
-rw-r--r--cfrontend/C2C.ml2
-rw-r--r--cfrontend/Cexec.v5
-rw-r--r--cfrontend/PrintClight.ml2
-rw-r--r--cfrontend/PrintCsyntax.ml4
-rw-r--r--common/Events.v84
-rw-r--r--common/PrintAST.ml1
-rw-r--r--ia32/Asmexpand.ml2
-rw-r--r--powerpc/Asmexpand.ml2
9 files changed, 47 insertions, 57 deletions
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 5415f78e..47269f8f 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -440,4 +440,4 @@ let expand_fundef id = function
Errors.OK (External ef)
let expand_program (p: Asm.program) : Asm.program Errors.res =
- AST.transform_partial_ident_program expand_fundef p
+ AST.transform_partial_program2 expand_fundef (fun id v -> Errors.OK v) p
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index e4001e6b..418fa702 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -1090,6 +1090,7 @@ let convertFundef loc env fd =
(** External function declaration *)
let re_builtin = Str.regexp "__builtin_"
+let re_runtime = Str.regexp "__i64_"
let convertFundecl env (sto, id, ty, optinit) =
let (args, res, cconv) =
@@ -1102,6 +1103,7 @@ let convertFundecl env (sto, id, ty, optinit) =
let ef =
if id.name = "malloc" then EF_malloc else
if id.name = "free" then EF_free else
+ if Str.string_match re_runtime id.name 0 then EF_runtime(id'', sg) else
if Str.string_match re_builtin id.name 0
&& List.mem_assoc id.name builtins.functions
then EF_builtin(id'', sg)
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 7e966ffe..36f7bf7d 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -536,6 +536,7 @@ Definition do_external (ef: external_function):
match ef with
| EF_external name sg => do_external_function name sg ge
| EF_builtin name sg => do_external_function name sg ge
+ | EF_runtime name sg => do_external_function name sg ge
| EF_vload chunk => do_ef_volatile_load chunk
| EF_vstore chunk => do_ef_volatile_store chunk
| EF_malloc => do_ef_malloc
@@ -558,6 +559,8 @@ Proof with try congruence.
eapply do_external_function_sound; eauto.
(* EF_builtin *)
eapply do_external_function_sound; eauto.
+(* EF_runtime *)
+ eapply do_external_function_sound; eauto.
(* EF_vload *)
unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs...
mydestr. destruct p as [[w'' t''] v]; mydestr.
@@ -604,6 +607,8 @@ Proof.
eapply do_external_function_complete; eauto.
(* EF_builtin *)
eapply do_external_function_complete; eauto.
+(* EF_runtime *)
+ eapply do_external_function_complete; eauto.
(* EF_vload *)
inv H; unfold do_ef_volatile_load.
exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto.
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index ed19e178..42892901 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -258,7 +258,7 @@ let print_function p id f =
let print_fundef p id fd =
match fd with
- | External(EF_external(_,_), args, res, cconv) ->
+ | External((EF_external _ | EF_runtime _), args, res, cconv) ->
fprintf p "extern %s;@ @ "
(name_cdecl (extern_atom id) (Tfunction(args, res, cconv)))
| External(_, _, _, _) ->
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index bb6576aa..d5853e38 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -264,6 +264,8 @@ let rec expr p (prec, e) =
(camlstring_of_coqstring txt) exprlist (false, args)
| Ebuiltin(EF_external(id, sg), _, args, _) ->
fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args)
+ | Ebuiltin(EF_runtime(id, sg), _, args, _) ->
+ fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args)
| Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) ->
extended_asm p txt None args clob
| Ebuiltin(EF_debug(kind,txt,_),_,args,_) ->
@@ -427,7 +429,7 @@ let print_function p id f =
let print_fundef p id fd =
match fd with
- | External(EF_external(_,_), args, res, cconv) ->
+ | External((EF_external _ | EF_runtime _), args, res, cconv) ->
fprintf p "extern %s;@ @ "
(name_cdecl (extern_atom id) (Tfunction(args, res, cconv)))
| External(_, _, _, _) ->
diff --git a/common/Events.v b/common/Events.v
index 7029a984..040029fb 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -619,9 +619,7 @@ Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop :=
(** The semantics is invariant under change of global environment that preserves symbols. *)
ec_symbols_preserved:
forall ge1 ge2 vargs m1 t vres m2,
- (forall id, Senv.find_symbol ge2 id = Senv.find_symbol ge1 id) ->
- (forall id, Senv.public_symbol ge2 id = Senv.public_symbol ge1 id) ->
- (forall b, Senv.block_is_volatile ge2 b = Senv.block_is_volatile ge1 b) ->
+ Senv.equiv ge1 ge2 ->
sem ge1 vargs m1 t vres m2 ->
sem ge2 vargs m1 t vres m2;
@@ -704,17 +702,15 @@ Inductive volatile_load_sem (chunk: memory_chunk) (ge: Senv.t):
Lemma volatile_load_preserved:
forall ge1 ge2 chunk m b ofs t v,
- (forall id, Senv.find_symbol ge2 id = Senv.find_symbol ge1 id) ->
- (forall id, Senv.public_symbol ge2 id = Senv.public_symbol ge1 id) ->
- (forall b, Senv.block_is_volatile ge2 b = Senv.block_is_volatile ge1 b) ->
+ Senv.equiv ge1 ge2 ->
volatile_load ge1 chunk m b ofs t v ->
volatile_load ge2 chunk m b ofs t v.
Proof.
- intros. inv H2; constructor; auto.
- rewrite H1; auto.
- rewrite H; auto.
+ intros. destruct H as (A & B & C). inv H0; constructor; auto.
+ rewrite C; auto.
+ rewrite A; auto.
eapply eventval_match_preserved; eauto.
- rewrite H1; auto.
+ rewrite C; auto.
Qed.
Lemma volatile_load_extends:
@@ -773,7 +769,7 @@ Proof.
- unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type.
eapply Mem.load_type; eauto.
(* symbols *)
-- inv H2. constructor. eapply volatile_load_preserved; eauto.
+- inv H0. constructor. eapply volatile_load_preserved; eauto.
(* valid blocks *)
- inv H; auto.
(* max perms *)
@@ -817,17 +813,15 @@ Inductive volatile_store_sem (chunk: memory_chunk) (ge: Senv.t):
Lemma volatile_store_preserved:
forall ge1 ge2 chunk m1 b ofs v t m2,
- (forall id, Senv.find_symbol ge2 id = Senv.find_symbol ge1 id) ->
- (forall id, Senv.public_symbol ge2 id = Senv.public_symbol ge1 id) ->
- (forall b, Senv.block_is_volatile ge2 b = Senv.block_is_volatile ge1 b) ->
+ Senv.equiv ge1 ge2 ->
volatile_store ge1 chunk m1 b ofs v t m2 ->
volatile_store ge2 chunk m1 b ofs v t m2.
Proof.
- intros. inv H2; constructor; auto.
- rewrite H1; auto.
- rewrite H; auto.
+ intros. destruct H as (A & B & C). inv H0; constructor; auto.
+ rewrite C; auto.
+ rewrite A; auto.
eapply eventval_match_preserved; eauto.
- rewrite H1; auto.
+ rewrite C; auto.
Qed.
Lemma volatile_store_readonly:
@@ -925,7 +919,7 @@ Proof.
(* well typed *)
- unfold proj_sig_res; simpl. inv H; constructor.
(* symbols preserved *)
-- inv H2. constructor. eapply volatile_store_preserved; eauto.
+- inv H0. constructor. eapply volatile_store_preserved; eauto.
(* valid block *)
- inv H. inv H1. auto. eauto with mem.
(* perms *)
@@ -972,19 +966,18 @@ Proof.
Mem.store Mint32 m' b (-4) (Vint n) = Some m'' ->
Mem.unchanged_on P m m'').
{
- intros; constructor; intros.
- - split; intros; eauto with mem.
- - assert (b0 <> b) by (eapply Mem.valid_not_valid_diff; eauto with mem).
- erewrite Mem.store_mem_contents; eauto. rewrite Maps.PMap.gso by auto.
- Local Transparent Mem.alloc. unfold Mem.alloc in H. injection H; intros A B.
- rewrite <- B; simpl. rewrite A. rewrite Maps.PMap.gso by auto. auto.
+ intros.
+ apply Mem.unchanged_on_implies with (fun b1 ofs1 => b1 <> b).
+ apply Mem.unchanged_on_trans with m'.
+ eapply Mem.alloc_unchanged_on; eauto.
+ eapply Mem.store_unchanged_on; eauto.
+ intros. eapply Mem.valid_not_valid_diff; eauto with mem.
}
-
constructor; intros.
(* well typed *)
- inv H. unfold proj_sig_res; simpl. auto.
(* symbols preserved *)
-- inv H2; econstructor; eauto.
+- inv H0; econstructor; eauto.
(* valid block *)
- inv H. eauto with mem.
(* perms *)
@@ -1045,7 +1038,7 @@ Proof.
(* well typed *)
- inv H. unfold proj_sig_res. simpl. auto.
(* symbols preserved *)
-- inv H2; econstructor; eauto.
+- inv H0; econstructor; eauto.
(* valid block *)
- inv H. eauto with mem.
(* perms *)
@@ -1124,7 +1117,7 @@ Proof.
- (* return type *)
intros. inv H. constructor.
- (* change of globalenv *)
- intros. inv H2. econstructor; eauto.
+ intros. inv H0. econstructor; eauto.
- (* valid blocks *)
intros. inv H. eauto with mem.
- (* perms *)
@@ -1235,7 +1228,7 @@ Proof.
(* well typed *)
- inv H. simpl. auto.
(* symbols *)
-- inv H2. econstructor; eauto.
+- destruct H as (A & B & C). inv H0. econstructor; eauto.
eapply eventval_list_match_preserved; eauto.
(* valid blocks *)
- inv H; auto.
@@ -1280,7 +1273,7 @@ Proof.
(* well typed *)
- inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto.
(* symbols *)
-- inv H2. econstructor; eauto.
+- destruct H as (A & B & C). inv H0. econstructor; eauto.
eapply eventval_match_preserved; eauto.
(* valid blocks *)
- inv H; auto.
@@ -1324,7 +1317,7 @@ Proof.
(* well typed *)
- inv H. simpl. auto.
(* symbols *)
-- inv H2. econstructor; eauto.
+- inv H0. econstructor; eauto.
(* valid blocks *)
- inv H; auto.
(* perms *)
@@ -1351,8 +1344,9 @@ Qed.
(** ** Semantics of external functions. *)
-(** For functions defined outside the program ([EF_external] and [EF_builtin]),
- we do not define their semantics, but only assume that it satisfies
+(** For functions defined outside the program ([EF_external],
+ [EF_builtin] and [EF_runtime]), we do not define their
+ semantics, but only assume that it satisfies
[extcall_properties]. *)
Parameter external_functions_sem: String.string -> signature -> extcall_sem.
@@ -1384,6 +1378,7 @@ Definition external_call (ef: external_function): extcall_sem :=
match ef with
| EF_external name sg => external_functions_sem name sg
| EF_builtin name sg => external_functions_sem name sg
+ | EF_runtime name sg => external_functions_sem name sg
| EF_vload chunk => volatile_load_sem chunk
| EF_vstore chunk => volatile_store_sem chunk
| EF_malloc => extcall_malloc_sem
@@ -1402,6 +1397,7 @@ Proof.
intros. unfold external_call, ef_sig; destruct ef.
apply external_functions_properties.
apply external_functions_properties.
+ apply external_functions_properties.
apply volatile_load_ok.
apply volatile_store_ok.
apply extcall_malloc_ok.
@@ -1414,7 +1410,7 @@ Proof.
Qed.
Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef).
-Definition external_call_symbols_preserved_gen ef := ec_symbols_preserved (external_call_spec ef).
+Definition external_call_symbols_preserved ef := ec_symbols_preserved (external_call_spec ef).
Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef).
Definition external_call_max_perm ef := ec_max_perm (external_call_spec ef).
Definition external_call_readonly ef := ec_readonly (external_call_spec ef).
@@ -1424,20 +1420,6 @@ Definition external_call_trace_length ef := ec_trace_length (external_call_spec
Definition external_call_receptive ef := ec_receptive (external_call_spec ef).
Definition external_call_determ ef := ec_determ (external_call_spec ef).
-(** Special cases of [external_call_symbols_preserved_gen]. *)
-
-Lemma external_call_symbols_preserved:
- forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2,
- external_call ef ge1 vargs m1 t vres m2 ->
- (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
- (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) ->
- (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) ->
- external_call ef ge2 vargs m1 t vres m2.
-Proof.
- intros. apply external_call_symbols_preserved_gen with (ge1 := ge1); auto.
- intros. simpl. unfold Genv.block_is_volatile. rewrite H2. auto.
-Qed.
-
(** Corollary of [external_call_valid_block]. *)
Lemma external_call_nextblock:
@@ -1596,9 +1578,7 @@ Qed.
Lemma external_call_symbols_preserved':
forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2,
external_call' ef ge1 vargs m1 t vres m2 ->
- (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
- (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) ->
- (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) ->
+ Senv.equiv ge1 ge2 ->
external_call' ef ge2 vargs m1 t vres m2.
Proof.
intros. inv H. exists v; auto. eapply external_call_symbols_preserved; eauto.
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 39481bfb..766f586b 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -39,6 +39,7 @@ let name_of_chunk = function
let name_of_external = function
| EF_external(name, sg) -> sprintf "extern %S" (camlstring_of_coqstring name)
| EF_builtin(name, sg) -> sprintf "builtin %S" (camlstring_of_coqstring name)
+ | EF_runtime(name, sg) -> sprintf "runtime %S" (camlstring_of_coqstring name)
| EF_vload chunk -> sprintf "volatile load %s" (name_of_chunk chunk)
| EF_vstore chunk -> sprintf "volatile store %s" (name_of_chunk chunk)
| EF_malloc -> "malloc"
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index 7ca31902..61beeb00 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -460,4 +460,4 @@ let expand_fundef id = function
Errors.OK (External ef)
let expand_program (p: Asm.program) : Asm.program Errors.res =
- AST.transform_partial_ident_program expand_fundef p
+ AST.transform_partial_program2 expand_fundef (fun id v -> Errors.OK v) p
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 7af27d20..dad19a6d 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -792,4 +792,4 @@ let expand_fundef id = function
Errors.OK (External ef)
let expand_program (p: Asm.program) : Asm.program Errors.res =
- AST.transform_partial_ident_program expand_fundef p
+ AST.transform_partial_program2 expand_fundef (fun id v -> Errors.OK v) p
generated by cgit (git 2.34.1) at 2024-06-02 16:08:45 +0000