generated_code.v 10.5 KB
Newer Older
Michael Sammler's avatar
Michael Sammler committed
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 [examples/talk_demo3.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
  Definition file_1 : string := "examples/talk_demo3.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 21 2 25 3.
  Definition loc_12 : location_info := LocationInfo file_1 21 27 23 3.
  Definition loc_13 : location_info := LocationInfo file_1 22 4 22 11.
  Definition loc_14 : location_info := LocationInfo file_1 22 4 22 6.
  Definition loc_15 : location_info := LocationInfo file_1 22 5 22 6.
  Definition loc_16 : location_info := LocationInfo file_1 22 5 22 6.
  Definition loc_17 : location_info := LocationInfo file_1 22 9 22 10.
  Definition loc_18 : location_info := LocationInfo file_1 22 9 22 10.
  Definition loc_19 : location_info := LocationInfo file_1 23 9 25 3.
  Definition loc_20 : location_info := LocationInfo file_1 24 4 24 27.
  Definition loc_21 : location_info := LocationInfo file_1 24 4 24 10.
  Definition loc_22 : location_info := LocationInfo file_1 24 4 24 10.
  Definition loc_23 : location_info := LocationInfo file_1 24 11 24 22.
  Definition loc_24 : location_info := LocationInfo file_1 24 12 24 22.
  Definition loc_25 : location_info := LocationInfo file_1 24 12 24 16.
  Definition loc_26 : location_info := LocationInfo file_1 24 12 24 16.
  Definition loc_27 : location_info := LocationInfo file_1 24 14 24 15.
  Definition loc_28 : location_info := LocationInfo file_1 24 14 24 15.
  Definition loc_29 : location_info := LocationInfo file_1 24 24 24 25.
  Definition loc_30 : location_info := LocationInfo file_1 24 24 24 25.
  Definition loc_31 : location_info := LocationInfo file_1 21 5 21 25.
  Definition loc_32 : location_info := LocationInfo file_1 21 5 21 7.
  Definition loc_33 : location_info := LocationInfo file_1 21 5 21 7.
  Definition loc_34 : location_info := LocationInfo file_1 21 6 21 7.
  Definition loc_35 : location_info := LocationInfo file_1 21 6 21 7.
  Definition loc_36 : location_info := LocationInfo file_1 21 11 21 25.
  Definition loc_39 : location_info := LocationInfo file_1 30 2 30 61.
  Definition loc_40 : location_info := LocationInfo file_1 31 2 31 17.
  Definition loc_41 : location_info := LocationInfo file_1 31 18 31 47.
  Definition loc_42 : location_info := LocationInfo file_1 32 2 32 61.
  Definition loc_43 : location_info := LocationInfo file_1 33 2 33 17.
  Definition loc_44 : location_info := LocationInfo file_1 33 18 33 47.
  Definition loc_45 : location_info := LocationInfo file_1 34 2 34 24.
  Definition loc_46 : location_info := LocationInfo file_1 35 2 37 3.
  Definition loc_47 : location_info := LocationInfo file_1 35 30 37 3.
  Definition loc_48 : location_info := LocationInfo file_1 36 4 36 28.
  Definition loc_49 : location_info := LocationInfo file_1 36 11 36 26.
  Definition loc_50 : location_info := LocationInfo file_1 36 11 36 21.
  Definition loc_51 : location_info := LocationInfo file_1 36 11 36 21.
  Definition loc_52 : location_info := LocationInfo file_1 36 11 36 16.
  Definition loc_53 : location_info := LocationInfo file_1 36 11 36 16.
  Definition loc_54 : location_info := LocationInfo file_1 36 25 36 26.
  Definition loc_56 : location_info := LocationInfo file_1 35 5 35 28.
  Definition loc_57 : location_info := LocationInfo file_1 35 5 35 10.
  Definition loc_58 : location_info := LocationInfo file_1 35 5 35 10.
  Definition loc_59 : location_info := LocationInfo file_1 35 14 35 28.
  Definition loc_60 : location_info := LocationInfo file_1 34 2 34 8.
  Definition loc_61 : location_info := LocationInfo file_1 34 2 34 8.
  Definition loc_62 : location_info := LocationInfo file_1 34 9 34 15.
  Definition loc_63 : location_info := LocationInfo file_1 34 10 34 15.
  Definition loc_64 : location_info := LocationInfo file_1 34 17 34 22.
  Definition loc_65 : location_info := LocationInfo file_1 34 17 34 22.
  Definition loc_66 : location_info := LocationInfo file_1 33 18 33 29.
  Definition loc_67 : location_info := LocationInfo file_1 33 18 33 23.
  Definition loc_68 : location_info := LocationInfo file_1 33 18 33 23.
  Definition loc_69 : location_info := LocationInfo file_1 33 32 33 46.
  Definition loc_70 : location_info := LocationInfo file_1 33 2 33 12.
  Definition loc_71 : location_info := LocationInfo file_1 33 2 33 7.
  Definition loc_72 : location_info := LocationInfo file_1 33 2 33 7.
  Definition loc_73 : location_info := LocationInfo file_1 33 15 33 16.
  Definition loc_74 : location_info := LocationInfo file_1 32 29 32 60.
  Definition loc_75 : location_info := LocationInfo file_1 32 29 32 34.
  Definition loc_76 : location_info := LocationInfo file_1 32 29 32 34.
  Definition loc_77 : location_info := LocationInfo file_1 32 35 32 59.
  Definition loc_80 : location_info := LocationInfo file_1 31 18 31 29.
  Definition loc_81 : location_info := LocationInfo file_1 31 18 31 23.
  Definition loc_82 : location_info := LocationInfo file_1 31 18 31 23.
  Definition loc_83 : location_info := LocationInfo file_1 31 32 31 46.
  Definition loc_84 : location_info := LocationInfo file_1 31 2 31 12.
  Definition loc_85 : location_info := LocationInfo file_1 31 2 31 7.
  Definition loc_86 : location_info := LocationInfo file_1 31 2 31 7.
  Definition loc_87 : location_info := LocationInfo file_1 31 15 31 16.
  Definition loc_88 : location_info := LocationInfo file_1 30 29 30 60.
  Definition loc_89 : location_info := LocationInfo file_1 30 29 30 34.
  Definition loc_90 : location_info := LocationInfo file_1 30 29 30 34.
  Definition loc_91 : location_info := LocationInfo file_1 30 35 30 59.
Michael Sammler's avatar
Michael Sammler committed
93
94
95
96
97
98

  (* Definition of struct [list_node]. *)
  Program Definition struct_list_node := {|
    sl_members := [
      (Some "val", it_layout i32);
      (None, Layout 4%nat 0%nat);
99
      (Some "next", void*)
Michael Sammler's avatar
Michael Sammler committed
100
101
102
103
    ];
  |}.
  Solve Obligations with solve_struct_obligations.

104
105
106
107
108
109
110
111
112
113
114
115
  (* 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
116
        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"))))))
117
118
119
120
      ]> $
    )%E
  |}.

