-
Notifications
You must be signed in to change notification settings - Fork 0
/
ebpf_proof.v
88 lines (84 loc) · 3.44 KB
/
ebpf_proof.v
1
2
3
4
5
6
7
8
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
(* (C) 2021 Digamma.ai *)
Require Import common.
Definition Gprog := ltac:(with_library prog [__mark_reg32_unbounded_spec;
__reg64_bound_s32_spec;
__reg64_bound_u32_spec;
(___reg_combine_64_into_32_CORRECT,
__reg_combine_64_into_32_spec);
__reg_deduce_bounds_spec;
__reg_bound_offset_spec;
__update_reg_bounds_spec]).
Theorem __reg_combine_64_into_32_correctness :
semax_body Vprog Gprog f___reg_combine_64_into_32_CORRECT
(___reg_combine_64_into_32_CORRECT, __reg_combine_64_into_32_spec).
Proof.
start_function.
forward_call (reg,
ref_obj_id,
s32_min_value, s32_max_value,
u32_min_value, u32_max_value,
smin_value64, smax_value64, umin_value64, umax_value64).
forward.
unfold reg_struct.
forward_call smin_value64.
forward_if (temp _t'2 (Val.of_bool (if (Sbounds smin_value64)
then (Sbounds smax_value64)
else false))).
- repeat forward.
forward_call smax_value64.
forward_H H.
- forward_H H.
- deadvars!.
remember (if Sbounds smin_value64
then Sbounds smax_value64
else false) as b.
forward_if (PROP ( )
LOCAL (temp _t'2 (Val.of_bool b);
temp _reg reg)
SEP (data_at Tsh (Tstruct _bpf_reg_state noattr)
(Vint ref_obj_id,
(Vint (if b then (int64_to_32 smin_value64) else S32Min),
(Vint (if b then (int64_to_32 smax_value64) else S32Max),
(Vint U32Min,
(Vint U32Max,
(Vlong smin_value64,
(Vlong smax_value64, (Vlong umin_value64, Vlong umax_value64))))))))
reg)).
+ forward_H H.
+ forward_H H.
+ forward.
forward_call umin_value64.
deadvars!.
forward_if (temp _t'5 (Val.of_bool (if (Ubounds umin_value64)
then (Ubounds umax_value64)
else false))).
-- repeat forward.
forward_call umax_value64.
forward_H H.
-- forward_H H.
-- deadvars!.
remember (if Ubounds umin_value64
then Ubounds umax_value64
else false) as bb.
forward_if (PROP ( )
LOCAL (temp _t'5 (Val.of_bool bb);
temp _reg reg)
SEP (data_at Tsh (Tstruct _bpf_reg_state noattr)
(Vint ref_obj_id,
(Vint (if b then (int64_to_32 smin_value64) else S32Min),
(Vint (if b then (int64_to_32 smax_value64) else S32Max),
(Vint (if bb then (int64_to_32 umin_value64) else U32Min),
(Vint (if bb then (int64_to_32 umax_value64) else U32Max),
(Vlong smin_value64,
(Vlong smax_value64, (Vlong umin_value64, Vlong umax_value64))))))))
reg)).
++ forward_H H.
++ forward_H H.
++ repeat forward_call (reg).
Exists (if b then int64_to_32 smin_value64 else S32Min).
Exists (if b then int64_to_32 smax_value64 else S32Max).
Exists (if bb then int64_to_32 umin_value64 else U32Min).
Exists (if bb then int64_to_32 umax_value64 else U32Max).
entailer!.
repeat break_if; try intuition.
Qed.