diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Constprop.v | 6 | ||||
-rw-r--r-- | backend/Constpropproof.v | 6 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 5 | ||||
-rw-r--r-- | backend/RTL.v | 3 | ||||
-rw-r--r-- | backend/RTLgen.v | 13 | ||||
-rw-r--r-- | backend/RTLgenproof.v | 1 | ||||
-rw-r--r-- | backend/RTLgenspec.v | 18 |
7 files changed, 34 insertions, 18 deletions
diff --git a/backend/Constprop.v b/backend/Constprop.v index cd844d30..8f4cb76d 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -144,9 +144,9 @@ Fixpoint debug_strength_reduction (ae: AE.t) (al: list (builtin_arg reg)) := | a :: al => let a' := builtin_arg_reduction ae a in let al' := a :: debug_strength_reduction ae al in - match a' with - | BA_int _ | BA_long _ | BA_float _ | BA_single _ => a' :: al' - | _ => al' + match a, a' with + | BA _, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => a' :: al' + | _, _ => al' end end. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index d9005f5e..eafefed5 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -243,7 +243,11 @@ Proof. induction 2; simpl. - exists (@nil val); constructor. - destruct IHlist_forall2 as (vl' & A). - destruct (builtin_arg_reduction ae a1); repeat (eauto; econstructor). + assert (eval_builtin_args ge (fun r => rs#r) sp m + (a1 :: debug_strength_reduction ae al) (b1 :: vl')) + by (constructor; eauto). + destruct a1; try (econstructor; eassumption). + destruct (builtin_arg_reduction ae (BA x)); repeat (eauto; econstructor). Qed. Lemma builtin_strength_reduction_correct: diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 2daa2d56..ed0fe524 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -266,6 +266,8 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args = args in match kind with | 1 -> (* line number *) + fprintf oc "%s debug: current scopes%a\n" + comment print_debug_args args; if Str.string_match re_file_line txt 0 then print_line oc (Str.matched_group 1 txt) (int_of_string (Str.matched_group 2 txt)) @@ -280,6 +282,9 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args = | 5 -> (* local variable preallocated in stack *) fprintf oc "%s debug: %s resides at%a\n" comment txt print_debug_args args + | 6 -> (* declaration of a local variable *) + fprintf oc "%s debug: %s declared in scope%a\n" + comment txt print_debug_args args | _ -> () diff --git a/backend/RTL.v b/backend/RTL.v index 56a5efeb..3cd4335d 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -104,8 +104,7 @@ Record function: Type := mkfunction { for its stack-allocated activation record. [fn_params] is the list of registers that are bound to the values of arguments at call time. [fn_entrypoint] is the node of the first instruction of the function - in the CFG. [fn_code_wf] asserts that all instructions of the function - have nodes no greater than [fn_nextpc]. *) + in the CFG. *) Definition fundef := AST.fundef function. diff --git a/backend/RTLgen.v b/backend/RTLgen.v index d818de58..3da961c6 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -415,11 +415,12 @@ Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list a1' :: convert_builtin_args al rl1 end. -Definition convert_builtin_res (map: mapping) (r: builtin_res ident) : mon (builtin_res reg) := - match r with - | BR id => do r <- find_var map id; ret (BR r) - | BR_none => ret BR_none - | _ => error (Errors.msg "RTLgen: bad builtin_res") +Definition convert_builtin_res (map: mapping) (oty: option typ) (r: builtin_res ident) : mon (builtin_res reg) := + match r, oty with + | BR id, _ => do r <- find_var map id; ret (BR r) + | BR_none, None => ret BR_none + | BR_none, Some _ => do r <- new_reg; ret (BR r) + | _, _ => error (Errors.msg "RTLgen: bad builtin_res") end. (** Translation of an expression. [transl_expr map a rd nd] @@ -598,7 +599,7 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) let al := exprlist_of_expr_list (params_of_builtin_args args) in do rargs <- alloc_regs map al; let args' := convert_builtin_args args rargs in - do res' <- convert_builtin_res map res; + do res' <- convert_builtin_res map (sig_res (ef_sig ef)) res; do n1 <- add_instr (Ibuiltin ef args' res' nd); transl_exprlist map al rargs n1 | Sseq s1 s2 => diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 559ab3a2..19f6f1f4 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -234,6 +234,7 @@ Proof. intros. inv H1; simpl. - eapply match_env_update_var; eauto. - auto. +- eapply match_env_update_temp; eauto. Qed. (** Matching and [let]-bound variables. *) diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 41b5016f..1e665002 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -814,7 +814,10 @@ Inductive tr_builtin_res: mapping -> builtin_res ident -> builtin_res reg -> Pro map.(map_vars)!id = Some r -> tr_builtin_res map (BR id) (BR r) | tr_builtin_res_none: forall map, - tr_builtin_res map BR_none BR_none. + tr_builtin_res map BR_none BR_none + | tr_builtin_res_fresh: forall map r, + ~reg_in_map map r -> + tr_builtin_res map BR_none (BR r). (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c], starting at node [ns], contains instructions that perform the Cminor @@ -1214,14 +1217,17 @@ Proof. Qed. Lemma convert_builtin_res_charact: - forall map res s res' s' INCR - (TR: convert_builtin_res map res s = OK res' s' INCR) + forall map oty res s res' s' INCR + (TR: convert_builtin_res map oty res s = OK res' s' INCR) (WF: map_valid map s), tr_builtin_res map res res'. Proof. - destruct res; simpl; intros; monadInv TR. -- constructor. unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto. -- constructor. + destruct res; simpl; intros. +- monadInv TR. constructor. unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto. +- destruct oty; monadInv TR. ++ constructor. eauto with rtlg. ++ constructor. +- monadInv TR. Qed. Lemma transl_stmt_charact: |