diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CMtypecheck.ml | 18 | ||||
-rw-r--r-- | backend/Cminor.v | 24 | ||||
-rw-r--r-- | backend/PrintCminor.ml | 11 | ||||
-rw-r--r-- | backend/RTL.v | 2 | ||||
-rw-r--r-- | backend/Selection.v | 3 | ||||
-rw-r--r-- | backend/Selectionproof.v | 10 |
6 files changed, 66 insertions, 2 deletions
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index e3a6f704..244a73f0 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -90,6 +90,7 @@ let type_unary_operation = function | Ocast8unsigned -> tint, tint | Ocast16unsigned -> tint, tint | Onegint -> tint, tint + | Oboolval -> tint, tint | Onotbool -> tint, tint | Onotint -> tint, tint | Onegf -> tfloat, tfloat @@ -134,6 +135,7 @@ let name_of_unary_operation = function | Ocast8unsigned -> "cast8unsigned" | Ocast16unsigned -> "cast16unsigned" | Onegint -> "negint" + | Oboolval -> "notbool" | Onotbool -> "notbool" | Onotint -> "notint" | Onegf -> "negf" @@ -293,6 +295,22 @@ let rec type_stmt env blk ret s = with Error s -> raise (Error (sprintf "In call:\n%s" s)) end + | Sbuiltin(optid, ef, el) -> + let sg = ef_sig ef in + let tel = type_exprlist env [] el in + begin try + unify_list (ty_of_sig_args sg.sig_args) tel; + let ty_res = + match sg.sig_res with + | None -> tint (*???*) + | Some t -> ty_of_typ t in + begin match optid with + | None -> () + | Some id -> unify (type_var env id) ty_res + end + with Error s -> + raise (Error (sprintf "In builtin call:\n%s" s)) + end | Sseq(s1, s2) -> type_stmt env blk ret s1; type_stmt env blk ret s2 diff --git a/backend/Cminor.v b/backend/Cminor.v index c9ee5b5c..6d288a9e 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -44,6 +44,7 @@ Inductive unary_operation : Type := | Ocast8signed: unary_operation (**r 8-bit sign extension *) | Ocast16unsigned: unary_operation (**r 16-bit zero extension *) | Ocast16signed: unary_operation (**r 16-bit sign extension *) + | Oboolval: unary_operation (**r 0 if null, 1 if non-null *) | Onegint: unary_operation (**r integer opposite *) | Onotbool: unary_operation (**r boolean negation *) | Onotint: unary_operation (**r bitwise complement *) @@ -103,6 +104,7 @@ Inductive stmt : Type := | Sstore : memory_chunk -> expr -> expr -> stmt | Scall : option ident -> signature -> expr -> list expr -> stmt | Stailcall: signature -> expr -> list expr -> stmt + | Sbuiltin : option ident -> external_function -> list expr -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: expr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -228,6 +230,7 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val := | Ocast8signed => Some (Val.sign_ext 8 arg) | Ocast16unsigned => Some (Val.zero_ext 16 arg) | Ocast16signed => Some (Val.sign_ext 16 arg) + | Oboolval => Some(Val.boolval arg) | Onegint => Some (Val.negint arg) | Onotbool => Some (Val.notbool arg) | Onotint => Some (Val.notint arg) @@ -401,6 +404,12 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) E0 (Callstate fd vargs (call_cont k) m') + | step_builtin: forall f optid ef bl k sp e m vargs t vres m', + eval_exprlist sp e m bl vargs -> + external_call ef ge vargs m t vres m' -> + step (State f (Sbuiltin optid ef bl) k sp e m) + t (State f Sskip k sp (set_optvar optid vres e) m') + | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) @@ -505,9 +514,11 @@ Proof. intros. subst. inv H0. exists s1; auto. inversion H; subst; auto. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + exists (State f Sskip k sp (set_optvar optid vres2 e) m2). econstructor; eauto. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate vres2 k m2). econstructor; eauto. (* trace length *) - inv H; simpl; try omega. eapply external_call_trace_length; eauto. + red; intros; inv H; simpl; try omega; eapply external_call_trace_length; eauto. Qed. (** * Alternate operational semantics (big-step) *) @@ -608,6 +619,12 @@ with exec_stmt: eval_funcall m fd vargs t m' vres -> e' = set_optvar optid vres e -> exec_stmt f sp e m (Scall optid sig a bl) t e' m' Out_normal + | exec_Sbuiltin: + forall f sp e m optid ef bl t m' vargs vres e', + eval_exprlist ge sp e m bl vargs -> + external_call ef ge vargs m t vres m' -> + e' = set_optvar optid vres e -> + exec_stmt f sp e m (Sbuiltin optid ef bl) t e' m' Out_normal | exec_Sifthenelse: forall f sp e m a s1 s2 v b t e' m' out, eval_expr ge sp e m a v -> @@ -884,6 +901,11 @@ Proof. constructor. reflexivity. traceEq. subst e'. constructor. +(* builtin *) + econstructor; split. + apply star_one. econstructor; eauto. + subst e'. constructor. + (* ifthenelse *) destruct (H2 k) as [S [A B]]. exists S; split. diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 30884b18..110e735e 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -21,6 +21,7 @@ open Datatypes open BinPos open Integers open AST +open PrintAST open Cminor (* Precedences and associativity -- like those of C *) @@ -57,6 +58,7 @@ let name_of_unop = function | Ocast16unsigned -> "int16u" | Ocast16signed -> "int16s" | Onegint -> "-" + | Oboolval -> "(_Bool)" | Onotbool -> "!" | Onotint -> "~" | Onegf -> "-f" @@ -193,6 +195,15 @@ let rec print_stmt p s = print_expr e1 print_expr_list (true, el) print_sig sg + | Sbuiltin(None, ef, el) -> + fprintf p "@[<hv 2>builtin %s@,(@[<hov 0>%a@])@;@]" + (name_of_external ef) + print_expr_list (true, el) + | Sbuiltin(Some id, ef, el) -> + fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]);@]@]" + (ident_name id) + (name_of_external ef) + print_expr_list (true, el) | Sseq(Sskip, s2) -> print_stmt p s2 | Sseq(s1, Sskip) -> diff --git a/backend/RTL.v b/backend/RTL.v index 6a209412..9b27a172 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -360,7 +360,7 @@ Proof. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate s0 vres2 m2). econstructor; eauto. (* trace length *) - inv H; simpl; try omega. + red; intros; inv H; simpl; try omega. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. Qed. diff --git a/backend/Selection.v b/backend/Selection.v index 9c037b82..2d6c9017 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -112,6 +112,7 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr := | Cminor.Ocast16unsigned => cast16unsigned arg | Cminor.Ocast16signed => cast16signed arg | Cminor.Onegint => negint arg + | Cminor.Oboolval => boolval arg | Cminor.Onotbool => notbool arg | Cminor.Onotint => notint arg | Cminor.Onegf => negf arg @@ -202,6 +203,8 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt := | None => Scall optid sg (sel_expr fn) (sel_exprlist args) | Some ef => Sbuiltin optid ef (sel_exprlist args) end + | Cminor.Sbuiltin optid ef args => + Sbuiltin optid ef (sel_exprlist args) | Cminor.Stailcall sg fn args => Stailcall sg (sel_expr fn) (sel_exprlist args) | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2) diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 54d59b1c..9681c66b 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -212,6 +212,7 @@ Proof. apply eval_cast8signed; auto. apply eval_cast16unsigned; auto. apply eval_cast16signed; auto. + apply eval_boolval; auto. apply eval_negint; auto. apply eval_notbool; auto. apply eval_notint; auto. @@ -619,6 +620,15 @@ Proof. eapply functions_translated; eauto. apply sig_function_translated. constructor; auto. apply call_cont_commut; auto. + (* Sbuiltin *) + exploit sel_exprlist_correct; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. + intros [vres' [m2 [A [B [C D]]]]]. + left; econstructor; split. + econstructor. eauto. eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + constructor; auto. + destruct optid; simpl; auto. apply set_var_lessdef; auto. (* Seq *) left; econstructor; split. constructor. constructor; auto. constructor; auto. (* Sifthenelse *) |