Skip to content
Snippets Groups Projects
Commit 192811b7 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Flags example cleanup.

parent bfd6fd27
No related branches found
No related tags found
No related merge requests found
Pipeline #33382 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/examples/misc/flags.c
+ 15
− 22
View file @ 192811b7
#include <stdint.h>
//@rc::inlined
//@Definition flags_type := (bool * bool * bool)%type.
//@Record Flags := mkFlags {
//@ flag1 : bool ;
//@ flag2 : bool ;
//@}.
//@
//@Definition flags_from_nat n :=
//@ let b0 := bool_decide (n `mod` 2 = 1) in
//@ let n := n `div` 2 in
//@ let b1 := bool_decide (n `mod` 2 = 1) in
//@ let n := n `div` 2 in
//@ let b2 := bool_decide (n `mod` 2 = 1) in
//@ let n := n `div` 2 in
//@ if bool_decide (n = 0) then Some (b0, b1, b2) else None.
//@Definition nat_encodes_flags n fs :=
//@ Z.testbit 0 n = flag1 fs ∧
//@ Z.testbit 1 n = flag2 fs ∧
//@ ∀ k, k > 1 → ¬ Z.testbit k n.
//@rc::end
typedef struct
[[rc::refined_by("f : flags_type")]]
[[rc::refined_by("f : Flags")]]
[[rc::exists("n : nat")]]
[[rc::constraints("{flags_from_nat n = Some f}")]]
[[rc::constraints("{nat_encodes_flags n f}")]]
flags {
[[rc::field("n @ int<u8>")]]
uint8_t flags;
} flags_t;
#define IS_SET(f, n) (((f).flags >> (n)) % 2 == 1)
#define IS_SET(f, n) (((f).flags >> (n)) & 1)
[[rc::parameters("f1 : bool", "f2 : bool", "f3 : bool")]]
[[rc::parameters("n1 : nat", "n2 : nat", "n3 : nat")]]
[[rc::args("{(f1, f2, f3)} @ flags")]]
[[rc::args("n1 @ int<u32>", "n2 @ int<u32>", "n3 @ int<u32>")]]
[[rc::parameters("fs : Flags", "n1 : nat", "n2 : nat")]]
[[rc::args("fs @ flags", "n1 @ int<u32>", "n2 @ int<u32>")]]
[[rc::requires("{n1 + n2 < it_max u32}")]]
[[rc::requires("{n2 + n3 < it_max u32}")]]
[[rc::requires("{n1 + n3 < it_max u32}")]]
[[rc::requires("{n1 + n2 + n3 < it_max u32}")]]
[[rc::returns("{(if f1 then n1 else 0) + (if f2 then n2 else 0) + (if f3 then n3 else 0)} @ int<u32>")]]
[[rc::returns("{(if flag1 fs then n1 else 0) + (if flag2 fs then n2 else 0)} @ int<u32>")]]
[[rc::trust_me]] // FIXME automation
unsigned int sum(flags_t f, unsigned int arg1, unsigned int arg2, unsigned int arg3){
unsigned int sum(flags_t f, unsigned int arg1, unsigned int arg2){
unsigned int r = 0;
if(IS_SET(f, 0)) r += arg1;
if(IS_SET(f, 1)) r += arg2;
if(IS_SET(f, 2)) r += arg3;
return r;
}
theories/examples/misc/flags_code.v
+ 64
− 107
View file @ 192811b7
......@@ -6,62 +6,41 @@ Set Default Proof Using "Type".
(* Generated from [theories/examples/misc/flags.c]. *)
Section code.
Definition file_0 : string := "theories/examples/misc/flags.c".
Definition loc_2 : location_info := LocationInfo file_0 38 2 38 21.
Definition loc_3 : location_info := LocationInfo file_0 39 2 39 46.
Definition loc_4 : location_info := LocationInfo file_0 40 2 40 46.
Definition loc_5 : location_info := LocationInfo file_0 41 2 41 46.
Definition loc_6 : location_info := LocationInfo file_0 42 2 42 11.
Definition loc_7 : location_info := LocationInfo file_0 42 9 42 10.
Definition loc_8 : location_info := LocationInfo file_0 42 9 42 10.
Definition loc_9 : location_info := LocationInfo file_0 41 36 41 46.
Definition loc_10 : location_info := LocationInfo file_0 41 36 41 37.
Definition loc_11 : location_info := LocationInfo file_0 41 36 41 45.
Definition loc_12 : location_info := LocationInfo file_0 41 36 41 37.
Definition loc_13 : location_info := LocationInfo file_0 41 36 41 37.
Definition loc_14 : location_info := LocationInfo file_0 41 41 41 45.
Definition loc_15 : location_info := LocationInfo file_0 41 41 41 45.
Definition loc_17 : location_info := LocationInfo file_0 41 5 41 34.
Definition loc_18 : location_info := LocationInfo file_0 41 6 41 28.
Definition loc_19 : location_info := LocationInfo file_0 41 6 41 24.
Definition loc_20 : location_info := LocationInfo file_0 41 7 41 16.
Definition loc_21 : location_info := LocationInfo file_0 41 7 41 16.
Definition loc_22 : location_info := LocationInfo file_0 41 7 41 10.
Definition loc_23 : location_info := LocationInfo file_0 41 20 41 23.
Definition loc_24 : location_info := LocationInfo file_0 41 27 41 28.
Definition loc_25 : location_info := LocationInfo file_0 41 32 41 33.
Definition loc_26 : location_info := LocationInfo file_0 40 36 40 46.
Definition loc_27 : location_info := LocationInfo file_0 40 36 40 37.
Definition loc_28 : location_info := LocationInfo file_0 40 36 40 45.
Definition loc_29 : location_info := LocationInfo file_0 40 36 40 37.
Definition loc_30 : location_info := LocationInfo file_0 40 36 40 37.
Definition loc_31 : location_info := LocationInfo file_0 40 41 40 45.
Definition loc_32 : location_info := LocationInfo file_0 40 41 40 45.
Definition loc_34 : location_info := LocationInfo file_0 40 5 40 34.
Definition loc_35 : location_info := LocationInfo file_0 40 6 40 28.
Definition loc_36 : location_info := LocationInfo file_0 40 6 40 24.
Definition loc_37 : location_info := LocationInfo file_0 40 7 40 16.
Definition loc_38 : location_info := LocationInfo file_0 40 7 40 16.
Definition loc_39 : location_info := LocationInfo file_0 40 7 40 10.
Definition loc_40 : location_info := LocationInfo file_0 40 20 40 23.
Definition loc_41 : location_info := LocationInfo file_0 40 27 40 28.
Definition loc_42 : location_info := LocationInfo file_0 40 32 40 33.
Definition loc_43 : location_info := LocationInfo file_0 39 36 39 46.
Definition loc_44 : location_info := LocationInfo file_0 39 36 39 37.
Definition loc_45 : location_info := LocationInfo file_0 39 36 39 45.
Definition loc_46 : location_info := LocationInfo file_0 39 36 39 37.
Definition loc_47 : location_info := LocationInfo file_0 39 36 39 37.
Definition loc_48 : location_info := LocationInfo file_0 39 41 39 45.
Definition loc_49 : location_info := LocationInfo file_0 39 41 39 45.
Definition loc_51 : location_info := LocationInfo file_0 39 5 39 34.
Definition loc_52 : location_info := LocationInfo file_0 39 6 39 28.
Definition loc_53 : location_info := LocationInfo file_0 39 6 39 24.
Definition loc_54 : location_info := LocationInfo file_0 39 7 39 16.
Definition loc_55 : location_info := LocationInfo file_0 39 7 39 16.
Definition loc_56 : location_info := LocationInfo file_0 39 7 39 10.
Definition loc_57 : location_info := LocationInfo file_0 39 20 39 23.
Definition loc_58 : location_info := LocationInfo file_0 39 27 39 28.
Definition loc_59 : location_info := LocationInfo file_0 39 32 39 33.
Definition loc_60 : location_info := LocationInfo file_0 38 19 38 20.
Definition loc_2 : location_info := LocationInfo file_0 32 2 32 21.
Definition loc_3 : location_info := LocationInfo file_0 33 2 33 41.
Definition loc_4 : location_info := LocationInfo file_0 34 2 34 41.
Definition loc_5 : location_info := LocationInfo file_0 35 2 35 11.
Definition loc_6 : location_info := LocationInfo file_0 35 9 35 10.
Definition loc_7 : location_info := LocationInfo file_0 35 9 35 10.
Definition loc_8 : location_info := LocationInfo file_0 34 31 34 41.
Definition loc_9 : location_info := LocationInfo file_0 34 31 34 32.
Definition loc_10 : location_info := LocationInfo file_0 34 31 34 40.
Definition loc_11 : location_info := LocationInfo file_0 34 31 34 32.
Definition loc_12 : location_info := LocationInfo file_0 34 31 34 32.
Definition loc_13 : location_info := LocationInfo file_0 34 36 34 40.
Definition loc_14 : location_info := LocationInfo file_0 34 36 34 40.
Definition loc_16 : location_info := LocationInfo file_0 34 5 34 29.
Definition loc_17 : location_info := LocationInfo file_0 34 6 34 24.
Definition loc_18 : location_info := LocationInfo file_0 34 7 34 16.
Definition loc_19 : location_info := LocationInfo file_0 34 7 34 16.
Definition loc_20 : location_info := LocationInfo file_0 34 7 34 10.
Definition loc_21 : location_info := LocationInfo file_0 34 20 34 23.
Definition loc_22 : location_info := LocationInfo file_0 34 27 34 28.
Definition loc_23 : location_info := LocationInfo file_0 33 31 33 41.
Definition loc_24 : location_info := LocationInfo file_0 33 31 33 32.
Definition loc_25 : location_info := LocationInfo file_0 33 31 33 40.
Definition loc_26 : location_info := LocationInfo file_0 33 31 33 32.
Definition loc_27 : location_info := LocationInfo file_0 33 31 33 32.
Definition loc_28 : location_info := LocationInfo file_0 33 36 33 40.
Definition loc_29 : location_info := LocationInfo file_0 33 36 33 40.
Definition loc_31 : location_info := LocationInfo file_0 33 5 33 29.
Definition loc_32 : location_info := LocationInfo file_0 33 6 33 24.
Definition loc_33 : location_info := LocationInfo file_0 33 7 33 16.
Definition loc_34 : location_info := LocationInfo file_0 33 7 33 16.
Definition loc_35 : location_info := LocationInfo file_0 33 7 33 10.
Definition loc_36 : location_info := LocationInfo file_0 33 20 33 23.
Definition loc_37 : location_info := LocationInfo file_0 33 27 33 28.
Definition loc_38 : location_info := LocationInfo file_0 32 19 32 20.
(* Definition of struct [flags]. *)
Program Definition struct_flags := {|
......@@ -76,8 +55,7 @@ Section code.
f_args := [
("f", layout_of struct_flags);
("arg1", it_layout u32);
("arg2", it_layout u32);
("arg3", it_layout u32)
("arg2", it_layout u32)
];
f_local_vars := [
("r", it_layout u32)
......@@ -86,71 +64,50 @@ Section code.
f_code := (
<[ "#0" :=
"r" <-{ it_layout u32 }
LocInfoE loc_60 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_60 (i2v 0 i32))) ;
locinfo: loc_51 ;
if: LocInfoE loc_51 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_51 ((LocInfoE loc_52 ((LocInfoE loc_53 ((LocInfoE loc_54 (UnOp (CastOp $ IntOp i32) (IntOp u8) (LocInfoE loc_54 (use{it_layout u8} (LocInfoE loc_55 ((LocInfoE loc_56 ("f")) at{struct_flags} "flags")))))) >>{IntOp i32, IntOp i32} (LocInfoE loc_57 (i2v 0 i32)))) %{IntOp i32, IntOp i32} (LocInfoE loc_58 (i2v 2 i32)))) ={IntOp i32, IntOp i32} (LocInfoE loc_59 (i2v 1 i32)))))
LocInfoE loc_38 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_38 (i2v 0 i32))) ;
locinfo: loc_31 ;
if: LocInfoE loc_31 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_31 ((LocInfoE loc_32 ((LocInfoE loc_33 (UnOp (CastOp $ IntOp i32) (IntOp u8) (LocInfoE loc_33 (use{it_layout u8} (LocInfoE loc_34 ((LocInfoE loc_35 ("f")) at{struct_flags} "flags")))))) >>{IntOp i32, IntOp i32} (LocInfoE loc_36 (i2v 0 i32)))) &{IntOp i32, IntOp i32} (LocInfoE loc_37 (i2v 1 i32)))))
then
locinfo: loc_43 ;
Goto "#8"
locinfo: loc_23 ;
Goto "#5"
else
locinfo: loc_34 ;
Goto "#9"
locinfo: loc_16 ;
Goto "#6"
]> $
<[ "#1" :=
locinfo: loc_34 ;
if: LocInfoE loc_34 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_34 ((LocInfoE loc_35 ((LocInfoE loc_36 ((LocInfoE loc_37 (UnOp (CastOp $ IntOp i32) (IntOp u8) (LocInfoE loc_37 (use{it_layout u8} (LocInfoE loc_38 ((LocInfoE loc_39 ("f")) at{struct_flags} "flags")))))) >>{IntOp i32, IntOp i32} (LocInfoE loc_40 (i2v 1 i32)))) %{IntOp i32, IntOp i32} (LocInfoE loc_41 (i2v 2 i32)))) ={IntOp i32, IntOp i32} (LocInfoE loc_42 (i2v 1 i32)))))
locinfo: loc_16 ;
if: LocInfoE loc_16 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_16 ((LocInfoE loc_17 ((LocInfoE loc_18 (UnOp (CastOp $ IntOp i32) (IntOp u8) (LocInfoE loc_18 (use{it_layout u8} (LocInfoE loc_19 ((LocInfoE loc_20 ("f")) at{struct_flags} "flags")))))) >>{IntOp i32, IntOp i32} (LocInfoE loc_21 (i2v 1 i32)))) &{IntOp i32, IntOp i32} (LocInfoE loc_22 (i2v 1 i32)))))
then
locinfo: loc_26 ;
Goto "#6"
locinfo: loc_8 ;
Goto "#3"
else
locinfo: loc_17 ;
Goto "#7"
locinfo: loc_5 ;
Goto "#4"
]> $
<[ "#2" :=
locinfo: loc_17 ;
if: LocInfoE loc_17 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_17 ((LocInfoE loc_18 ((LocInfoE loc_19 ((LocInfoE loc_20 (UnOp (CastOp $ IntOp i32) (IntOp u8) (LocInfoE loc_20 (use{it_layout u8} (LocInfoE loc_21 ((LocInfoE loc_22 ("f")) at{struct_flags} "flags")))))) >>{IntOp i32, IntOp i32} (LocInfoE loc_23 (i2v 2 i32)))) %{IntOp i32, IntOp i32} (LocInfoE loc_24 (i2v 2 i32)))) ={IntOp i32, IntOp i32} (LocInfoE loc_25 (i2v 1 i32)))))
then
locinfo: loc_9 ;
Goto "#4"
else
locinfo: loc_6 ;
Goto "#5"
locinfo: loc_5 ;
Return (LocInfoE loc_6 (use{it_layout u32} (LocInfoE loc_7 ("r"))))
]> $
<[ "#3" :=
locinfo: loc_6 ;
Return (LocInfoE loc_7 (use{it_layout u32} (LocInfoE loc_8 ("r"))))
]> $
<[ "#4" :=
locinfo: loc_9 ;
LocInfoE loc_10 ("r") <-{ it_layout u32 }
LocInfoE loc_11 ((LocInfoE loc_12 (use{it_layout u32} (LocInfoE loc_13 ("r")))) +{IntOp u32, IntOp u32} (LocInfoE loc_14 (use{it_layout u32} (LocInfoE loc_15 ("arg3"))))) ;
locinfo: loc_6 ;
Goto "#3"
]> $
<[ "#5" :=
locinfo: loc_6 ;
Goto "#3"
]> $
<[ "#6" :=
locinfo: loc_26 ;
LocInfoE loc_27 ("r") <-{ it_layout u32 }
LocInfoE loc_28 ((LocInfoE loc_29 (use{it_layout u32} (LocInfoE loc_30 ("r")))) +{IntOp u32, IntOp u32} (LocInfoE loc_31 (use{it_layout u32} (LocInfoE loc_32 ("arg2"))))) ;
locinfo: loc_17 ;
locinfo: loc_8 ;
LocInfoE loc_9 ("r") <-{ it_layout u32 }
LocInfoE loc_10 ((LocInfoE loc_11 (use{it_layout u32} (LocInfoE loc_12 ("r")))) +{IntOp u32, IntOp u32} (LocInfoE loc_13 (use{it_layout u32} (LocInfoE loc_14 ("arg2"))))) ;
locinfo: loc_5 ;
Goto "#2"
]> $
<[ "#7" :=
locinfo: loc_17 ;
<[ "#4" :=
locinfo: loc_5 ;
Goto "#2"
]> $
<[ "#8" :=
locinfo: loc_43 ;
LocInfoE loc_44 ("r") <-{ it_layout u32 }
LocInfoE loc_45 ((LocInfoE loc_46 (use{it_layout u32} (LocInfoE loc_47 ("r")))) +{IntOp u32, IntOp u32} (LocInfoE loc_48 (use{it_layout u32} (LocInfoE loc_49 ("arg1"))))) ;
locinfo: loc_34 ;
<[ "#5" :=
locinfo: loc_23 ;
LocInfoE loc_24 ("r") <-{ it_layout u32 }
LocInfoE loc_25 ((LocInfoE loc_26 (use{it_layout u32} (LocInfoE loc_27 ("r")))) +{IntOp u32, IntOp u32} (LocInfoE loc_28 (use{it_layout u32} (LocInfoE loc_29 ("arg1"))))) ;
locinfo: loc_16 ;
Goto "#1"
]> $
<[ "#9" :=
locinfo: loc_34 ;
<[ "#6" :=
locinfo: loc_16 ;
Goto "#1"
]> $∅
)%E
......
theories/examples/misc/flags_spec.v
+ 19
− 20
View file @ 192811b7
......@@ -8,24 +8,23 @@ Section spec.
(* Inlined code. *)
Definition flags_type := (bool * bool * bool)%type.
Record Flags := mkFlags {
flag1 : bool ;
flag2 : bool ;
}.
Definition flags_from_nat n :=
let b0 := bool_decide (n `mod` 2 = 1) in
let n := n `div` 2 in
let b1 := bool_decide (n `mod` 2 = 1) in
let n := n `div` 2 in
let b2 := bool_decide (n `mod` 2 = 1) in
let n := n `div` 2 in
if bool_decide (n = 0) then Some (b0, b1, b2) else None.
Definition nat_encodes_flags n fs :=
Z.testbit 0 n = flag1 fs ∧
Z.testbit 1 n = flag2 fs ∧
∀ k, k > 1 → ¬ Z.testbit k n.
(* Definition of type [flags]. *)
Definition flags_rec : (flags_type -d> typeO) → (flags_type -d> typeO) := (λ self f,
Definition flags_rec : (Flags -d> typeO) → (Flags -d> typeO) := (λ self f,
tyexists (λ n : nat,
constrained (struct struct_flags [@{type}
(n @ (int (u8)))
]) (
⌜flags_from_nat n = Some f⌝
⌜nat_encodes_flags n f⌝
))
)%I.
Typeclasses Opaque flags_rec.
......@@ -34,17 +33,17 @@ Section spec.
Proof. solve_type_proper. Qed.
Definition flags : rtype := {|
rty_type := flags_type;
rty_type := Flags;
rty r__ := fixp flags_rec r__
|}.
Lemma flags_unfold (f : flags_type) :
Lemma flags_unfold (f : Flags) :
(f @ flags)%I ≡@{type} (
tyexists (λ n : nat,
constrained (struct struct_flags [@{type}
(n @ (int (u8)))
]) (
⌜flags_from_nat n = Some f⌝
⌜nat_encodes_flags n f⌝
))
)%I.
Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.
......@@ -54,18 +53,18 @@ Section spec.
{| rmovable 'f := movable_eq _ _ (flags_unfold f) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance flags_simplify_hyp_place_inst l_ β_ (f : flags_type) :
Global Instance flags_simplify_hyp_place_inst l_ β_ (f : Flags) :
SimplifyHypPlace l_ β_ (f @ flags)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (flags_unfold _)).
Global Instance flags_simplify_goal_place_inst l_ β_ (f : flags_type) :
Global Instance flags_simplify_goal_place_inst l_ β_ (f : Flags) :
SimplifyGoalPlace l_ β_ (f @ flags)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (flags_unfold _)).
Global Program Instance flags_simplify_hyp_val_inst v_ (f : flags_type) :
Global Program Instance flags_simplify_hyp_val_inst v_ (f : Flags) :
SimplifyHypVal v_ (f @ flags)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (flags_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance flags_simplify_goal_val_inst v_ (f : flags_type) :
Global Program Instance flags_simplify_goal_val_inst v_ (f : Flags) :
SimplifyGoalVal v_ (f @ flags)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (flags_unfold _) T _).
Next Obligation. done. Qed.
......@@ -74,8 +73,8 @@ Section spec.
(* Specifications for function [sum]. *)
Definition type_of_sum :=
fn(∀ (f1, f2, f3, n1, n2, n3) : bool * bool * bool * nat * nat * nat; (((f1, f2, f3)) @ (flags)), (n1 @ (int (u32))), (n2 @ (int (u32))), (n3 @ (int (u32))); ⌜n1 + n2 < it_max u32⌝ ∗ ⌜n2 + n3 < it_max u32⌝ ∗ ⌜n1 + n3 < it_max u32⌝ ∗ ⌜n1 + n2 + n3 < it_max u32⌝)
→ ∃ () : (), (((if f1 then n1 else 0) + (if f2 then n2 else 0) + (if f3 then n3 else 0)) @ (int (u32))); True.
fn(∀ (fs, n1, n2) : Flags * nat * nat; (fs @ (flags)), (n1 @ (int (u32))), (n2 @ (int (u32))); ⌜n1 + n2 < it_max u32⌝)
→ ∃ () : (), (((if flag1 fs then n1 else 0) + (if flag2 fs then n2 else 0)) @ (int (u32))); True.
End spec.
Typeclasses Opaque flags_rec.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment