diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-09 10:17:43 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-09 10:17:43 +0100 |
| commit | 5aecefe808aaaad6ab05037e7d5e7f53b53e0b94 (patch) | |
| tree | 68ca0f66ccda018b2cd61262b3711ed030654a79 /backend/ValueAnalysis.v | |
| parent | 06841a5bb7ca27bc436e87e7991d0d05dbf5267c (diff) | |
| download | compcert-kvx-5aecefe808aaaad6ab05037e7d5e7f53b53e0b94.tar.gz compcert-kvx-5aecefe808aaaad6ab05037e7d5e7f53b53e0b94.zip | |
More prudent analysis of uninitialized const global variables.
In the presence of separate compilation and linking, an uninitialized
const global variable may be initialized elsewhere with a pointer value,
falsifying the points-to analysis. Report and fix by Chung-Kil Hur
and Jeehoon Kang.
Diffstat (limited to 'backend/ValueAnalysis.v')
| -rw-r--r-- | backend/ValueAnalysis.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 813944d6..9c7ca1f7 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -186,6 +186,7 @@ Definition alloc_global (rm: romem) (idg: ident * globdef fundef unit): romem := PTree.remove id rm | (id, Gvar v) => if v.(gvar_readonly) && negb v.(gvar_volatile) + && match v.(gvar_init) with nil => false | _ => true end then PTree.set id (store_init_data_list (ablock_init Pbot) 0 v.(gvar_init)) rm else PTree.remove id rm end. @@ -1677,13 +1678,15 @@ Proof. destruct (peq id id1). congruence. eapply H; eauto. - rewrite PTree.gsspec in H0. destruct (peq id id1). + inv H0. rewrite PTree.gss. - destruct (gvar_readonly v1 && negb (gvar_volatile v1)) eqn:RO. - InvBooleans. rewrite negb_true_iff in H2. + destruct (gvar_readonly v1 && negb (gvar_volatile v1) && + match gvar_init v1 with nil => false | _ => true end) eqn:RO. + InvBooleans. rewrite negb_true_iff in H4. rewrite PTree.gss in H1. exists v1. intuition congruence. rewrite PTree.grs in H1. discriminate. + rewrite PTree.gso. eapply H; eauto. - destruct (gvar_readonly v1 && negb (gvar_volatile v1)). + destruct (gvar_readonly v1 && negb (gvar_volatile v1) && + match gvar_init v1 with nil => false | _ => true end). rewrite PTree.gso in H1; auto. rewrite PTree.gro in H1; auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto. |