1 /*
2 * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3 *
4 * Licensed under the Apache License, Version 2.0 (the "License").
5 * You may not use this file except in compliance with the License.
6 * A copy of the License is located at
7 *
8 * http://aws.amazon.com/apache2.0
9 *
10 * or in the "license" file accompanying this file. This file is distributed
11 * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
12 * express or implied. See the License for the specific language governing
13 * permissions and limitations under the License.
14 */
15
16 /* clang-format off */
17 #include "preamble.h"
18
19 struct aws_allocator *aws_default_allocator()
20 _(ensures \wrapped(\result))
21 ;
22
23 uint64_t next_timestamp();
24
clock(uint64_t * timestamp)25 int clock(uint64_t *timestamp)
26 _(writes timestamp)
27 {
28 *timestamp = next_timestamp();
29 return AWS_OP_SUCCESS;
30 }
31
test_new_destroy()32 void test_new_destroy()
33 {
34 struct aws_allocator *alloc = aws_default_allocator();
35 _(ghost \claim c_mutex)
36 struct aws_event_loop *event_loop = aws_event_loop_new_default(alloc, clock, _(out c_mutex));
37 if (!event_loop) return;
38 _(ghost \claim c_event_loop;)
39 _(ghost c_event_loop = \make_claim({event_loop}, event_loop->\closed);)
40 s_destroy(event_loop _(ghost c_event_loop) _(ghost c_mutex));
41 }
42
43 void on_event(
44 struct aws_event_loop *event_loop,
45 struct aws_io_handle *handle,
46 int events,
47 void *user_data _(ghost \claim(c))
48 );
49
test_subscribe_unsubscribe(struct aws_event_loop * event_loop _ (ghost\\claim (c_event_loop))_ (ghost\\claim (c_mutex)))50 void test_subscribe_unsubscribe(struct aws_event_loop *event_loop
51 _(ghost \claim(c_event_loop))
52 _(ghost \claim(c_mutex))
53 )
54 _(always c_event_loop, event_loop->\closed)
55 _(requires \wrapped(c_mutex) && \claims_object(c_mutex, &(epoll_loop_of(event_loop)->task_pre_queue_mutex)))
56 _(writes event_loop)
57 _(updates &epoll_loop_of(event_loop)->scheduler)
58 {
59 struct aws_io_handle *handle = malloc(sizeof(struct aws_io_handle));
60 if (!handle) return;
61 handle->data.fd = 1; /* model successful open() */
62 _(wrap handle)
63 int err = s_subscribe_to_io_events(event_loop, handle, 0, on_event, NULL, _(ghost c_event_loop));
64 if (err) {
65 return;
66 }
67 _(assert wf_cio_handle(handle))
68 _(assert \wrapped((struct epoll_event_data *)handle->additional_data))
69 _(assert ((struct epoll_event_data *)handle->additional_data)->\owner == \me)
70 s_unsubscribe_from_io_events(event_loop, handle _(ghost c_event_loop) _(ghost c_mutex));
71 }
72
task_fn(struct aws_task * task,void * arg,enum aws_task_status)73 void task_fn(struct aws_task *task, void *arg, enum aws_task_status) {
74 (void)task;
75 (void)arg;
76 }
77
test_schedule_cancel(struct aws_event_loop * event_loop _ (ghost\\claim (c_event_loop))_ (ghost\\claim (c_mutex)))78 void test_schedule_cancel(struct aws_event_loop *event_loop
79 _(ghost \claim(c_event_loop))
80 _(ghost \claim(c_mutex))
81 )
82 _(requires \wrapped(event_loop))
83 _(always c_event_loop, event_loop->\closed)
84 _(requires \wrapped(c_mutex) && \claims_object(c_mutex, &(epoll_loop_of(event_loop)->task_pre_queue_mutex)))
85 _(updates &epoll_loop_of(event_loop)->scheduler)
86 {
87 struct aws_task *task = malloc(sizeof(struct aws_task));
88 if (!task) return;
89 aws_task_init(task, task_fn, NULL, "test_task");
90 s_schedule_task_now(event_loop, task _(ghost c_event_loop) _(ghost c_mutex));
91 s_cancel_task(event_loop, task);
92 }
93 /* clang-format on */
94