generated_code.v 10.7 KB
Newer Older
1
2
3
4
5
6
7
From refinedc.lang Require Export notation.
From refinedc.lang Require Import tactics.
From refinedc.typing Require Import annotations.
Set Default Proof Using "Type".

(* Generated from [tutorial/t07_arrays.c]. *)
Section code.
8
  Definition file_0 : string := "include/refinedc.h".
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
  Definition file_1 : string := "tutorial/t07_arrays.c".
  Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
  Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.
  Definition loc_4 : location_info := LocationInfo file_0 49 9 49 32.
  Definition loc_5 : location_info := LocationInfo file_0 49 33 49 37.
  Definition loc_6 : location_info := LocationInfo file_0 49 33 49 37.
  Definition loc_7 : location_info := LocationInfo file_0 49 39 49 45.
  Definition loc_8 : location_info := LocationInfo file_0 49 39 49 45.
  Definition loc_11 : location_info := LocationInfo file_1 14 2 14 16.
  Definition loc_12 : location_info := LocationInfo file_1 15 2 15 16.
  Definition loc_13 : location_info := LocationInfo file_1 16 2 16 12.
  Definition loc_14 : location_info := LocationInfo file_1 16 2 16 7.
  Definition loc_15 : location_info := LocationInfo file_1 16 2 16 7.
  Definition loc_16 : location_info := LocationInfo file_1 16 2 16 4.
  Definition loc_17 : location_info := LocationInfo file_1 16 2 16 4.
  Definition loc_18 : location_info := LocationInfo file_1 16 5 16 6.
  Definition loc_19 : location_info := LocationInfo file_1 16 5 16 6.
  Definition loc_20 : location_info := LocationInfo file_1 16 10 16 11.
  Definition loc_21 : location_info := LocationInfo file_1 16 10 16 11.
  Definition loc_22 : location_info := LocationInfo file_1 15 2 15 7.
  Definition loc_23 : location_info := LocationInfo file_1 15 2 15 7.
  Definition loc_24 : location_info := LocationInfo file_1 15 2 15 4.
  Definition loc_25 : location_info := LocationInfo file_1 15 2 15 4.
  Definition loc_26 : location_info := LocationInfo file_1 15 5 15 6.
  Definition loc_27 : location_info := LocationInfo file_1 15 5 15 6.
  Definition loc_28 : location_info := LocationInfo file_1 15 10 15 15.
  Definition loc_29 : location_info := LocationInfo file_1 15 10 15 15.
  Definition loc_30 : location_info := LocationInfo file_1 15 10 15 15.
  Definition loc_31 : location_info := LocationInfo file_1 15 10 15 12.
  Definition loc_32 : location_info := LocationInfo file_1 15 10 15 12.
  Definition loc_33 : location_info := LocationInfo file_1 15 13 15 14.
  Definition loc_34 : location_info := LocationInfo file_1 15 13 15 14.
  Definition loc_35 : location_info := LocationInfo file_1 14 10 14 15.
  Definition loc_36 : location_info := LocationInfo file_1 14 10 14 15.
  Definition loc_37 : location_info := LocationInfo file_1 14 10 14 15.
  Definition loc_38 : location_info := LocationInfo file_1 14 10 14 12.
  Definition loc_39 : location_info := LocationInfo file_1 14 10 14 12.
  Definition loc_40 : location_info := LocationInfo file_1 14 13 14 14.
  Definition loc_41 : location_info := LocationInfo file_1 14 13 14 14.
  Definition loc_46 : location_info := LocationInfo file_1 33 2 33 23.
  Definition loc_47 : location_info := LocationInfo file_1 35 2 35 14.
  Definition loc_48 : location_info := LocationInfo file_1 44 2 46 3.
  Definition loc_49 : location_info := LocationInfo file_1 44 2 46 3.
  Definition loc_50 : location_info := LocationInfo file_1 44 2 46 3.
  Definition loc_51 : location_info := LocationInfo file_1 48 2 48 13.
  Definition loc_52 : location_info := LocationInfo file_1 48 9 48 12.
  Definition loc_53 : location_info := LocationInfo file_1 48 9 48 12.
  Definition loc_54 : location_info := LocationInfo file_1 44 28 46 3.
  Definition loc_55 : location_info := LocationInfo file_1 45 4 45 32.
  Definition loc_56 : location_info := LocationInfo file_1 44 2 46 3.
  Definition loc_58 : location_info := LocationInfo file_1 44 24 44 25.
  Definition loc_59 : location_info := LocationInfo file_1 45 24 45 32.
  Definition loc_60 : location_info := LocationInfo file_1 45 24 45 27.
  Definition loc_61 : location_info := LocationInfo file_1 45 30 45 31.
  Definition loc_62 : location_info := LocationInfo file_1 45 30 45 31.
  Definition loc_64 : location_info := LocationInfo file_1 45 7 45 22.
  Definition loc_65 : location_info := LocationInfo file_1 45 7 45 12.
  Definition loc_66 : location_info := LocationInfo file_1 45 7 45 12.
  Definition loc_67 : location_info := LocationInfo file_1 45 7 45 12.
  Definition loc_68 : location_info := LocationInfo file_1 45 7 45 9.
  Definition loc_69 : location_info := LocationInfo file_1 45 7 45 9.
  Definition loc_70 : location_info := LocationInfo file_1 45 10 45 11.
  Definition loc_71 : location_info := LocationInfo file_1 45 10 45 11.
  Definition loc_72 : location_info := LocationInfo file_1 45 15 45 22.
  Definition loc_73 : location_info := LocationInfo file_1 45 15 45 22.
  Definition loc_74 : location_info := LocationInfo file_1 45 15 45 22.
  Definition loc_75 : location_info := LocationInfo file_1 45 15 45 17.
  Definition loc_76 : location_info := LocationInfo file_1 45 15 45 17.
  Definition loc_77 : location_info := LocationInfo file_1 45 18 45 21.
  Definition loc_78 : location_info := LocationInfo file_1 45 18 45 21.
  Definition loc_79 : location_info := LocationInfo file_1 44 17 44 22.
  Definition loc_80 : location_info := LocationInfo file_1 44 17 44 18.
  Definition loc_81 : location_info := LocationInfo file_1 44 17 44 18.
  Definition loc_82 : location_info := LocationInfo file_1 44 21 44 22.
  Definition loc_83 : location_info := LocationInfo file_1 44 21 44 22.
  Definition loc_84 : location_info := LocationInfo file_1 44 14 44 15.
  Definition loc_87 : location_info := LocationInfo file_1 35 12 35 13.
  Definition loc_90 : location_info := LocationInfo file_1 33 13 33 23.
  Definition loc_91 : location_info := LocationInfo file_1 33 20 33 22.
  Definition loc_92 : location_info := LocationInfo file_1 33 21 33 22.
  Definition loc_94 : location_info := LocationInfo file_1 33 5 33 11.
  Definition loc_95 : location_info := LocationInfo file_1 33 5 33 6.
  Definition loc_96 : location_info := LocationInfo file_1 33 5 33 6.
  Definition loc_97 : location_info := LocationInfo file_1 33 10 33 11.

  (* Definition of function [copy_alloc_id]. *)
  Definition impl_copy_alloc_id : function := {|
    f_args := [
      ("to", it_layout uintptr_t);
      ("from", void*)
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
        locinfo: loc_2 ;
Michael Sammler's avatar
Michael Sammler committed
106
        Return (LocInfoE loc_3 (CopyAllocId (IntOp uintptr_t) (LocInfoE loc_5 (use{IntOp uintptr_t} (LocInfoE loc_6 ("to")))) (LocInfoE loc_7 (use{PtrOp} (LocInfoE loc_8 ("from"))))))
107
108
109
      ]> $
    )%E
  |}.