Michael Sammler's avatar
Michael Sammler committed
121
  (* Definition of function [append]. *)
122
  Definition impl_append (global_append : loc): function := {|
Michael Sammler's avatar
Michael Sammler committed
123
    f_args := [
124
125
      ("l", void*);
      ("k", void*)
Michael Sammler's avatar
Michael Sammler committed
126
127
128
129
130
131
    ];
    f_local_vars := [
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
132
        locinfo: loc_31 ;
Michael Sammler's avatar
Michael Sammler committed
133
        if: LocInfoE loc_31 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_31 ((LocInfoE loc_32 (use{PtrOp} (LocInfoE loc_34 (!{PtrOp} (LocInfoE loc_35 ("l")))))) ={PtrOp, PtrOp} (LocInfoE loc_36 (NULL)))))
Michael Sammler's avatar
Michael Sammler committed
134
        then
135
        locinfo: loc_13 ;
Michael Sammler's avatar
Michael Sammler committed
136
137
          Goto "#1"
        else
138
        locinfo: loc_20 ;
Michael Sammler's avatar
Michael Sammler committed
139
140
141
          Goto "#2"
      ]> $
      <[ "#1" :=
142
        locinfo: loc_13 ;
Michael Sammler's avatar
Michael Sammler committed
143
144
        LocInfoE loc_15 (!{PtrOp} (LocInfoE loc_16 ("l"))) <-{ PtrOp }
          LocInfoE loc_17 (use{PtrOp} (LocInfoE loc_18 ("k"))) ;
Michael Sammler's avatar
Michael Sammler committed
145
146
147
        Return (VOID)
      ]> $
      <[ "#2" :=
148
        locinfo: loc_20 ;
Michael Sammler's avatar
Michael Sammler committed
149
150
        expr: (LocInfoE loc_20 (Call (LocInfoE loc_22 (global_append)) [@{expr} LocInfoE loc_23 (&(LocInfoE loc_24 ((LocInfoE loc_25 (!{PtrOp} (LocInfoE loc_27 (!{PtrOp} (LocInfoE loc_28 ("l")))))) at{struct_list_node} "next"))) ;
        LocInfoE loc_29 (use{PtrOp} (LocInfoE loc_30 ("k"))) ])) ;
Michael Sammler's avatar
Michael Sammler committed
151
152
153
154
155
156
        Return (VOID)
      ]> $
    )%E
  |}.

  (* Definition of function [test]. *)
157
  Definition impl_test (global_alloc global_append : loc): function := {|
Michael Sammler's avatar
Michael Sammler committed
158
159
160
    f_args := [
    ];
    f_local_vars := [
161
162
      ("node1", void*);
      ("node2", void*)
Michael Sammler's avatar
Michael Sammler committed
163
164
165
166
    ];
    f_init := "#0";
    f_code := (
      <[ "#0" :=
Michael Sammler's avatar
Michael Sammler committed
167
        "node1" <-{ PtrOp }
168
169
          LocInfoE loc_88 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_88 (Call (LocInfoE loc_90 (global_alloc)) [@{expr} LocInfoE loc_91 (i2v (layout_of struct_list_node).(ly_size) size_t) ]))) ;
        locinfo: loc_40 ;
Michael Sammler's avatar
Michael Sammler committed
170
        LocInfoE loc_84 ((LocInfoE loc_85 (!{PtrOp} (LocInfoE loc_86 ("node1")))) at{struct_list_node} "val") <-{ IntOp i32 }
171
172
          LocInfoE loc_87 (i2v 1 i32) ;
        locinfo: loc_41 ;
Michael Sammler's avatar
Michael Sammler committed
173
        LocInfoE loc_80 ((LocInfoE loc_81 (!{PtrOp} (LocInfoE loc_82 ("node1")))) at{struct_list_node} "next") <-{ PtrOp }
174
          LocInfoE loc_83 (NULL) ;
Michael Sammler's avatar
Michael Sammler committed
175
        "node2" <-{ PtrOp }
176
177
          LocInfoE loc_74 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_74 (Call (LocInfoE loc_76 (global_alloc)) [@{expr} LocInfoE loc_77 (i2v (layout_of struct_list_node).(ly_size) size_t) ]))) ;
        locinfo: loc_43 ;
Michael Sammler's avatar
Michael Sammler committed
178
        LocInfoE loc_70 ((LocInfoE loc_71 (!{PtrOp} (LocInfoE loc_72 ("node2")))) at{struct_list_node} "val") <-{ IntOp i32 }
179
180
          LocInfoE loc_73 (i2v 2 i32) ;
        locinfo: loc_44 ;
Michael Sammler's avatar
Michael Sammler committed
181
        LocInfoE loc_66 ((LocInfoE loc_67 (!{PtrOp} (LocInfoE loc_68 ("node2")))) at{struct_list_node} "next") <-{ PtrOp }
182
183
184
          LocInfoE loc_69 (NULL) ;
        locinfo: loc_45 ;
        expr: (LocInfoE loc_45 (Call (LocInfoE loc_61 (global_append)) [@{expr} LocInfoE loc_62 (&(LocInfoE loc_63 ("node1"))) ;
Michael Sammler's avatar
Michael Sammler committed
185
        LocInfoE loc_64 (use{PtrOp} (LocInfoE loc_65 ("node2"))) ])) ;
186
        locinfo: loc_56 ;
Michael Sammler's avatar
Michael Sammler committed
187
        if: LocInfoE loc_56 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_56 ((LocInfoE loc_57 (use{PtrOp} (LocInfoE loc_58 ("node1")))) !={PtrOp, PtrOp} (LocInfoE loc_59 (NULL)))))
Michael Sammler's avatar
Michael Sammler committed
188
        then
189
        locinfo: loc_48 ;
Michael Sammler's avatar
Michael Sammler committed
190
          Goto "#1"
Michael Sammler's avatar
Michael Sammler committed
191
192
193
194
        else
        Goto "#2"
      ]> $
      <[ "#1" :=
195
        locinfo: loc_48 ;
Michael Sammler's avatar
Michael Sammler committed
196
        assert: (LocInfoE loc_49 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_49 ((LocInfoE loc_50 (use{IntOp i32} (LocInfoE loc_51 ((LocInfoE loc_52 (!{PtrOp} (LocInfoE loc_53 ("node1")))) at{struct_list_node} "val")))) ={IntOp i32, IntOp i32} (LocInfoE loc_54 (i2v 1 i32)))))) ;
Michael Sammler's avatar
Michael Sammler committed
197
198
199
200
201
202
203
204
        Return (VOID)
      ]> $
      <[ "#2" :=
        Return (VOID)
      ]> $
    )%E
  |}.
End code.