diff options
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Compiler.v | 97 | ||||
-rw-r--r-- | driver/Interp.ml | 55 |
2 files changed, 32 insertions, 120 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index 6fbfacdd..e6e8cc2b 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -184,91 +184,6 @@ Proof. intros; unfold print. destruct (printer prog); auto. Qed. -Lemma map_partial_compose: - forall (X A B C: Type) - (ctx: X -> errmsg) - (f1: A -> res B) (f2: B -> res C) - (pa: list (X * A)) (pc: list (X * C)), - map_partial ctx (fun f => f1 f @@@ f2) pa = OK pc -> - { pb | map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc }. -Proof. - induction pa; simpl. - intros. inv H. econstructor; eauto. - intro pc. destruct a as [x a]. - destruct (f1 a) as [] _eqn; simpl; try congruence. - destruct (f2 b) as [] _eqn; simpl; try congruence. - destruct (map_partial ctx (fun f => f1 f @@@ f2) pa) as [] _eqn; simpl; try congruence. - intros. inv H. - destruct (IHpa l) as [pb [P Q]]; auto. - rewrite P; simpl. - econstructor; split. eauto. simpl. rewrite Heqr0. rewrite Q. auto. -Qed. - -Lemma transform_partial_program_compose: - forall (A B C V: Type) - (f1: A -> res B) (f2: B -> res C) - (pa: program A V) (pc: program C V), - transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc -> - { pb | transform_partial_program f1 pa = OK pb /\ - transform_partial_program f2 pb = OK pc }. -Proof. - intros. unfold transform_partial_program in H. - destruct (map_partial prefix_name (fun f : A => f1 f @@@ f2) (prog_funct pa)) as [] _eqn; - simpl in H; inv H. - destruct (map_partial_compose _ _ _ _ _ _ _ _ _ Heqr) as [xb [P Q]]. - exists (mkprogram xb (prog_main pa) (prog_vars pa)); split. - unfold transform_partial_program. rewrite P; auto. - unfold transform_partial_program. simpl. rewrite Q; auto. -Qed. - -Lemma transform_program_partial_program: - forall (A B V: Type) (f: A -> B) (p: program A V) (tp: program B V), - transform_partial_program (fun x => OK (f x)) p = OK tp -> - transform_program f p = tp. -Proof. - intros until tp. unfold transform_partial_program. - rewrite map_partial_total. simpl. intros. inv H. auto. -Qed. - -Lemma transform_program_compose: - forall (A B C V: Type) - (f1: A -> res B) (f2: B -> C) - (pa: program A V) (pc: program C V), - transform_partial_program (fun f => f1 f @@ f2) pa = OK pc -> - { pb | transform_partial_program f1 pa = OK pb /\ - transform_program f2 pb = pc }. -Proof. - intros. - replace (fun f : A => f1 f @@ f2) - with (fun f : A => f1 f @@@ (fun x => OK (f2 x))) in H. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [pb [X Y]]. - exists pb; split. auto. - apply transform_program_partial_program. auto. - apply extensionality; intro. destruct(f1 x); auto. -Qed. - -Lemma transform_partial_program_identity: - forall (A V: Type) (pa pb: program A V), - transform_partial_program (@OK A) pa = OK pb -> - pa = pb. -Proof. - intros until pb. unfold transform_partial_program. - replace (@OK A) with (fun b => @OK A b). - rewrite map_partial_identity. simpl. destruct pa; simpl; congruence. - apply extensionality; auto. -Qed. - -Lemma transform_program_print_identity: - forall (A V: Type) (p: program A V) (f: A -> unit), - transform_program (print f) p = p. -Proof. - intros until f. unfold transform_program, transf_program. - destruct p; simpl; f_equal. - transitivity (map (fun x => x) prog_funct). - apply list_map_exten; intros. destruct x; simpl. rewrite print_identity. auto. - apply list_map_identity. -Qed. - Lemma compose_print_identity: forall (A: Type) (x: res A) (f: A -> unit), x @@ print f = x. @@ -290,18 +205,6 @@ Qed. These results establish the correctness of the whole compiler! *) -Ltac TransfProgInv := - match goal with - | [ H: transform_partial_program (fun f => _ @@@ _) _ = OK _ |- _ ] => - let p := fresh "p" in let X := fresh "X" in let P := fresh "P" in - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p [X P]]; - clear H - | [ H: transform_partial_program (fun f => _ @@ _) _ = OK _ |- _ ] => - let p := fresh "p" in let X := fresh "X" in let P := fresh "P" in - destruct (transform_program_compose _ _ _ _ _ _ _ _ H) as [p [X P]]; - clear H - end. - Theorem transf_rtl_program_correct: forall p tp, transf_rtl_program p = OK tp -> diff --git a/driver/Interp.ml b/driver/Interp.ml index fc0526a5..9031042f 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -87,9 +87,11 @@ let print_event p = function let name_of_fundef prog fd = let rec find_name = function | [] -> "<unknown function>" - | (id, fd') :: rem -> + | (id, Gfun fd') :: rem -> if fd = fd' then extern_atom id else find_name rem - in find_name prog.prog_funct + | (id, Gvar v) :: rem -> + find_name rem + in find_name prog.prog_defs let name_of_function prog fn = name_of_fundef prog (Internal fn) @@ -468,11 +470,13 @@ let rec explore p prog ge time ss = (* Massaging the source program *) let unvolatile prog = - let unvolatile_globvar (id, gv) = - (id, if gv.gvar_volatile - then {gv with gvar_readonly = false; gvar_volatile = false} - else gv) in - {prog with prog_vars = List.map unvolatile_globvar prog.prog_vars} + let unvolatile_globdef = function + | (id, Gvar gv) -> + (id, Gvar(if gv.gvar_volatile + then {gv with gvar_readonly = false; gvar_volatile = false} + else gv)) + | idfd -> idfd in + {prog with prog_defs = List.map unvolatile_globdef prog.prog_defs} let change_main_function p old_main old_main_ty = let old_main = Evalof(Evar(old_main, old_main_ty), old_main_ty) in @@ -483,24 +487,29 @@ let change_main_function p old_main old_main_ty = let new_main_fn = { fn_return = type_int32s; fn_params = []; fn_vars = []; fn_body = body } in let new_main_id = intern_string "___main" in - { p with - prog_main = new_main_id; - prog_funct = (new_main_id, Internal new_main_fn) :: p.prog_funct } + { prog_main = new_main_id; + prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs } + +let rec find_main_function name = function + | [] -> None + | (id, Gfun fd) :: gdl -> if id = name then Some fd else find_main_function name gdl + | (id, Gvar v) :: gdl -> find_main_function name gdl let fixup_main p = - try - match type_of_fundef (List.assoc p.prog_main p.prog_funct) with - | Tfunction(Tnil, Tint(I32, Signed, _)) -> - Some p - | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)), - Tint _) as ty -> - Some (change_main_function p p.prog_main ty) - | _ -> - fprintf err_formatter "ERROR: wrong type for main() function"; - None - with Not_found -> - fprintf err_formatter "ERROR: no main() function"; - None + match find_main_function p.prog_main p.prog_defs with + | None -> + fprintf err_formatter "ERROR: no main() function"; + None + | Some main_fd -> + match type_of_fundef main_fd with + | Tfunction(Tnil, Tint(I32, Signed, _)) -> + Some p + | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)), + Tint _) as ty -> + Some (change_main_function p p.prog_main ty) + | _ -> + fprintf err_formatter "ERROR: wrong type for main() function"; + None (* Execution of a whole program *) |