1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory AbsInt0_const |
|
4 imports AbsInt0 |
|
5 begin |
|
6 |
|
7 subsection "Constant Propagation" |
|
8 |
|
9 datatype cval = Const val | Any |
|
10 |
|
11 fun rep_cval where |
|
12 "rep_cval (Const n) = {n}" | |
|
13 "rep_cval (Any) = UNIV" |
|
14 |
|
15 fun plus_cval where |
|
16 "plus_cval (Const m) (Const n) = Const(m+n)" | |
|
17 "plus_cval _ _ = Any" |
|
18 |
|
19 instantiation cval :: SL_top |
|
20 begin |
|
21 |
|
22 fun le_cval where |
|
23 "_ \<sqsubseteq> Any = True" | |
|
24 "Const n \<sqsubseteq> Const m = (n=m)" | |
|
25 "Any \<sqsubseteq> Const _ = False" |
|
26 |
|
27 fun join_cval where |
|
28 "Const m \<squnion> Const n = (if n=m then Const m else Any)" | |
|
29 "_ \<squnion> _ = Any" |
|
30 |
|
31 definition "Top = Any" |
|
32 |
|
33 instance |
|
34 proof |
|
35 case goal1 thus ?case by (cases x) simp_all |
|
36 next |
|
37 case goal2 thus ?case by(cases z, cases y, cases x, simp_all) |
|
38 next |
|
39 case goal3 thus ?case by(cases x, cases y, simp_all) |
|
40 next |
|
41 case goal4 thus ?case by(cases y, cases x, simp_all) |
|
42 next |
|
43 case goal5 thus ?case by(cases z, cases y, cases x, simp_all) |
|
44 next |
|
45 case goal6 thus ?case by(simp add: Top_cval_def) |
|
46 qed |
|
47 |
|
48 end |
|
49 |
|
50 interpretation Rep rep_cval |
|
51 proof |
|
52 case goal1 thus ?case |
|
53 by(cases a, cases b, simp, simp, cases b, simp, simp) |
|
54 qed |
|
55 |
|
56 interpretation Val_abs rep_cval Const plus_cval |
|
57 proof |
|
58 case goal1 show ?case by simp |
|
59 next |
|
60 case goal2 thus ?case |
|
61 by(cases a1, cases a2, simp, simp, cases a2, simp, simp) |
|
62 qed |
|
63 |
|
64 interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)" |
|
65 defines AI_const is AI |
|
66 and aval'_const is aval' |
|
67 proof qed (auto simp: iter'_pfp_above) |
|
68 |
|
69 text{* Straight line code: *} |
|
70 definition "test1_const = |
|
71 ''y'' ::= N 7; |
|
72 ''z'' ::= Plus (V ''y'') (N 2); |
|
73 ''y'' ::= Plus (V ''x'') (N 0)" |
|
74 |
|
75 text{* Conditional: *} |
|
76 definition "test2_const = |
|
77 IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5" |
|
78 |
|
79 text{* Conditional, test is ignored: *} |
|
80 definition "test3_const = |
|
81 ''x'' ::= N 42; |
|
82 IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6" |
|
83 |
|
84 text{* While: *} |
|
85 definition "test4_const = |
|
86 ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0" |
|
87 |
|
88 text{* While, test is ignored: *} |
|
89 definition "test5_const = |
|
90 ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1" |
|
91 |
|
92 text{* Iteration is needed: *} |
|
93 definition "test6_const = |
|
94 ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2; |
|
95 WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')" |
|
96 |
|
97 text{* More iteration would be needed: *} |
|
98 definition "test7_const = |
|
99 ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3; |
|
100 WHILE Less (V ''x'') (N 1) |
|
101 DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')" |
|
102 |
|
103 value [code] "list (AI_const test1_const Top)" |
|
104 value [code] "list (AI_const test2_const Top)" |
|
105 value [code] "list (AI_const test3_const Top)" |
|
106 value [code] "list (AI_const test4_const Top)" |
|
107 value [code] "list (AI_const test5_const Top)" |
|
108 value [code] "list (AI_const test6_const Top)" |
|
109 value [code] "list (AI_const test7_const Top)" |
|
110 |
|
111 end |
|