Commit bbba4f9e authored by Michael Sammler's avatar Michael Sammler
Browse files

added support for container of

parent 36fe970f
Pipeline #39185 passed with stage
in 21 minutes and 56 seconds
......@@ -39,3 +39,4 @@
-Q _build/default/examples/proofs/buddy_alloc refinedc.examples.buddy_alloc
-Q _build/default/examples/proofs/wrapping_add refinedc.examples.wrapping_add
-Q _build/default/linux/proofs/early_alloc refinedc.linux.early_alloc
-Q _build/default/examples/proofs/container_of refinedc.examples.container_of
#define container_of(ptr, type, member) (type *)( (char *)(ptr) - offsetof(type,member) )
struct test {
int a;
int b;
};
[[rc::returns("{4} @ int<i32>")]]
int container_of_test() {
struct test t = {.a = 1, .b = 2};
int *b = &t.b;
*b = 3;
struct test *pt = container_of(b, struct test, b);
pt->a = 4;
return pt->a;
}
; Generated by [refinedc], do not edit.
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.container_of)
(theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
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/container_of.c]. *)
Section code.
Definition file_0 : string := "examples/container_of.c".
Definition loc_2 : location_info := LocationInfo file_0 11 2 11 35.
Definition loc_3 : location_info := LocationInfo file_0 12 2 12 16.
Definition loc_4 : location_info := LocationInfo file_0 13 2 13 9.
Definition loc_5 : location_info := LocationInfo file_0 14 2 14 77.
Definition loc_6 : location_info := LocationInfo file_0 15 2 15 12.
Definition loc_7 : location_info := LocationInfo file_0 16 2 16 15.
Definition loc_8 : location_info := LocationInfo file_0 16 9 16 14.
Definition loc_9 : location_info := LocationInfo file_0 16 9 16 14.
Definition loc_10 : location_info := LocationInfo file_0 16 9 16 11.
Definition loc_11 : location_info := LocationInfo file_0 16 9 16 11.
Definition loc_12 : location_info := LocationInfo file_0 15 2 15 7.
Definition loc_13 : location_info := LocationInfo file_0 15 2 15 4.
Definition loc_14 : location_info := LocationInfo file_0 15 2 15 4.
Definition loc_15 : location_info := LocationInfo file_0 15 10 15 11.
Definition loc_16 : location_info := LocationInfo file_0 14 20 14 76.
Definition loc_17 : location_info := LocationInfo file_0 14 35 14 76.
Definition loc_18 : location_info := LocationInfo file_0 14 37 14 48.
Definition loc_19 : location_info := LocationInfo file_0 14 45 14 48.
Definition loc_20 : location_info := LocationInfo file_0 14 45 14 48.
Definition loc_21 : location_info := LocationInfo file_0 14 51 14 74.
Definition loc_24 : location_info := LocationInfo file_0 13 2 13 4.
Definition loc_25 : location_info := LocationInfo file_0 13 3 13 4.
Definition loc_26 : location_info := LocationInfo file_0 13 3 13 4.
Definition loc_27 : location_info := LocationInfo file_0 13 7 13 8.
Definition loc_28 : location_info := LocationInfo file_0 12 11 12 15.
Definition loc_29 : location_info := LocationInfo file_0 12 12 12 15.
Definition loc_30 : location_info := LocationInfo file_0 12 12 12 13.
Definition loc_34 : location_info := LocationInfo file_0 11 32 11 33.
Definition loc_35 : location_info := LocationInfo file_0 11 24 11 25.
(* Definition of struct [test]. *)
Program Definition struct_test := {|
sl_members := [
(Some "a", it_layout i32);
(Some "b", it_layout i32)
];
|}.
Solve Obligations with solve_struct_obligations.
(* Definition of function [container_of_test]. *)
Definition impl_container_of_test : function := {|
f_args := [
];
f_local_vars := [
("b", LPtr);
("t", layout_of struct_test);
("pt", LPtr)
];
f_init := "#0";
f_code := (
<[ "#0" :=
"t" <-{ layout_of struct_test }
StructInit struct_test [
("a", LocInfoE loc_35 (i2v 1 i32) : expr) ;
("b", LocInfoE loc_34 (i2v 2 i32) : expr)
] ;
"b" <-{ LPtr }
LocInfoE loc_28 (&(LocInfoE loc_29 ((LocInfoE loc_30 ("t")) at{struct_test} "b"))) ;
locinfo: loc_4 ;
LocInfoE loc_25 (!{LPtr} (LocInfoE loc_26 ("b"))) <-{ it_layout i32 }
LocInfoE loc_27 (i2v 3 i32) ;
"pt" <-{ LPtr }
LocInfoE loc_16 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_17 ((LocInfoE loc_18 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_19 (use{LPtr} (LocInfoE loc_20 ("b")))))) at_neg_offset{it_layout u8, PtrOp, IntOp size_t} (LocInfoE loc_21 ((OffsetOf (struct_test) ("b"))))))) ;
locinfo: loc_6 ;
LocInfoE loc_12 ((LocInfoE loc_13 (!{LPtr} (LocInfoE loc_14 ("pt")))) at{struct_test} "a") <-{ it_layout i32 }
LocInfoE loc_15 (i2v 4 i32) ;
locinfo: loc_7 ;
Return (LocInfoE loc_8 (use{it_layout i32} (LocInfoE loc_9 ((LocInfoE loc_10 (!{LPtr} (LocInfoE loc_11 ("pt")))) at{struct_test} "a"))))
]> $
)%E
|}.
End code.
From refinedc.typing Require Import typing.
From refinedc.examples.container_of Require Import generated_code.
From refinedc.examples.container_of Require Import generated_spec.
Set Default Proof Using "Type".
(* Generated from [examples/container_of.c]. *)
Section proof_container_of_test.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [container_of_test]. *)
Lemma type_container_of_test :
typed_function impl_container_of_test type_of_container_of_test.
Proof.
start_function "container_of_test" ([]) => local_b local_t local_pt.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "container_of_test" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: print_sidecondition_goal "container_of_test".
Qed.
End proof_container_of_test.
From refinedc.typing Require Import typing.
From refinedc.examples.container_of Require Import generated_code.
Set Default Proof Using "Type".
(* Generated from [examples/container_of.c]. *)
Section spec.
Context `{!typeG Σ} `{!globalG Σ}.
(* Type definitions. *)
(* Specifications for function [container_of_test]. *)
Definition type_of_container_of_test :=
fn( () : (); True) () : (), ((4) @ (int (i32))); True.
End spec.
generated_proof_container_of_test.v
......@@ -110,7 +110,7 @@ let rec translate_int_type : loc -> i_type -> Coq_ast.int_type = fun loc i ->
| Wchar_t -> not_impl loc "layout_of (Wchar_t)"
| Wint_t -> not_impl loc "layout_of (Win_t)"
| Size_t -> ItSize_t(false)
| Ptrdiff_t -> not_impl loc "layout_of (Ptrdiff_t)"
| Ptrdiff_t -> ItSize_t(true)
(** [layout_of fa c_ty] translates the C type [c_ty] into a layout. Note that
argument [fa] must be set to [true] when in function arguments, since this
......@@ -265,6 +265,12 @@ let struct_data : ail_expr -> string * bool = fun e ->
| GenRValueType(_ ) -> assert false
| GenLValueType(_,_ ,_) -> assert false
let struct_data_of_type : c_type -> string * bool = fun Ctype.(Ctype(_, c_ty)) ->
match c_ty with
| Struct(s) -> (sym_to_str s, false)
| Union(s) -> (sym_to_str s, true)
| _ -> assert false
let strip_expr (AilSyntax.AnnotatedExpression(_,_,_,e)) = e
let rec function_decls decls =
......@@ -522,7 +528,9 @@ let rec translate_expr : bool -> op_type option -> ail_expr -> expr * calls =
(locate (Var(ret_id, false)), l @ [(coq_loc, ret_id, e, es)])
end
| AilEassert(e) -> not_impl loc "expr assert nested"
| AilEoffsetof(c_ty,is) -> not_impl loc "expr offsetof"
| AilEoffsetof(c_ty,is) ->
let (struct_name, from_union) = struct_data_of_type c_ty in
(locate (OffsetOf(struct_name,from_union, id_to_str is)), [])
| AilEgeneric(e,gas) -> not_impl loc "expr generic"
| AilEarray(b,c_ty,oes) -> not_impl loc "expr array"
| AilEstruct(sym,fs) when lval -> not_impl loc "Struct initializer not supported in lvalue context"
......
......@@ -50,6 +50,7 @@ and expr_aux =
| Use of bool (* Atomic? *) * layout * expr
| AddrOf of expr
| GetMember of expr * string * bool (* From_union? *) * string
| OffsetOf of string * bool (* From_union? *) * string
| AnnotExpr of int * coq_expr * expr
| Struct of string * (string * expr) list
| Macro of string * string list * expr list * expr
......
......@@ -147,6 +147,9 @@ let rec pp_expr : Coq_ast.expr pp = fun ff e ->
| (OpPtr(l), OpInt(_), AddOp) ->
pp "(%a) at_offset{%a, PtrOp, %a} (%a)" pp_expr e1
(pp_layout false) l pp_op_type ty2 pp_expr e2
| (OpPtr(l), OpInt(_), SubOp) ->
pp "(%a) at_neg_offset{%a, PtrOp, %a} (%a)" pp_expr e1
(pp_layout false) l pp_op_type ty2 pp_expr e2
| (OpPtr(_), OpInt(_), _) ->
panic_no_pos "Binop [%a] not supported on pointers."
pp_bin_op op
......@@ -178,6 +181,10 @@ let rec pp_expr : Coq_ast.expr pp = fun ff e ->
pp "(%a) at{struct_%s} %S" pp_expr e name field
| GetMember(e,name,true ,field) ->
pp "(%a) at_union{union_%s} %S" pp_expr e name field
| OffsetOf(name,false,field) ->
pp "(OffsetOf (struct_%s) (%S))" name field
| OffsetOf(name,true,field) ->
pp "(OffsetOfUnion (union_%s) (%S))" name field
| AnnotExpr(i,coq_e,e) ->
pp "AnnotExpr %i%%nat %a (%a)" i
(pp_simple_coq_expr true) coq_e pp_expr e
......
......@@ -79,7 +79,8 @@ static inline void __list_add(struct list_head *new,
struct list_head *prev,
struct list_head *next)
{
if (!__list_add_valid(new, prev, next))
/* if (!__list_add_valid(new, prev, next)) */
if (__list_add_valid(new, prev, next) == (bool)0)
return;
next->prev = new;
......@@ -130,7 +131,8 @@ static inline void __list_del(struct list_head * prev, struct list_head * next)
static inline void __list_del_entry(struct list_head *entry)
{
if (!__list_del_entry_valid(entry))
/* if (!__list_del_entry_valid(entry)) */
if (__list_del_entry_valid(entry) == (bool)0)
return;
__list_del(entry->prev, entry->next);
......@@ -294,7 +296,10 @@ static void __hyp_attach_page(struct hyp_pool *pool,
/* Otherwise, coalesce the buddies and go one level up */
list_del_init(&buddy->node);
buddy->order = HYP_NO_ORDER;
p = (p < buddy) ? p : buddy;
if (buddy < p) {
p = buddy;
}
/* p = (p < buddy) ? p : buddy; */
}
p->order = order;
......@@ -353,8 +358,10 @@ static void clear_hyp_page(struct hyp_page *p)
{
unsigned long i;
for (i = 0; i < (1 << p->order); i++)
clear_page(hyp_page_to_virt(p) + (i << PAGE_SHIFT));
/* for (i = 0; i < (1 << p->order); i++) */
for (i = 0; i < (1UL << p->order); i++)
clear_page((unsigned char *)hyp_page_to_virt(p) + (i << PAGE_SHIFT));
/* clear_page(hyp_page_to_virt(p) + (i << PAGE_SHIFT)); */
}
static void * __hyp_alloc_pages(struct hyp_pool *pool, gfp_t mask,
......@@ -388,9 +395,14 @@ void * hyp_alloc_pages(struct hyp_pool *pool, gfp_t mask,
p = __hyp_alloc_pages(pool, mask, order);
/* nvhe_spin_unlock(&pool->lock); */
return p ? hyp_page_to_virt(p) : NULL;
/* return p ? hyp_page_to_virt(p) : NULL; */
if (p) {
return hyp_page_to_virt(p);
} else {
return NULL;
}
}
#if 0
/* hyp_vmemmap must be backed beforehand */
int hyp_pool_extend_used(struct hyp_pool *pool, phys_addr_t phys,
unsigned int nr_pages,
......@@ -425,7 +437,7 @@ int hyp_pool_extend_used(struct hyp_pool *pool, phys_addr_t phys,
return 0;
}
#endif
void hyp_pool_init(struct hyp_pool *pool)
{
unsigned int i;
......
......@@ -288,7 +288,7 @@ Inductive bin_op : Set :=
| AddOp | SubOp | MulOp | DivOp | ModOp | AndOp | OrOp | XorOp | ShlOp
| ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp
(* Ptr is the second argument and pffset the first *)
| PtrOffsetOp (ly : layout).
| PtrOffsetOp (ly : layout) | PtrNegOffsetOp (ly : layout).
Inductive un_op : Set :=
| NotBoolOp | NotIntOp | NegOp | CastOp (ot : op_type).
......@@ -756,6 +756,11 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
(* TODO: should we have an alignment check here? *)
0 o
eval_bin_op (PtrOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly} o))
| PtrNegOffsetOpIP v1 v2 σ o l ly it:
val_to_int v1 it = Some o
val_to_loc v2 = Some l
(* TODO: should we have an alignment check here? *)
eval_bin_op (PtrNegOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly} -o))
| EqOpPNull v1 v2 σ l v:
heap_loc_in_bounds l 0%nat σ
val_to_loc v1 = Some l
......
......@@ -249,6 +249,18 @@ Proof.
- move => ->. by apply PtrOffsetOpIP.
Qed.
Lemma wp_ptr_neg_offset Φ vl l E it o ly vo:
val_to_loc vl = Some l
val_to_int vo it = Some o
Φ (val_of_loc (l offset{ly} -o)) - WP Val vl at_neg_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
Proof.
iIntros (Hvl Hvo) "HΦ".
iApply wp_binop_det. iSplit; last done.
iIntros (σ v) "_ !%". split.
- inversion 1. by simplify_eq.
- move => ->. by apply PtrNegOffsetOpIP.
Qed.
Lemma wp_get_member Φ vl l sl n E:
val_to_loc vl = Some l
is_Some (index_of sl.(sl_members) n)
......@@ -272,6 +284,25 @@ Lemma wp_get_member_union Φ vl l ul n E:
Φ (val_of_loc (l at_union{ul} n)) - WP Val vl at_union{ul} n @ E {{ Φ }}.
Proof. iIntros (->%val_of_to_loc) "?". rewrite /GetMemberUnion/GetMemberUnionLoc. by iApply @wp_value. Qed.
Lemma wp_offset_of Φ s m i E:
offset_of s.(sl_members) m = Some i
( v, val_of_int i size_t = Some v - Φ v) -
WP OffsetOf s m @ E {{ Φ }}.
Proof.
rewrite /OffsetOf. iIntros (Ho) "HΦ".
have [|? Hs]:= (val_of_int_is_some size_t i). {
split; first by rewrite /min_int/=; lia.
move: Ho => /fmap_Some[?[?->]].
by apply offset_of_bound.
}
rewrite Ho /= Hs /=. iApply @wp_value.
by iApply "HΦ".
Qed.
Lemma wp_offset_of_union Φ ul m E:
Φ (i2v 0 size_t) - WP OffsetOfUnion ul m @ E {{ Φ }}.
Proof. by iApply @wp_value. Qed.
Lemma wp_skip Φ v E:
Φ v - WP SkipE (Val v) @ E {{ Φ }}.
Proof.
......
......@@ -49,6 +49,8 @@ Notation "e1 ^{ ot1 , ot2 } e2" := (BinOp XorOp ot1 ot2 e1%E e2%E)
(* The offset must be evaluated first for the type system to work, thus the order is switched here. *)
Notation "e1 'at_offset{' ly , ot1 , ot2 } e2" := (BinOp (PtrOffsetOp ly) ot2 ot1 e2%E e1%E)
(at level 70, format "e1 at_offset{ ly , ot1 , ot2 } e2") : expr_scope.
Notation "e1 'at_neg_offset{' ly , ot1 , ot2 } e2" := (BinOp (PtrNegOffsetOp ly) ot2 ot1 e2%E e1%E)
(at level 70, format "e1 at_neg_offset{ ly , ot1 , ot2 } e2") : expr_scope.
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
Notation "e1 <-{ ly , o } e2 ; s" := (Assign o ly e1%E e2%E s%E)
(at level 80, s at level 200, format "e1 <-{ ly , o } e2 ; s") : expr_scope.
......@@ -152,8 +154,8 @@ Definition offset_of_idx (s : field_list) (i : nat) : nat :=
sum_list (take i (ly_size <$> s.*2)).
Definition index_of (s : field_list) (n : var_name) : option nat :=
fst <$> list_find (λ x, x.1 = Some n) s.
Definition offset_of (s : field_list) (n : var_name) : nat :=
default 0%nat ((λ idx, offset_of_idx s idx) <$> index_of s n).
Definition offset_of (s : field_list) (n : var_name) : option nat :=
(λ idx, offset_of_idx s idx) <$> index_of s n.
Definition field_idx_of_idx (s : field_list) (i : nat) : nat :=
length (field_names (take i s)).
Fixpoint field_index_of (s : field_list) (n : var_name) : option nat :=
......@@ -253,15 +255,29 @@ Lemma pad_struct_snoc_None {A} s ly (ls : list A) f :
pad_struct (s ++ [(None, ly)]) ls f = pad_struct s ls f ++ [f ly].
Proof. elim: s ls => //=. move => -[n' ly'] s IH ls /=. f_equal. by apply IH. Qed.
Lemma offset_of_cons' n n' ly s:
offset_of ((n', ly)::s) n = (if decide (n' = Some n) then Some 0 else (λ m, ly_size ly + m) <$> (offset_of s n))%nat.
Proof. rewrite /offset_of/= index_of_cons. case_decide => //=. destruct (index_of s n) eqn: Hfind => //=. Qed.
Lemma offset_of_cons n n' ly s:
n' = Some n n field_names s
offset_of ((n', ly)::s) n = (if decide (n' = Some n) then 0 else ly_size ly + offset_of s n)%nat.
default 0%nat (offset_of ((n', ly)::s) n) = (if decide (n' = Some n) then 0 else ly_size ly + (default 0%nat (offset_of s n)))%nat.
Proof.
rewrite /offset_of/= index_of_cons. case_decide => //= -[|/elem_of_list_omap[x Hin]]//.
destruct (index_of s n) eqn: Hfind => //=.
move: Hfind => /fmap_None/list_find_None /Forall_forall Hfind. set_solver.
Qed.
Lemma offset_of_from_in m s:
Some m s.*1 n, offset_of s m = Some n.
Proof.
elim: s. set_solver.
move => [??]? IH. rewrite offset_of_cons'. csimpl => ?.
case_decide => //; [ naive_solver |].
have [|? ->]:= IH. by set_solver.
naive_solver.
Qed.
Lemma offset_of_bound i sl:
offset_of_idx sl.(sl_members) i max_int size_t.
Proof.
......@@ -290,17 +306,22 @@ Proof.
Qed.
Definition GetMember (e : expr) (s : struct_layout) (m : var_name) : expr :=
(e at_offset{u8, PtrOp, IntOp size_t} Val (default [MPoison] (val_of_int (Z.of_nat (offset_of s.(sl_members) m)) size_t)))%E.
(e at_offset{u8, PtrOp, IntOp size_t} Val (default [MPoison] (offset_of s.(sl_members) m = (λ m, val_of_int (Z.of_nat m) size_t))))%E.
Notation "e 'at{' s } m" := (GetMember e%E s m) (at level 10, format "e 'at{' s } m") : expr_scope.
Typeclasses Opaque GetMember.
Arguments GetMember : simpl never.
Definition GetMemberLoc (l : loc) (s : struct_layout) (m : var_name) : loc :=
(l + Z.of_nat (offset_of s.(sl_members) m))%E.
(l + Z.of_nat (default 0%nat (offset_of s.(sl_members) m)))%E.
Notation "l 'at{' s '}ₗ' m" := (GetMemberLoc l s m) (at level 10, format "l 'at{' s '}ₗ' m") : stdpp_scope.
Typeclasses Opaque GetMemberLoc.
Arguments GetMemberLoc : simpl never.
Definition OffsetOf (s : struct_layout) (m : var_name) : expr :=
(default StuckE (Val <$> (offset_of s.(sl_members) m) = (λ m, val_of_int (Z.of_nat m) size_t)))%E.
Typeclasses Opaque OffsetOf.
Arguments OffsetOf : simpl never.
Record union_layout := {
ul_members : list (var_name * layout);
ul_nodup : NoDup ul_members.*1;
......@@ -347,6 +368,10 @@ Notation "l 'at_union{' ul '}ₗ' m" := (GetMemberUnionLoc l ul m) (at level 10,
Typeclasses Opaque GetMemberUnionLoc.
Arguments GetMemberUnionLoc : simpl never.
Definition OffsetOfUnion (ul : union_layout) (m : var_name) : expr := (i2v 0 size_t).
Typeclasses Opaque OffsetOfUnion.
Arguments OffsetOfUnion : simpl never.
Definition mk_array_layout := ly_mult.
Typeclasses Opaque mk_array_layout.
......
......@@ -22,6 +22,8 @@ Inductive expr :=
| AddrOf (e : expr)
| GetMember (e : expr) (s : struct_layout) (m : var_name)
| GetMemberUnion (e : expr) (ul : union_layout) (m : var_name)
| OffsetOf (s : struct_layout) (m : var_name)
| OffsetOfUnion (ul : union_layout) (m : var_name)
| AnnotExpr (n : nat) {A} (a : A) (e : expr)
| LocInfoE (a : location_info) (e : expr)
| StructInit (ly : struct_layout) (fs : list (string * expr))
......@@ -46,6 +48,8 @@ Lemma expr_ind (P : expr → Prop) :
( (e : expr), P e P (AddrOf e))
( (e : expr) (s : struct_layout) (m : var_name), P e P (GetMember e s m))
( (e : expr) (ul : union_layout) (m : var_name), P e P (GetMemberUnion e ul m))
( (s : struct_layout) (m : var_name), P (OffsetOf s m))
( (ul : union_layout) (m : var_name), P (OffsetOfUnion ul m))
( (n : nat) (A : Type) (a : A) (e : expr), P e P (AnnotExpr n a e))
( (a : location_info) (e : expr), P e P (LocInfoE a e))
( (ly : struct_layout) (fs : list (string * expr)), Forall P fs.*2 P (StructInit ly fs))
......@@ -53,14 +57,14 @@ Lemma expr_ind (P : expr → Prop) :
( (e : lang.expr), P (Expr e)) (e : expr), P e.
Proof.
move => *. generalize dependent P => P. match goal with | e : expr |- _ => revert e end.
fix FIX 1. move => [ ^e] => ??????? Hconcat ???????? Hstruct Hmacro ?.
fix FIX 1. move => [ ^e] => ??????? Hconcat ?????????? Hstruct Hmacro ?.
8: {
apply Hconcat. apply Forall_true => ?. by apply: FIX.
}
16: {
18: {
apply Hstruct. apply Forall_fmap. apply Forall_true => ?. by apply: FIX.
}
16: {
18: {
apply Hmacro. apply Forall_true => ?. by apply: FIX.
}
all: auto.
......@@ -85,6 +89,8 @@ Fixpoint to_expr (e : expr) : lang.expr :=
| StructInit ly fs => notation.StructInit ly (prod_map id to_expr <$> fs)
| GetMember e s m => notation.GetMember (to_expr e) s m
| GetMemberUnion e ul m => notation.GetMemberUnion (to_expr e) ul m
| OffsetOf s m => notation.OffsetOf s m
| OffsetOfUnion ul m => notation.OffsetOfUnion ul m
| MacroE m es _ => notation.MacroE m (to_expr <$> es)
| Expr e => e
end.
......@@ -112,6 +118,8 @@ Ltac of_expr e :=
let e := of_expr e in constr:(GetMember e s m)
| notation.GetMemberUnion ?e ?ul ?m =>
let e := of_expr e in constr:(GetMemberUnion e ul m)
| notation.OffsetOf ?s ?m => constr:(OffsetOf s m)
| notation.OffsetOfUnion ?ul ?m => constr:(OffsetOfUnion ul m)
| notation.Use ?o ?ly ?e =>
let e := of_expr e in constr:(Use o ly e)
| lang.Val ?x => constr:(Val x)
......@@ -208,8 +216,7 @@ Fixpoint find_expr_fill (e : expr) (bind_val : bool) : option (list ectx_item *
else if find_expr_fill e3 bind_val is Some (Ks, e') then
if e1 is Val v1 then if e2 is Val v2 then Some (Ks ++ [CASRCtx ot v1 v2], e') else None else None
else Some ([], e)
| Concat _ => None
| MacroE _ _ _ => None
| Concat _ | MacroE _ _ _ | OffsetOf _ _ | OffsetOfUnion _ _ => None
| SkipE e1 =>
if find_expr_fill e1 bind_val is Some (Ks, e') then
Some (Ks ++ [SkipECtx], e') else Some ([], e)
......@@ -471,6 +478,8 @@ Fixpoint subst (x : var_name) (v : val) (e : expr) : expr :=
| StructInit ly fs => StructInit ly (prod_map id (subst x v) <$> fs)
| GetMember e s m => GetMember (subst x v e) s m
| GetMemberUnion e ul m => GetMemberUnion (subst x v e) ul m
| OffsetOf s m => OffsetOf s m
| OffsetOfUnion ul m => OffsetOfUnion ul m
| MacroE m es wf => MacroE m (subst x v <$> es) wf
| Expr e => Expr (lang.subst x v e)
end.
......@@ -492,6 +501,9 @@ Proof.
match goal with
| _ : ?e1 = ?e2 |- _ => assert (e1 = e2) as -> by assumption
end; done.
- rewrite /notation.OffsetOf/=.
match goal with | |- context [offset_of ?s ?m] => destruct (offset_of s m) end => //=.
by match goal with | |- context [val_of_int ?o ?it] => destruct (val_of_int o it) end.
- (** AnnotExpr *)
match goal with
| |- notation.AnnotExpr ?n _ _ = _ => generalize dependent n
......
......@@ -2,7 +2,7 @@ From iris.proofmode Require Import coq_tactics reduction.
From refinedc.typing Require Export type.
From refinedc.lithium Require Export tactics.
From refinedc.typing.automation Require Export normalize solvers simplification proof_state.
From refinedc.typing Require Import programs function singleton own struct uninit.
From refinedc.typing Require Import programs function singleton own struct uninit int.
Set Default Proof Using "Type".
(** * Registering extensions *)
......@@ -180,6 +180,7 @@ Ltac liRExpr :=
| W.BinOp _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_bin_op _ _ _ _ _ _) _)
| W.UnOp _ _ _ => notypeclasses refine (tac_fast_apply (type_un_op _ _ _ _) _)
| W.CAS _ _ _ _ => notypeclasses refine (tac_fast_apply (type_cas _ _ _ _ _) _)
| W.OffsetOf _ _ => notypeclasses refine (tac_fast_apply (type_offset_of _ _ _) _)
| W.AnnotExpr _ ?a _ => notypeclasses refine (tac_fast_apply (type_annot_expr _ _ _ _) _)
| W.StructInit _ _ => notypeclasses refine (tac_fast_apply (type_struct_init _ _ _) _)
| W.SkipE _ => notypeclasses refine (tac_fast_apply (type_skipe' _ _) _)
......
......@@ -387,6 +387,53 @@ Section programs.