source: src/Clight/toCminorCorrectness.ma @ 2458

Last change on this file since 2458 was 2458, checked in by campbell, 7 years ago

Clight to Cminor allocates stack variables to disjoint regions within the
frame.

File size: 4.5 KB
Line 
1include "Clight/toCminor.ma".
2
3(* When we characterise the local Clight variables, those that are stack
4   allocated are given disjoint regions of the stack. *)
5
6lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
7  characterise_vars globals f = 〈vartypes, stacksize〉 →
8  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
9  ∀id',n',ty'. id ≠ id' →
10  lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
11  n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
12#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
13whd in ⊢ (??%? → ?);
14generalize in match vartypes; -vartypes
15generalize in match stacksize; -stacksize
16elim (args@vars)
17[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
18  elim globals in L;
19  [ normalize #L destruct
20  | * * #id' #r #ty' #tl #IH
21    whd in match (foldr ?????);
22    #L cases (lookup_add_cases ??????? L)
23    [ * #E1 #E2 destruct
24    | @IH
25    ]
26  ]
27| * #id1 #ty1 #tl #IH #stacksize #vartypes
28  whd in match (foldr ?????);
29  (* Avoid writing out the definition again *)
30  letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
31  lapply (refl ? ih) whd in match ih; -ih
32  cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
33  #vartypes' #stack' #FOLD #IH
34  whd in ⊢ (??(match % with [_⇒?])? → ?);
35  cases (orb ??)
36  #CHAR whd in CHAR:(??%?); destruct
37  #L cases (lookup_add_cases ??????? L)
38  [ 1,3: * #E1 #E2 destruct
39    #id' #n' #ty' #NE >lookup_add_miss /2/
40    #L' %1 -L -IH
41    generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
42    generalize in match stack'; -stack'
43    elim tl
44    [ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
45      elim globals in L';
46      [ normalize #E destruct
47      | * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
48        #L cases (lookup_add_cases ??????? L)
49        [ * #E1 #E2 destruct
50        | @IH
51        ]
52      ]
53    | * #id2 #ty2 #tl2 #IH #stack' #vartypes'
54      whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
55      #vartypes2 #stack2 #IH
56      whd in ⊢ (??%? → ?);
57      cases (orb ??)
58      [ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
59        [ * #E1 #E2 destruct //
60        | #L'' lapply (IH ?? (refl ??) L'') /2/
61        ]
62      | #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
63        [ * #E1 #E2 destruct
64        | #L'' lapply (IH ?? (refl ??) L'') /2/
65        ]
66      ]
67    ]
68  | -L #L #id' #n' #ty' #NE #L'
69    cases (lookup_add_cases ??????? L')
70    [ * #E1 #E2 destruct
71      %2 -IH -L'
72      generalize in match vartypes' in FOLD L; -vartypes'
73      generalize in match stack'; -stack'
74      elim tl
75      [ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
76        elim globals in L;
77        [ normalize #E destruct
78        | * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
79          #L cases (lookup_add_cases ??????? L)
80          [ * #E1 #E2 destruct
81          | @IH
82          ]
83        ]
84      | * #id1 #ty1 #tl1 #IH #stack' #vartypes'
85        whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
86        #vartypes2 #stack2 #IH
87        whd in ⊢ (??%? → ?);
88        cases (orb ??)
89        #E whd in E:(??%?); destruct
90        #L cases (lookup_add_cases ??????? L)
91        [ 1,3: * #E1 #E2 destruct //
92        | 2,4: #L' lapply (IH ?? (refl ??) L') /2/
93        ]
94      ]
95    | @(IH … (refl ??) L … NE)
96    ]
97  | -L #L #id' #n' #ty' #NE #L'
98    cases (lookup_add_cases ??????? L')
99    [ * #E1 #E2 destruct
100    | @(IH … (refl ??) L … NE)
101    ]
102  ]
103] qed.
104
105(* And everything is in the stack frame. *)
106
107lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
108  characterise_vars globals f = 〈vartypes, stacksize〉 →
109  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
110  n + sizeof ty ≤ stacksize.
111#globals * #ret #args #vars #body whd in match (characterise_vars ??);
112elim (args@vars)
113[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
114  whd in FOLD:(??%?); destruct elim globals in L;
115  [ #E normalize in E; destruct
116  | * * #id' #r' #ty' #tl' #IH
117    whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
118    [ * #E1 #E2 destruct
119    | @IH
120    ]
121  ]
122| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
123  whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
124  #vartypes' #stackspace' #IH
125  whd in ⊢ (??(match % with [_⇒?])? → ?);
126  cases (orb ??) whd in ⊢ (??%? → ?);
127  #E destruct #L cases (lookup_add_cases ??????? L)
128  [ 1,3: * #E1 #E2 destruct //
129  | 2,4: #L' lapply (IH … (refl ??) L') /2/
130  ]
131] qed.
Note: See TracBrowser for help on using the repository browser.