110
111
112
113

  (* Definition of function [permute]. *)
  Definition impl_permute : function := {|
    f_args := [
114
      ("ar", void*);
115
116
117
118
119
120
121
122
123
      ("i", it_layout i32);
      ("j", it_layout i32)
    ];
    f_local_vars := [
      ("k", it_layout i32)
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
Michael Sammler's avatar
Michael Sammler committed
124
125
        "k" <-{ IntOp i32 }
          LocInfoE loc_35 (use{IntOp i32} (LocInfoE loc_37 ((LocInfoE loc_38 (!{PtrOp} (LocInfoE loc_39 ("ar")))) at_offset{it_layout i32, PtrOp, IntOp i32} (LocInfoE loc_40 (use{IntOp i32} (LocInfoE loc_41 ("i"))))))) ;
126
        locinfo: loc_12 ;
Michael Sammler's avatar
Michael Sammler committed
127
128
        LocInfoE loc_23 ((LocInfoE loc_24 (!{PtrOp} (LocInfoE loc_25 ("ar")))) at_offset{it_layout i32, PtrOp, IntOp i32} (LocInfoE loc_26 (use{IntOp i32} (LocInfoE loc_27 ("i"))))) <-{ IntOp i32 }
          LocInfoE loc_28 (use{IntOp i32} (LocInfoE loc_30 ((LocInfoE loc_31 (!{PtrOp} (LocInfoE loc_32 ("ar")))) at_offset{it_layout i32, PtrOp, IntOp i32} (LocInfoE loc_33 (use{IntOp i32} (LocInfoE loc_34 ("j"))))))) ;
129
        locinfo: loc_13 ;
Michael Sammler's avatar
Michael Sammler committed
130
131
        LocInfoE loc_15 ((LocInfoE loc_16 (!{PtrOp} (LocInfoE loc_17 ("ar")))) at_offset{it_layout i32, PtrOp, IntOp i32} (LocInfoE loc_18 (use{IntOp i32} (LocInfoE loc_19 ("j"))))) <-{ IntOp i32 }
          LocInfoE loc_20 (use{IntOp i32} (LocInfoE loc_21 ("k"))) ;
132
133
134
135
136
137
138
139
        Return (VOID)
      ]> $
    )%E
  |}.

  (* Definition of function [min_array]. *)
  Definition impl_min_array : function := {|
    f_args := [
140
      ("ar", void*);
141
142
143
144
145
146
147
148
149
      ("n", it_layout i32)
    ];
    f_local_vars := [
      ("i", it_layout i32);
      ("res", it_layout i32)
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
150
        locinfo: loc_94 ;
Michael Sammler's avatar
Michael Sammler committed
151
        if: LocInfoE loc_94 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_94 ((LocInfoE loc_95 (use{IntOp i32} (LocInfoE loc_96 ("n")))) ={IntOp i32, IntOp i32} (LocInfoE loc_97 (i2v 0 i32)))))
