diff options
author | Xavier Leroy <xavier.leroy@gmail.com> | 2015-09-20 15:23:38 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@gmail.com> | 2015-09-20 15:23:38 +0200 |
commit | 9147350fdb47f3471ce6d9202b7c996f79ffab2d (patch) | |
tree | f47977b33fa0975d614cc9bc2e4a22c996a96401 /backend/Constpropproof.v | |
parent | db0a62a01bbf90617701b68917319767159bf039 (diff) | |
download | compcert-9147350fdb47f3471ce6d9202b7c996f79ffab2d.tar.gz compcert-9147350fdb47f3471ce6d9202b7c996f79ffab2d.zip |
Experiment: track the scopes of local variables via __builtin_debug.
C2C: the code that insert debug builtins with the line numbers is now
in Unblock. Handle calls to __builtin_debug.
Unblock: generate __builtin_debug(1) for line numbers, carrying
the list of active scopes as extra arguments.
Generate __builtin_debug(6) for local variable declarations,
carrying the corresponding scope number as extra argument.
Constprop: avoid duplicating debug arguments that are constants already.
PrintAsmaux: show this extra debug info as comments.
Diffstat (limited to 'backend/Constpropproof.v')
-rw-r--r-- | backend/Constpropproof.v | 6 |
1 files changed, 5 insertions, 1 deletions
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: |