Commit 08d9915b authored by Michael Sammler's avatar Michael Sammler

add macros

parent e8e7d660
......@@ -37,3 +37,4 @@
-Q _build/default/examples/proofs/paper_example_2_1 refinedc.examples.paper_example_2_1
-Q _build/default/examples/proofs/paper_example_2_2 refinedc.examples.paper_example_2_2
-Q _build/default/examples/proofs/buddy_alloc refinedc.examples.buddy_alloc
-Q _build/default/examples/proofs/wrapping_add refinedc.examples.wrapping_add
; Generated by [refinedc], do not edit.
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.wrapping_add)
(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.
From refinedc.examples.wrapping_add Require Import wrapping_def.
Set Default Proof Using "Type".
(* Generated from [examples/wrapping_add.c]. *)
Section code.
Definition file_0 : string := "examples/wrapping_add.c".
Definition loc_2 : location_info := LocationInfo file_0 16 2 16 144.
Definition loc_3 : location_info := LocationInfo file_0 16 9 16 143.
Definition loc_4 : location_info := LocationInfo file_0 16 95 16 102.
Definition loc_5 : location_info := LocationInfo file_0 16 96 16 97.
Definition loc_6 : location_info := LocationInfo file_0 16 96 16 97.
Definition loc_7 : location_info := LocationInfo file_0 16 100 16 101.
Definition loc_8 : location_info := LocationInfo file_0 16 100 16 101.
Definition loc_9 : location_info := LocationInfo file_0 16 84 16 85.
Definition loc_10 : location_info := LocationInfo file_0 16 84 16 85.
Definition loc_11 : location_info := LocationInfo file_0 16 125 16 142.
Definition loc_12 : location_info := LocationInfo file_0 16 126 16 129.
Definition loc_13 : location_info := LocationInfo file_0 16 126 16 129.
Definition loc_14 : location_info := LocationInfo file_0 16 132 16 141.
Definition loc_15 : location_info := LocationInfo file_0 16 134 16 135.
Definition loc_16 : location_info := LocationInfo file_0 16 134 16 135.
Definition loc_17 : location_info := LocationInfo file_0 16 138 16 139.
Definition loc_18 : location_info := LocationInfo file_0 16 138 16 139.
(* Definition of function [wrapping_add]. *)
Definition impl_wrapping_add : function := {|
f_args := [
("a", it_layout size_t);
("b", it_layout size_t);
("c", it_layout size_t)
];
f_local_vars := [
];
f_init := "#0";
f_code := (
<[ "#0" :=
locinfo: loc_2 ;
Return (LocInfoE loc_3 (CheckedMacroE (WrappingAdd size_t size_t) [
(LocInfoE loc_9 (use{it_layout size_t} (LocInfoE loc_10 ("a"))) : expr) ;
(LocInfoE loc_4 ((LocInfoE loc_5 (use{it_layout size_t} (LocInfoE loc_6 ("b")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_7 (use{it_layout size_t} (LocInfoE loc_8 ("c"))))) : expr)
] (LocInfoE loc_11 ((LocInfoE loc_12 (use{it_layout size_t} (LocInfoE loc_13 ("a")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_14 ((LocInfoE loc_15 (use{it_layout size_t} (LocInfoE loc_16 ("b")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_17 (use{it_layout size_t} (LocInfoE loc_18 ("c"))))))) : expr)))
]> $
)%E
|}.
End code.
From refinedc.typing Require Import typing.
From refinedc.examples.wrapping_add Require Import generated_code.
From refinedc.examples.wrapping_add Require Import generated_spec.
From refinedc.examples.wrapping_add Require Import wrapping_rules.
Set Default Proof Using "Type".
(* Generated from [examples/wrapping_add.c]. *)
Section proof_wrapping_add.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [wrapping_add]. *)
Lemma type_wrapping_add :
typed_function impl_wrapping_add type_of_wrapping_add.
Proof.
start_function "wrapping_add" ([[a b] c]) => arg_a arg_b arg_c.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "wrapping_add" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: print_sidecondition_goal "wrapping_add".
Qed.
End proof_wrapping_add.
From refinedc.typing Require Import typing.
From refinedc.examples.wrapping_add Require Import generated_code.
From refinedc.examples.wrapping_add Require Import wrapping_rules.
Set Default Proof Using "Type".
(* Generated from [examples/wrapping_add.c]. *)
Section spec.
Context `{!typeG Σ} `{!globalG Σ}.
(* Type definitions. *)
(* Specifications for function [wrapping_add]. *)
Definition type_of_wrapping_add :=
fn( (a, b, c) : Z * Z * Z; (a @ (int (size_t))), (b @ (int (size_t))), (c @ (int (size_t))); (b + c < int_modulus size_t))
() : (), ((((a + (b + c)) `mod` int_modulus size_t)) @ (int (size_t))); True.
End spec.
generated_proof_wrapping_add.v
From refinedc.lang Require Import notation tactics.
Set Default Proof Using "Type".
Definition WrappingAdd (it1 it2 : int_type) (es : list expr) : expr :=
match es with
| [e1 ; e2] => e1 +{IntOp it1, IntOp it2} e2
| _ => Val VOID
end%E.
Program Instance WrappingAdd_wf it1 it2 : MacroWfSubst (WrappingAdd it1 it2).
Next Obligation. move => ???? [|?[|?[|??]]]//. Qed.
Typeclasses Opaque WrappingAdd.
From refinedc.typing Require Import typing.
From refinedc.examples.wrapping_add Require Export wrapping_def.
Set Default Proof Using "Type".
Section type.
Context `{!typeG Σ}.
Lemma macro_wrapping_add it1 it2 e1 e2 T:
typed_val_expr e1 (λ v1 ty1, typed_val_expr e2 (λ v2 ty2,
n1 n2, subsume (v1 ◁ᵥ ty1) (v1 ◁ᵥ n1 @ int it1) (
subsume (v2 ◁ᵥ ty2) (v2 ◁ᵥ n2 @ int it2) (
(n1 it1 - n2 it2 - it1 = it2 it_signed it1 = false (
v, T v (t2mt (((n1 + n2) `mod` int_modulus it1) @ int it1)))))))) -
typed_macro_expr (WrappingAdd it1 it2) [e1 ; e2] T.
Proof.
iIntros "HT". rewrite /typed_macro_expr/WrappingAdd. iApply type_bin_op.
iIntros (Φ) "HΦ". iApply "HT". iIntros (v1 ty1) "Hty1 HT". iApply ("HΦ" with "Hty1"). clear.
iIntros (Φ) "HΦ". iApply "HT". iIntros (v2 ty2) "Hty2 HT". iApply ("HΦ" with "Hty2"). clear.
iIntros "Hty1 Hty2". iDestruct "HT" as (n1 n2) "HT".
iDestruct ("HT" with "Hty1") as (Hv1) "HT".
iDestruct ("HT" with "Hty2") as (Hv2) "HT".
iIntros (Φ) "HΦ".
iDestruct ("HT" with "[] []" ) as (??) "HT".
1-2: iPureIntro; by apply: val_of_int_in_range.
have /val_of_int_is_some[v Hv] : ((n1 + n2) `mod` int_modulus it1) it1 by apply int_modulus_mod_in_range.
move: Hv1 Hv2 => /val_to_of_int Hv1 /val_to_of_int Hv2. subst it2.
iApply (wp_binop_det v). iSplit.
- iIntros (σ v') "_ !%". split.
+ inversion 1; simplify_eq/=.
by destruct it1 as [? []]; simplify_eq/=.
+ move => ->. econstructor => //.
by destruct it1 as [? []]; simplify_eq/=.
- iIntros "!>". iApply "HΦ"; last done. by iPureIntro.
Qed.
Global Instance macro_wrapping_add_inst it1 it2 e1 e2 :
TypedMacroExpr (WrappingAdd it1 it2) [e1 ; e2] :=
λ T, i2p (macro_wrapping_add it1 it2 e1 e2 T).
End type.
#include <stddef.h>
#include <refinedc.h>
#define WRAPPING_ADD(it1, it2, a, b) RC_MACRO(WrappingAdd, (a) + (b), \
RC_MACRO_ARG(it1), RC_MACRO_ARG(it2), RC_MACRO_EXPR(a), RC_MACRO_EXPR(b))
//@rc::import wrapping_def from refinedc.examples.wrapping_add (for code only)
//@rc::import wrapping_rules from refinedc.examples.wrapping_add
[[rc::parameters("a : Z", "b : Z", "c : Z")]]
[[rc::args("a @ int<size_t>", "b @ int<size_t>", "c @ int<size_t>")]]
[[rc::requires("{(b + c < int_modulus size_t)}")]]
/* We don't want to add the following: [[rc::requires("{(a + b < int_modulus size_t)}")]] */
[[rc::returns("{((a + (b + c)) `mod` int_modulus size_t)} @ int<size_t>")]]
size_t wrapping_add(size_t a, size_t b, size_t c) {
return WRAPPING_ADD(size_t, size_t, a, (b + c));
}
......@@ -179,6 +179,27 @@ let is_const_0 (AilSyntax.AnnotatedExpression(_, _, _, e)) =
end
| _ -> false
type 'a macro_annot_arg =
| MacroString of string
| MacroExpr of ail_expr
let rec macro_annot_to_list e =
let open AilSyntax in
let get_expr e =
match e with
| AnnotatedExpression(_, _, _, AilEarray_decay(AnnotatedExpression(_, _, _, AilEstr(_, strs)))) -> MacroString(String.concat "" strs)
| _ -> MacroExpr(e)
in
match e with
| AnnotatedExpression(_, _, _, AilEbinary(e1, Comma, e2)) -> List.append (macro_annot_to_list e1) [get_expr e2]
| _ -> [get_expr e]
let is_macro_annot e =
match macro_annot_to_list e with
| MacroString("rc_macro") :: _ -> true
| _ -> false
let rec op_type_of loc Ctype.(Ctype(_, c_ty)) =
match c_ty with
| Void -> not_impl loc "op_type_of (Void)"
......@@ -457,6 +478,27 @@ let rec translate_expr : bool -> op_type option -> ail_expr -> expr * calls =
(locate (BinOp(op, ty1, ty2, e1, e2)), l1 @ l2)
| AilEassign(e1,e2) -> forbidden loc "nested assignment"
| AilEcompoundAssign(e1,op,e2) -> not_impl loc "expr compound assign"
| AilEcond(e1,e2,e3) when is_const_0 e1 && is_macro_annot e2 ->
begin
match macro_annot_to_list e2 with
| _ :: MacroString(name) :: rest ->
let rec process_rest rest =
match rest with
| [_] -> ([], [])
| MacroString("ARG") :: MacroString(s) :: rest ->
let (args, es) = process_rest rest in
(s :: args, es)
| MacroString("EXPR") :: MacroExpr(e) :: rest ->
let (args, es) = process_rest rest in
let (e, l) = translate e in
(args, e :: es)
| _ -> not_impl loc "wrong macro args"
in
let (args, es) = process_rest rest in
let (e3, l) = translate e3 in
(locate(Macro(name, args, es, e3)), l)
| _ -> not_impl loc "wrong macro"
end
| AilEcond(e1,e2,e3) -> not_impl loc "expr cond"
| AilEcast(q,c_ty,e) ->
begin
......
......@@ -52,6 +52,7 @@ and expr_aux =
| GetMember of expr * 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
type stmt = stmt_aux Location.located
and stmt_aux =
......
......@@ -189,6 +189,14 @@ let rec pp_expr : Coq_ast.expr pp = fun ff e ->
in
List.iteri fn fs;
pp "@]@;]@]"
| Macro(name, args, es, e) ->
pp "@[@[<hov 2>CheckedMacroE (%s %s) [" name (String.concat " " args);
let fn i e =
let s = if i = List.length es - 1 then "" else " ;" in
pp "@;(%a : expr)%s" pp_expr e s
in
List.iteri fn es;
pp "@]@;] (%a : expr)@]" pp_expr e
in
match Location.get e.loc with
| Some(d) when !print_expr_locs ->
......
......@@ -35,4 +35,8 @@
#define RC_FOCUS_X
#endif
#define RC_MACRO_ARG(arg) "ARG", #arg
#define RC_MACRO_EXPR(expr) "EXPR", expr
#define RC_MACRO(name, m, ...) (0 ? ("rc_macro", #name, __VA_ARGS__, (m)) : (m))
#endif
......@@ -180,6 +180,18 @@ Section IntType.
Global Instance int_elem_of_it : ElemOf Z int_type :=
λ z it, min_int it z max_int it.
Lemma int_modulus_mod_in_range n it:
it_signed it = false
(n `mod` int_modulus it) it.
Proof.
move => ?.
have [|??]:= Z.mod_pos_bound n (int_modulus it). {
apply: Z.pow_pos_nonneg => //. rewrite /bits_per_int/bits_per_byte/=. lia.
}
destruct it as [? []] => //.
split; unfold min_int, max_int => /=; lia.
Qed.
Definition it_layout (it : int_type) :=
Layout (bytes_per_int it) it.(it_byte_size_log).
......
......@@ -97,6 +97,33 @@ Notation "'locinfo:' a ; b" := (LocInfo (B:=stmt) a b%E)
(at level 80, b at level 200, format "'locinfo:' a ; b") : expr_scope.
Notation LocInfoE := (LocInfo (B:=expr)).
Definition MacroE (m : list expr expr) (es : list expr) := m es.
Arguments MacroE : simpl never.
Typeclasses Opaque MacroE.
(* One could probably get rid of this type class by swallowing the
substitutions in MacroE, i.e. make it parametrized by a list of names
and a list of expressions which are substituted in m. (Then one can
maybe also get rid of es?) *)
Class MacroWfSubst (m : list expr expr) : Prop :=
macro_wf_subst x v es: subst x v (m es) = m (subst x v <$> es)
.
(* Like [MacroE m es] but checks that [m es] is equal to [e] *)
Notation CheckedMacroE m es e := (ltac:(
let rec get_head e := match e with
| ?f ?a => get_head f
| ?x => x
end in
let mhead := get_head constr:(m%function) in
let munf := (eval unfold mhead in (m%function)) in
let esunf := (eval unfold LocInfo in (es%list)) in
let eunf := (eval unfold LocInfo in e) in
(* idtac munf; *)
unify (munf esunf) eunf with typeclass_instances;
exact (MacroE m es))) (only parsing).
Lemma annot_expr_S {A} n (a : A) e:
AnnotExpr (S n) a e = SkipE (AnnotExpr n a e).
Proof. done. Qed.
......
......@@ -25,6 +25,7 @@ Inductive expr :=
| AnnotExpr (n : nat) {A} (a : A) (e : expr)
| LocInfoE (a : location_info) (e : expr)
| StructInit (ly : struct_layout) (fs : list (string * expr))
| MacroE (m : list lang.expr lang.expr) (es : list expr) (wf : MacroWfSubst m)
(* for opaque expressions*)
| Expr (e : lang.expr)
.
......@@ -47,17 +48,21 @@ Lemma expr_ind (P : expr → Prop) :
( (e : expr) (ul : union_layout) (m : var_name), P e P (GetMemberUnion e 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 (λ se, P se) fs.*2 P (StructInit ly fs))
( (ly : struct_layout) (fs : list (string * expr)), Forall P fs.*2 P (StructInit ly fs))
( (m : list lang.expr lang.expr) (es : list expr) (wf : MacroWfSubst m), Forall P es P (MacroE m es wf))
( (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 *.
fix FIX 1. move => [ ^e] => ??????? Hconcat ???????? Hstruct Hmacro ?.
8: {
apply Hconcat. apply Forall_true => ?. by apply: FIX.
}
16: {
apply Hstruct. apply Forall_fmap. apply Forall_true => ?. by apply: FIX.
}
16: {
apply Hmacro. apply Forall_true => ?. by apply: FIX.
}
all: auto.
Qed.
......@@ -80,6 +85,7 @@ 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
| MacroE m es _ => notation.MacroE m (to_expr <$> es)
| Expr e => e
end.
......@@ -96,6 +102,8 @@ Ltac of_expr e :=
let e := of_expr e in constr:(AddrOf e)
| notation.AnnotExpr ?n ?a ?e =>
let e := of_expr e in constr:(AnnotExpr n a e)
| notation.MacroE ?m ?es =>
let es := of_expr es in constr:(MacroE m es _)
| notation.LocInfo ?a ?e =>
let e := of_expr e in constr:(LocInfoE a e)
| notation.StructInit ?ly ?fs =>
......@@ -201,6 +209,7 @@ Fixpoint find_expr_fill (e : expr) (bind_val : bool) : option (list ectx_item *
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
| SkipE e1 =>
if find_expr_fill e1 bind_val is Some (Ks, e') then
Some (Ks ++ [SkipECtx], e') else Some ([], e)
......@@ -462,6 +471,7 @@ 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
| MacroE m es wf => MacroE m (subst x v <$> es) wf
| Expr e => Expr (lang.subst x v e)
end.
......@@ -498,6 +508,9 @@ Proof.
rewrite !list_to_map_fmap !lookup_fmap. destruct (list_to_map fs !! f) as [e|] eqn:H; simpl; last done.
f_equal. move: Hf => /Forall_forall IH. apply (IH _).
simplify_eq. apply elem_of_list_to_map_2 in H. set_solver.
- (** MacroE *)
rewrite /notation.MacroE macro_wf_subst. f_equal.
rewrite -!list_fmap_compose. apply list_fmap_ext' => //. by apply Forall_forall.
Qed.
Lemma to_expr_subst_l xs vs e :
......
......@@ -51,6 +51,7 @@ Ltac convert_to_i2p_tac P ::=
| typed_cas ?ot ?v1 ?P1 ?v2 ?P2 ?v3 ?P3 ?T => uconstr:(((_ : TypedCas _ _ _ _ _ _ _) _).(i2p_proof))
| typed_annot_expr ?n ?a ?v ?ty ?T => uconstr:(((_ : TypedAnnotExpr _ _ _ _) _) .(i2p_proof))
| typed_annot_stmt ?a ?l ?β ?ty ?T => uconstr:(((_ : TypedAnnotStmt _ _ _ _) _).(i2p_proof))
| typed_macro_expr ?m ?es ?T => uconstr:(((_ : TypedMacroExpr _ _) _).(i2p_proof))
end.
(** * Main automation tactics *)
......@@ -182,6 +183,7 @@ Ltac liRExpr :=
| 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' _ _) _)
| W.MacroE _ _ _ => notypeclasses refine (tac_fast_apply (type_macro_expr _ _ _) _)
| _ => fail "do_expr: unknown expr" e
end
end.
......
......@@ -127,6 +127,14 @@ Section judgements.
Class TypedCas (ot : op_type) (v1 : val) (P1 : iProp Σ) (v2 : val) (P2 : iProp Σ) (v3 : val) (P3 : iProp Σ) : Type :=
typed_cas_proof T : iProp_to_Prop (typed_cas ot v1 P1 v2 P2 v3 P3 T).
(* This does not allow overloading the macro based on the type of
es. Is this a problem? There is a work around where the rule inserts
another judgment that allows type-based overloading. *)
Definition typed_macro_expr (m : list expr expr) (es : list expr) (T : val mtype iProp Σ) : iProp Σ :=
(typed_val_expr (m es) T).
Class TypedMacroExpr (m : list expr expr) (es : list expr) : Type :=
typed_macro_expr_proof T : iProp_to_Prop (typed_macro_expr m es T).
(*** places *)
Definition typed_write (atomic : bool) (e : expr) (v : val) (ty : type) `{!Movable ty} (T : iProp Σ) : iProp Σ :=
let E := if atomic then else in
......@@ -305,8 +313,10 @@ Hint Mode TypedAddrOfEnd + + + + + : typeclass_instances.
Hint Mode TypedPlace + + + + + + : typeclass_instances.
Hint Mode TypedAnnotExpr + + + + + + + : typeclass_instances.
Hint Mode TypedAnnotStmt + + + + + + + : typeclass_instances.
Hint Mode TypedMacroExpr + + + + : typeclass_instances.
Arguments typed_annot_expr : simpl never.
Arguments typed_annot_stmt : simpl never.
Arguments typed_macro_expr : simpl never.
Arguments learnalign_align {_ _ _ _} _.
Arguments learnalign_learn {_ _ _ _} _.
......@@ -814,6 +824,11 @@ Section typing.
by iApply ("IH" with "HΦ HT").
Qed.
Lemma type_macro_expr m es T:
typed_macro_expr m es T -
typed_val_expr (MacroE m es) T.
Proof. done. Qed.
Lemma type_use ly T e o:
if o is Na2Ord then False else True typed_read (if o is ScOrd then true else false) e ly T -
typed_val_expr (use{ly, o} e) T.
......
Markdown is supported
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