152
        then
153
        locinfo: loc_90 ;
154
155
156
157
158
          Goto "#8"
        else
        Goto "#9"
      ]> $
      <[ "#1" :=
Michael Sammler's avatar
Michael Sammler committed
159
160
        "res" <-{ IntOp i32 } LocInfoE loc_87 (i2v 0 i32) ;
        "i" <-{ IntOp i32 } LocInfoE loc_84 (i2v 1 i32) ;
161
        locinfo: loc_50 ;
162
163
164
        Goto "#2"
      ]> $
      <[ "#2" :=
165
        locinfo: loc_79 ;
Michael Sammler's avatar
Michael Sammler committed
166
        if: LocInfoE loc_79 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_79 ((LocInfoE loc_80 (use{IntOp i32} (LocInfoE loc_81 ("i")))) <{IntOp i32, IntOp i32} (LocInfoE loc_82 (use{IntOp i32} (LocInfoE loc_83 ("n")))))))
167
        then
168
        locinfo: loc_64 ;
169
170
          Goto "#3"
        else
171
        locinfo: loc_51 ;
172
173
174
          Goto "#4"
      ]> $
      <[ "#3" :=
175
        locinfo: loc_64 ;
Michael Sammler's avatar
Michael Sammler committed
176
        if: LocInfoE loc_64 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_64 ((LocInfoE loc_65 (use{IntOp i32} (LocInfoE loc_67 ((LocInfoE loc_68 (!{PtrOp} (LocInfoE loc_69 ("ar")))) at_offset{it_layout i32, PtrOp, IntOp i32} (LocInfoE loc_70 (use{IntOp i32} (LocInfoE loc_71 ("i")))))))) <{IntOp i32, IntOp i32} (LocInfoE loc_72 (use{IntOp i32} (LocInfoE loc_74 ((LocInfoE loc_75 (!{PtrOp} (LocInfoE loc_76 ("ar")))) at_offset{it_layout i32, PtrOp, IntOp i32} (LocInfoE loc_77 (use{IntOp i32} (LocInfoE loc_78 ("res")))))))))))
177
        then
178
        locinfo: loc_59 ;
179
180
          Goto "#6"
        else
181
        locinfo: loc_56 ;
182
183
184
          Goto "#7"
      ]> $
      <[ "#4" :=
185
        locinfo: loc_51 ;
Michael Sammler's avatar
Michael Sammler committed
186
        Return (LocInfoE loc_52 (use{IntOp i32} (LocInfoE loc_53 ("res"))))
187
188
      ]> $
      <[ "#5" :=
189
190
        locinfo: loc_56 ;
        Goto "continue6"
191
192
      ]> $
      <[ "#6" :=
193
        locinfo: loc_59 ;
Michael Sammler's avatar
Michael Sammler committed
194
195
        LocInfoE loc_60 ("res") <-{ IntOp i32 }
          LocInfoE loc_61 (use{IntOp i32} (LocInfoE loc_62 ("i"))) ;
196
        locinfo: loc_56 ;
197
198
199
        Goto "#5"
      ]> $
      <[ "#7" :=
200
        locinfo: loc_56 ;
201
202
203
        Goto "#5"
      ]> $
      <[ "#8" :=
204
205
        locinfo: loc_90 ;
        Return (LocInfoE loc_91 (UnOp NegOp (IntOp i32) (LocInfoE loc_92 (i2v 1 i32))))
206
207
208
209
      ]> $
      <[ "#9" :=
        Goto "#1"
      ]> $
210
      <[ "continue6" :=
Michael Sammler's avatar
Michael Sammler committed
211
212
        LocInfoE loc_58 ("i") <-{ IntOp i32 }
          (use{IntOp i32} (LocInfoE loc_58 ("i"))) +{IntOp i32, IntOp i32} (i2v 1 i32) ;
213
        locinfo: loc_50 ;
214
215
216
217
218
        Goto "#2"
      ]> $
    )%E
  |}.
End code.