Skip to content

GitLab

Commit 971ef3f2 authored by Lennard Gäher's avatar Lennard Gäher Committed by Michael Sammler
Browse files

parameterise operators with boolean result by the result integer type

parent 72833963
Pipeline #51183 passed with stage
in 16 minutes and 42 seconds
Show whitespace changes
Inline Side-by-side
frontend/coq_pp.ml
View file @ 971ef3f2
......@@ -130,6 +130,12 @@ let pp_bin_op : Coq_ast.bin_op pp = fun ff op ->
| LazyAndOp -> "&&"
| LazyOrOp -> "||"
let is_bool_result_op = fun op ->
match op with
| EqOp | NeOp | LtOp | GtOp | LeOp | GeOp -> true
| LazyAndOp | LazyOrOp -> true
| _ -> false
let rec pp_expr : Coq_ast.expr pp = fun ff e ->
let pp fmt = Format.fprintf ff fmt in
let pp_expr_body ff e =
......@@ -170,6 +176,9 @@ let rec pp_expr : Coq_ast.expr pp = fun ff e ->
| (OpInt(_), OpPtr(_), _ ) ->
panic_no_pos "Wrong ordering of integer pointer binop [%a]."
pp_bin_op op
| _ when is_bool_result_op op ->
pp "(%a) %a{%a, %a, i32} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
| _ ->
pp "(%a) %a{%a, %a} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
......
theories/lang/lang.v
View file @ 971ef3f2
......@@ -12,7 +12,8 @@ Definition label := string.
(* see http://compcert.inria.fr/doc/html/compcert.cfrontend.Cop.html#binary_operation *)
Inductive bin_op : Set :=
| AddOp | SubOp | MulOp | DivOp | ModOp | AndOp | OrOp | XorOp | ShlOp
| ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp | Comma
| ShrOp | EqOp (rit : int_type) | NeOp (rit : int_type) | LtOp (rit : int_type)
| GtOp (rit : int_type) | LeOp (rit : int_type) | GeOp (rit : int_type) | Comma
(* Ptr is the second argument and offset the first *)
| PtrOffsetOp (ly : layout) | PtrNegOffsetOp (ly : layout)
| PtrDiffOp (ly : layout).
......@@ -249,41 +250,41 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
valid_ptr l2 σ.(st_heap) →
val_of_Z ((l1.2 - l2.2) `div` ly.(ly_size)) ptrdiff_t None = Some v →
eval_bin_op (PtrDiffOp ly) PtrOp PtrOp σ v1 v2 v
| RelOpPNull v1 v2 σ l v op b p a:
| RelOpPNull v1 v2 σ l v op b p a rit:
val_to_loc v1 = Some l →
l = (ProvAlloc p, a) →
v2 = NULL →
heap_state_loc_in_bounds l 0%nat σ.(st_heap) →
match op with
| EqOp => Some false
| NeOp => Some true
| EqOp rit => Some (false, rit)
| NeOp rit => Some (true, rit)
| _ => None
end = Some b →
val_of_Z (Z_of_bool b) i32 None = Some v →
end = Some (b, rit) →
val_of_Z (Z_of_bool b) rit None = Some v →
eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpNullP v1 v2 σ l v op b p a:
| RelOpNullP v1 v2 σ l v op b p a rit:
v1 = NULL →
val_to_loc v2 = Some l →
l = (ProvAlloc p, a) →
heap_state_loc_in_bounds l 0%nat σ.(st_heap) →
match op with
| EqOp => Some false
| NeOp => Some true
| EqOp rit => Some (false, rit)
| NeOp rit => Some (true, rit)
| _ => None
end = Some b →
val_of_Z (Z_of_bool b) i32 None = Some v →
end = Some (b, rit) →
val_of_Z (Z_of_bool b) rit None = Some v →
eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpNullNull v1 v2 σ v op b:
| RelOpNullNull v1 v2 σ v op b rit:
v1 = NULL →
v2 = NULL →
match op with
| EqOp => Some true
| NeOp => Some false
| EqOp rit => Some (true, rit)
| NeOp rit => Some (false, rit)
| _ => None
end = Some b →
val_of_Z (Z_of_bool b) i32 None = Some v →
end = Some (b, rit) →
val_of_Z (Z_of_bool b) rit None = Some v →
eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpPP v1 v2 σ l1 l2 p1 p2 a1 a2 v b op:
| RelOpPP v1 v2 σ l1 l2 p1 p2 a1 a2 v b op rit:
val_to_loc v1 = Some l1 →
val_to_loc v2 = Some l2 →
(* Note that this is technically redundant due to the valid_ptr,
......@@ -292,43 +293,41 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
l2 = (ProvAlloc p2, a2) →
valid_ptr l1 σ.(st_heap) → valid_ptr l2 σ.(st_heap) →
match op with
| EqOp => Some (bool_decide (a1 = a2))
| NeOp => Some (bool_decide (a1 ≠ a2))
| LtOp => if bool_decide (p1 = p2) then Some (bool_decide (a1 < a2)) else None
| GtOp => if bool_decide (p1 = p2) then Some (bool_decide (a1 > a2)) else None
| LeOp => if bool_decide (p1 = p2) then Some (bool_decide (a1 <= a2)) else None
| GeOp => if bool_decide (p1 = p2) then Some (bool_decide (a1 >= a2)) else None
| EqOp rit => Some (bool_decide (a1 = a2), rit)
| NeOp rit => Some (bool_decide (a1 ≠ a2), rit)
| LtOp rit => if bool_decide (p1 = p2) then Some (bool_decide (a1 < a2), rit) else None
| GtOp rit => if bool_decide (p1 = p2) then Some (bool_decide (a1 > a2), rit) else None
| LeOp rit => if bool_decide (p1 = p2) then Some (bool_decide (a1 <= a2), rit) else None
| GeOp rit => if bool_decide (p1 = p2) then Some (bool_decide (a1 >= a2), rit) else None
| _ => None
end = Some b →
val_of_Z (Z_of_bool b) i32 None = Some v →
end = Some (b, rit) →
val_of_Z (Z_of_bool b) rit None = Some v →
eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpFnPP v1 v2 σ l1 l2 a1 a2 v b op:
| RelOpFnPP v1 v2 σ l1 l2 a1 a2 v b op rit:
val_to_loc v1 = Some l1 →
val_to_loc v2 = Some l2 →
l1 = (ProvFnPtr, a1) →
l2 = (ProvFnPtr, a2) →
match op with
| EqOp => Some (bool_decide (a1 = a2))
| NeOp => Some (bool_decide (a1 ≠ a2))
| EqOp rit => Some (bool_decide (a1 = a2), rit)
| NeOp rit => Some (bool_decide (a1 ≠ a2), rit)
| _ => None
end = Some b →
val_of_Z (Z_of_bool b) i32 None = Some v →
end = Some (b, rit) →
val_of_Z (Z_of_bool b) rit None = Some v →
eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpII op v1 v2 v σ n1 n2 it b:
| RelOpII op v1 v2 v σ n1 n2 it b rit:
match op with
| EqOp => Some (bool_decide (n1 = n2))
| NeOp => Some (bool_decide (n1 ≠ n2))
| LtOp => Some (bool_decide (n1 < n2))
| GtOp => Some (bool_decide (n1 > n2))
| LeOp => Some (bool_decide (n1 <= n2))
| GeOp => Some (bool_decide (n1 >= n2))
| EqOp rit => Some (bool_decide (n1 = n2), rit)
| NeOp rit => Some (bool_decide (n1 ≠ n2), rit)
| LtOp rit => Some (bool_decide (n1 < n2), rit)
| GtOp rit => Some (bool_decide (n1 > n2), rit)
| LeOp rit => Some (bool_decide (n1 <= n2), rit)
| GeOp rit => Some (bool_decide (n1 >= n2), rit)
| _ => None
end = Some b →
end = Some (b, rit) →
val_to_Z v1 it = Some n1 →
val_to_Z v2 it = Some n2 →
(* TODO: What is the right int type of the result here? C seems to
use i32 but maybe we don't want to hard code that. *)
val_of_Z (Z_of_bool b) i32 None = Some v →
val_of_Z (Z_of_bool b) rit None = Some v →
eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
| ArithOpII op v1 v2 σ n1 n2 it n v:
match op with
......
theories/lang/lifting.v
View file @ 971ef3f2
......@@ -461,19 +461,19 @@ Proof.
by iApply wp_value.
Qed.
Lemma wp_ptr_relop Φ op v1 v2 v l1 l2 b:
Lemma wp_ptr_relop Φ op v1 v2 v l1 l2 b rit:
val_to_loc v1 = Some l1 →
val_to_loc v2 = Some l2 →
val_of_Z (Z_of_bool b) i32 None = Some v →
val_of_Z (Z_of_bool b) rit None = Some v →
match op with
| EqOp => Some (bool_decide (l1.2 = l2.2))
| NeOp => Some (bool_decide (l1.2 ≠ l2.2))
| LtOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 < l2.2)) else None
| GtOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 > l2.2)) else None
| LeOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 <= l2.2)) else None
| GeOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 >= l2.2)) else None
| EqOp rit => Some (bool_decide (l1.2 = l2.2), rit)
| NeOp rit => Some (bool_decide (l1.2 ≠ l2.2), rit)
| LtOp rit => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 < l2.2), rit) else None
| GtOp rit => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 > l2.2), rit) else None
| LeOp rit => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 <= l2.2), rit) else None
| GeOp rit => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 >= l2.2), rit) else None
| _ => None
end = Some b →
end = Some (b, rit) →
loc_in_bounds l1 0 -∗ loc_in_bounds l2 0 -∗
(alloc_alive_loc l1 ∧ alloc_alive_loc l2 ∧ ▷ Φ v) -∗
WP BinOp op PtrOp PtrOp (Val v1) (Val v2) {{ Φ }}.
......
theories/lang/notation.v
View file @ 971ef3f2
......@@ -18,18 +18,18 @@ Notation "e1 '+' '{' ot1 , ot2 } e2" := (BinOp AddOp ot1 ot2 e1%E e2%E)
(* This conflicts with rewrite -{2}(app_nil_r vs). *)
Notation "e1 '-' '{' ot1 , ot2 } e2" := (BinOp SubOp ot1 ot2 e1%E e2%E)
(at level 50, left associativity, format "e1 '-' '{' ot1 , ot2 } e2") : expr_scope.
Notation "e1 '=' '{' ot1 , ot2 } e2" := (BinOp EqOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 '=' '{' ot1 , ot2 } e2") : expr_scope.
Notation "e1 '!=' '{' ot1 , ot2 } e2" := (BinOp NeOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 '!=' '{' ot1 , ot2 } e2") : expr_scope.
Notation "e1 ≤{ ot1 , ot2 } e2" := (BinOp LeOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 ≤{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 <{ ot1 , ot2 } e2" := (BinOp LtOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 <{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 ≥{ ot1 , ot2 } e2" := (BinOp GeOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 ≥{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 >{ ot1 , ot2 } e2" := (BinOp GtOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 >{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 '=' '{' ot1 , ot2 , rit } e2" := (BinOp (EqOp rit) ot1 ot2 e1%E e2%E)
(at level 70, format "e1 '=' '{' ot1 , ot2 , rit } e2") : expr_scope.
Notation "e1 '!=' '{' ot1 , ot2 , rit } e2" := (BinOp (NeOp rit) ot1 ot2 e1%E e2%E)
(at level 70, format "e1 '!=' '{' ot1 , ot2 , rit } e2") : expr_scope.
Notation "e1 ≤{ ot1 , ot2 , rit } e2" := (BinOp (LeOp rit) ot1 ot2 e1%E e2%E)
(at level 70, format "e1 ≤{ ot1 , ot2 , rit } e2") : expr_scope.
Notation "e1 <{ ot1 , ot2 , rit } e2" := (BinOp (LtOp rit) ot1 ot2 e1%E e2%E)
(at level 70, format "e1 <{ ot1 , ot2 , rit } e2") : expr_scope.
Notation "e1 ≥{ ot1 , ot2 , rit } e2" := (BinOp (GeOp rit) ot1 ot2 e1%E e2%E)
(at level 70, format "e1 ≥{ ot1 , ot2 , rit } e2") : expr_scope.
Notation "e1 >{ ot1 , ot2 , rit } e2" := (BinOp (GtOp rit) ot1 ot2 e1%E e2%E)
(at level 70, format "e1 >{ ot1 , ot2 , rit } e2") : expr_scope.
Notation "e1 ×{ ot1 , ot2 } e2" := (BinOp MulOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 ×{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 /{ ot1 , ot2 } e2" := (BinOp DivOp ot1 ot2 e1%E e2%E)
......@@ -65,17 +65,17 @@ Notation "'if{' ot '}' ':' e1 'then' s1 'else' s2" := (IfS ot e1%E s1%E s2%E)
Notation "'expr:' e ; s" := (ExprS e%E s%E)
(at level 80, s at level 200, format "'[v' 'expr:' e ';' '/' s ']'") : expr_scope.
Definition LogicalAnd (ot1 ot2 : op_type) (e1 e2 : expr) : expr :=
(IfE ot1 e1 (IfE ot2 e2 (i2v 1 i32) (i2v 0 i32)) (i2v 0 i32)).
Notation "e1 &&{ ot1 , ot2 } e2" := (LogicalAnd ot1 ot2 e1 e2)
(at level 70, format "e1 &&{ ot1 , ot2 } e2") : expr_scope.
Definition LogicalAnd (ot1 ot2 : op_type) rit (e1 e2 : expr) : expr :=
(IfE ot1 e1 (IfE ot2 e2 (i2v 1 rit) (i2v 0 rit)) (i2v 0 rit)).
Notation "e1 &&{ ot1 , ot2 , rit } e2" := (LogicalAnd ot1 ot2 rit e1 e2)
(at level 70, format "e1 &&{ ot1 , ot2 , rit } e2") : expr_scope.
Arguments LogicalAnd : simpl never.
Typeclasses Opaque LogicalAnd.
Definition LogicalOr (ot1 ot2 : op_type) (e1 e2 : expr) : expr :=
(IfE ot1 e1 (i2v 1 i32) (IfE ot2 e2 (i2v 1 i32) (i2v 0 i32))).
Notation "e1 ||{ ot1 , ot2 } e2" := (LogicalOr ot1 ot2 e1 e2)
(at level 70, format "e1 ||{ ot1 , ot2 } e2") : expr_scope.
Definition LogicalOr (ot1 ot2 : op_type) rit (e1 e2 : expr) : expr :=
(IfE ot1 e1 (i2v 1 rit) (IfE ot2 e2 (i2v 1 rit) (i2v 0 rit))).
Notation "e1 ||{ ot1 , ot2 , rit } e2" := (LogicalOr ot1 ot2 rit e1 e2)
(at level 70, format "e1 ||{ ot1 , ot2 , rit } e2") : expr_scope.
Arguments LogicalOr : simpl never.
Typeclasses Opaque LogicalOr.
......@@ -190,8 +190,8 @@ Arguments OffsetOfUnion : simpl never.
(*** Tests *)
Example test1 (l : loc) ly ot :
(l <-{ly} use{ot}(&l +{PtrOp, IntOp size_t} (l ={PtrOp, PtrOp} l)); ExprS (Call l [ (l : expr); (l : expr)]) (l <-{ly, ScOrd} l; Goto "a"))%E =
(Assign Na1Ord ly l (Use Na1Ord ot (BinOp AddOp PtrOp (IntOp size_t) (AddrOf l) (BinOp EqOp PtrOp PtrOp l l))))
(l <-{ly} use{ot}(&l +{PtrOp, IntOp size_t} (l ={PtrOp, PtrOp, i32} l)); ExprS (Call l [ (l : expr); (l : expr)]) (l <-{ly, ScOrd} l; Goto "a"))%E =
(Assign Na1Ord ly l (Use Na1Ord ot (BinOp AddOp PtrOp (IntOp size_t) (AddrOf l) (BinOp (EqOp i32) PtrOp PtrOp l l))))
(ExprS (Call l [ Val (val_of_loc l); Val (val_of_loc l)]) ((Assign ScOrd ly l l) (Goto "a"))).
Proof. simpl. reflexivity. Abort.
......
theories/lang/tactics.v
View file @ 971ef3f2
......@@ -21,8 +21,8 @@ Inductive expr :=
| SkipE (e : expr)
| StuckE
(* new constructors *)
| LogicalAnd (ot1 ot2 : op_type) (e1 e2 : expr)
| LogicalOr (ot1 ot2 : op_type) (e1 e2 : expr)
| LogicalAnd (ot1 ot2 : op_type) (rit : int_type) (e1 e2 : expr)
| LogicalOr (ot1 ot2 : op_type) (rit : int_type) (e1 e2 : expr)
| Use (o : order) (ot : op_type) (e : expr)
| AddrOf (e : expr)
| LValue (e : expr)
......@@ -53,8 +53,8 @@ Lemma expr_ind (P : expr → Prop) :
(∀ (ot : op_type) (e1 e2 e3 : expr), P e1 → P e2 → P e3 → P (IfE ot e1 e2 e3)) →
(∀ (e : expr), P e → P (SkipE e)) →
(P StuckE) →
(∀ (ot1 ot2 : op_type) (e1 e2 : expr), P e1 → P e2 → P (LogicalAnd ot1 ot2 e1 e2)) →
(∀ (ot1 ot2 : op_type) (e1 e2 : expr), P e1 → P e2 → P (LogicalOr ot1 ot2 e1 e2)) →
(∀ (ot1 ot2 : op_type) (rit : int_type) (e1 e2 : expr), P e1 → P e2 → P (LogicalAnd ot1 ot2 rit e1 e2)) →
(∀ (ot1 ot2 : op_type) (rit : int_type) (e1 e2 : expr), P e1 → P e2 → P (LogicalOr ot1 ot2 rit e1 e2)) →
(∀ (o : order) (ot : op_type) (e : expr), P e → P (Use o ot e)) →
(∀ (e : expr), P e → P (AddrOf e)) →
(∀ (e : expr), P e → P (LValue e)) →
......@@ -100,8 +100,8 @@ Fixpoint to_expr (e : expr) : lang.expr :=
| IfE ot e1 e2 e3 => lang.IfE ot (to_expr e1) (to_expr e2) (to_expr e3)
| SkipE e => lang.SkipE (to_expr e)
| StuckE => lang.StuckE
| LogicalAnd ot1 ot2 e1 e2 => notation.LogicalAnd ot1 ot2 (to_expr e1) (to_expr e2)
| LogicalOr ot1 ot2 e1 e2 => notation.LogicalOr ot1 ot2 (to_expr e1) (to_expr e2)
| LogicalAnd ot1 ot2 rit e1 e2 => notation.LogicalAnd ot1 ot2 rit (to_expr e1) (to_expr e2)
| LogicalOr ot1 ot2 rit e1 e2 => notation.LogicalOr ot1 ot2 rit (to_expr e1) (to_expr e2)
| Use o ot e => notation.Use o ot (to_expr e)
| AddrOf e => notation.AddrOf (to_expr e)
| LValue e => notation.LValue (to_expr e)
......@@ -143,14 +143,14 @@ Ltac of_expr e :=
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.LogicalAnd ?ot1 ?ot2 ?e1 ?e2 =>
| notation.LogicalAnd ?ot1 ?ot2 ?rit ?e1 ?e2 =>
let e1 := of_expr e1 in
let e2 := of_expr e2 in
constr:(LogicalAnd ot1 ot2 e1 e2)
| notation.LogicalOr ?ot1 ?ot2 ?e1 ?e2 =>
constr:(LogicalAnd ot1 ot2 rit e1 e2)
| notation.LogicalOr ?ot1 ?ot2 ?rit ?e1 ?e2 =>
let e1 := of_expr e1 in
let e2 := of_expr e2 in
constr:(LogicalOr ot1 ot2 e1 e2)
constr:(LogicalOr ot1 ot2 rit e1 e2)
| notation.Use ?o ?ot ?e =>
let e := of_expr e in constr:(Use o ot e)
| lang.Val ?x => constr:(Val x)
......@@ -279,7 +279,7 @@ Fixpoint find_expr_fill (e : expr) (bind_val : bool) : option (list ectx_item *
if find_expr_fill f bind_val is Some (Ks, e') then
Some (Ks ++ [CallLCtx args], e') else
(* TODO: handle arguments? *) None
| Concat _ | MacroE _ _ _ | OffsetOf _ _ | OffsetOfUnion _ _ | LogicalAnd _ _ _ _ | LogicalOr _ _ _ _ => None
| Concat _ | MacroE _ _ _ | OffsetOf _ _ | OffsetOfUnion _ _ | LogicalAnd _ _ _ _ _ | LogicalOr _ _ _ _ _ => None
| IfE ot e1 e2 e3 =>
if find_expr_fill e1 bind_val is Some (Ks, e') then
Some (Ks ++ [IfECtx ot e2 e3], e') else Some ([], e)
......@@ -534,8 +534,8 @@ Fixpoint subst_l (xs : list (var_name * val)) (e : expr) : expr :=
| IfE ot e1 e2 e3 => IfE ot (subst_l xs e1) (subst_l xs e2) (subst_l xs e3)
| SkipE e => SkipE (subst_l xs e)
| StuckE => StuckE
| LogicalAnd ot1 ot2 e1 e2 => LogicalAnd ot1 ot2 (subst_l xs e1) (subst_l xs e2)
| LogicalOr ot1 ot2 e1 e2 => LogicalOr ot1 ot2 (subst_l xs e1) (subst_l xs e2)
| LogicalAnd ot1 ot2 rit e1 e2 => LogicalAnd ot1 ot2 rit (subst_l xs e1) (subst_l xs e2)
| LogicalOr ot1 ot2 rit e1 e2 => LogicalOr ot1 ot2 rit (subst_l xs e1) (subst_l xs e2)
| Use o ot e => Use o ot (subst_l xs e)
| AddrOf e => AddrOf (subst_l xs e)
| LValue e => LValue (subst_l xs e)
......
theories/typing/automation.v
View file @ 971ef3f2
......@@ -225,8 +225,8 @@ Ltac liRExpr :=
| W.AnnotExpr _ ?a _ => notypeclasses refine (tac_fast_apply (type_annot_expr _ _ _ _) _)
| W.StructInit _ _ => notypeclasses refine (tac_fast_apply (type_struct_init _ _ _) _)
| W.IfE _ _ _ _ => notypeclasses refine (tac_fast_apply (type_ife _ _ _ _ _) _)
| W.LogicalAnd _ _ _ _ => notypeclasses refine (tac_fast_apply (type_logical_and _ _ _ _ _) _)
| W.LogicalOr _ _ _ _ => notypeclasses refine (tac_fast_apply (type_logical_or _ _ _ _ _) _)
| W.LogicalAnd _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_logical_and _ _ _ _ _) _)
| W.LogicalOr _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_logical_or _ _ _ _ _) _)
| 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
......
theories/typing/int.v
View file @ 971ef3f2
......@@ -134,16 +134,16 @@ Section programs.
(* TODO: instead of adding it_in_range to the context here, have a
SimplifyPlace/Val instance for int which adds it to the context if
it does not yet exist (using check_hyp_not_exists)?! *)
Lemma type_relop_int_int it v1 n1 v2 n2 T b op:
Lemma type_relop_int_int it v1 n1 v2 n2 T b op :
match op with
| EqOp => Some (bool_decide (n1 = n2))
| NeOp => Some (bool_decide (n1 ≠ n2))
| LtOp => Some (bool_decide (n1 < n2))
| GtOp => Some (bool_decide (n1 > n2))
| LeOp => Some (bool_decide (n1 <= n2))
| GeOp => Some (bool_decide (n1 >= n2))
| EqOp rit => Some (bool_decide (n1 = n2), rit)
| NeOp rit => Some (bool_decide (n1 ≠ n2), rit)
| LtOp rit => Some (bool_decide (n1 < n2), rit)
| GtOp rit => Some (bool_decide (n1 > n2), rit)
| LeOp rit => Some (bool_decide (n1 <= n2), rit)
| GeOp rit => Some (bool_decide (n1 >= n2), rit)
| _ => None
end = Some b →
end = Some (b, i32) →
(⌜n1 ∈ it⌝ -∗ ⌜n2 ∈ it⌝ -∗ T (i2v (Z_of_bool b) i32) (t2mt (b @ boolean i32))) -∗
typed_bin_op v1 (v1 ◁ᵥ n1 @ int it) v2 (v2 ◁ᵥ n2 @ int it) op (IntOp it) (IntOp it) T.
Proof.
......@@ -159,22 +159,22 @@ Section programs.
Qed.
Global Program Instance type_eq_int_int_inst it v1 n1 v2 n2:
TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I EqOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 = n2)) _ _).
TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I (EqOp i32) (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 = n2)) _ _).
Next Obligation. done. Qed.
Global Program Instance type_ne_int_int_inst it v1 n1 v2 n2:
TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I NeOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 ≠ n2)) _ _).
TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I (NeOp i32) (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 ≠ n2)) _ _).
Next Obligation. done. Qed.
Global Program Instance type_lt_int_int_inst it v1 n1 v2 n2:
TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I LtOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 < n2)) _ _).
TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I (LtOp i32) (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 < n2)) _ _).
Next Obligation. done. Qed.
Global Program Instance type_gt_int_int_inst it v1 n1 v2 n2:
TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I GtOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 > n2)) _ _).
TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I (GtOp i32) (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 > n2)) _ _).
Next Obligation. done. Qed.
Global Program Instance type_le_int_int_inst it v1 n1 v2 n2:
TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I LeOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 <= n2)) _ _).
TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I (LeOp i32) (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 <= n2)) _ _).
Next Obligation. done. Qed.
Global Program Instance type_ge_int_int_inst it v1 n1 v2 n2:
TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I GeOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 >= n2)) _ _).
TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I (GeOp i32) (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 >= n2)) _ _).
Next Obligation. done. Qed.
Definition arith_op_result (it : int_type) n1 n2 op : option Z :=
......@@ -477,10 +477,10 @@ Section programs.
Lemma type_relop_bool_bool it v1 b1 v2 b2 T b op:
match op with
| EqOp => Some (eqb b1 b2)
| NeOp => Some (negb (eqb b1 b2))
| EqOp rit => Some (eqb b1 b2, rit)
| NeOp rit => Some (negb (eqb b1 b2), rit)
| _ => None
end = Some b →
end = Some (b, i32) →
(T (i2v (Z_of_bool b) i32) (t2mt (b @ boolean i32))) -∗
typed_bin_op v1 (v1 ◁ᵥ b1 @ boolean it) v2 (v2 ◁ᵥ b2 @ boolean it) op (IntOp it) (IntOp it) T.
Proof.
......@@ -495,10 +495,10 @@ Section programs.
Qed.
Global Program Instance type_eq_bool_bool_inst it v1 b1 v2 b2:
TypedBinOpVal v1 (b1 @ (boolean it))%I v2 (b2 @ (boolean it))%I EqOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_bool_bool it v1 b1 v2 b2 T (eqb b1 b2) _ _).
TypedBinOpVal v1 (b1 @ (boolean it))%I v2 (b2 @ (boolean it))%I (EqOp i32) (IntOp it) (IntOp it) := λ T, i2p (type_relop_bool_bool it v1 b1 v2 b2 T (eqb b1 b2) _ _).
Next Obligation. done. Qed.
Global Program Instance type_ne_bool_bool_inst it v1 b1 v2 b2:
TypedBinOpVal v1 (b1 @ (boolean it))%I v2 (b2 @ (boolean it))%I NeOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_bool_bool it v1 b1 v2 b2 T (negb (eqb b1 b2)) _ _).
TypedBinOpVal v1 (b1 @ (boolean it))%I v2 (b2 @ (boolean it))%I (NeOp i32) (IntOp it) (IntOp it) := λ T, i2p (type_relop_bool_bool it v1 b1 v2 b2 T (negb (eqb b1 b2)) _ _).
Next Obligation. done. Qed.
Lemma type_if_bool it (b : bool) v T1 T2 :
......@@ -655,7 +655,7 @@ Section tests.
Example type_eq n1 n3 T:
n1 ∈ size_t →
n3 ∈ size_t →
⊢ typed_val_expr ((i2v n1 size_t +{IntOp size_t, IntOp size_t} i2v 0 size_t) = {IntOp size_t, IntOp size_t} i2v n3 size_t ) T.
⊢ typed_val_expr ((i2v n1 size_t +{IntOp size_t, IntOp size_t} i2v 0 size_t) = {IntOp size_t, IntOp size_t, i32} i2v n3 size_t ) T.
Proof.
move => Hn1 Hn2.
iApply type_bin_op.
......
theories/typing/optional.v
View file @ 971ef3f2
......@@ -10,7 +10,7 @@ Class Optionable `{!typeG Σ} (ty : type) `{!Movable ty} (optty : type) `{!Movab
opt_pre : val → val → iProp Σ;
opt_bin_op (bty beq : bool) v1 v2 σ v :
(⊢ opt_pre v1 v2 -∗ (if bty then v1 ◁ᵥ ty else v1 ◁ᵥ optty) -∗ v2 ◁ᵥ optty -∗ state_ctx σ -∗
⌜eval_bin_op (if beq then EqOp else NeOp) ot1 ot2 σ v1 v2 v ↔ val_of_Z (Z_of_bool (xorb bty beq)) i32 None = Some v⌝);
⌜eval_bin_op (if beq then EqOp i32 else NeOp i32) ot1 ot2 σ v1 v2 v ↔ val_of_Z (Z_of_bool (xorb bty beq)) i32 None = Some v⌝);
}.
Arguments opt_pre {_ _} _ {_ _ _ _ _ _} _ _.
......@@ -164,7 +164,7 @@ Section optional.
opt_pre ty v1 v2 ∧
destruct_hint DHintInfo (DestructHintOptionalEq b) (⌜b⌝ -∗ v1 ◁ᵥ ty -∗ T (i2v (Z_of_bool false) i32) (t2mt (false @ boolean i32))) ∧
destruct_hint DHintInfo (DestructHintOptionalEq (¬ b)) (⌜¬ b⌝ -∗ v1 ◁ᵥ optty -∗ T (i2v (Z_of_bool true) i32) (t2mt (true @ boolean i32))) -∗
typed_bin_op v1 (v1 ◁ᵥ b @ (optional ty optty)) v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 T.
typed_bin_op v1 (v1 ◁ᵥ b @ (optional ty optty)) v2 (v2 ◁ᵥ optty) (EqOp i32) ot1 ot2 T.
Proof.
unfold destruct_hint. iIntros "HT Hv1 Hv2" (Φ) "HΦ".
iDestruct "Hv1" as "[[% Hv1]|[% Hv1]]".
......@@ -194,13 +194,13 @@ Section optional.
by iApply ("HΦ" with "[] HT").
Qed.
Global Instance type_eq_optional_refined_inst v1 v2 ty optty `{!Movable ty} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2} b :
TypedBinOp v1 (v1 ◁ᵥ b @ (optional ty optty))%I v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 :=
TypedBinOp v1 (v1 ◁ᵥ b @ (optional ty optty))%I v2 (v2 ◁ᵥ optty) (EqOp i32) ot1 ot2 :=
λ T, i2p (type_eq_optional_refined v1 v2 ty optty ot1 ot2 T b).
Lemma type_eq_optional_neq v1 v2 ty optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} T :
opt_pre ty v1 v2 ∧
(∀ v, v1 ◁ᵥ ty -∗ T v (t2mt (false @ boolean i32)) ) -∗
typed_bin_op v1 (v1 ◁ᵥ ty) v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 T.
typed_bin_op v1 (v1 ◁ᵥ ty) v2 (v2 ◁ᵥ optty) (EqOp i32) ot1 ot2 T.
Proof.
iIntros "HT Hv1 Hv2". iIntros (Φ) "HΦ".
have [|v' Hv] := val_of_Z_is_Some None i32 (Z_of_bool false) => //.
......@@ -216,14 +216,14 @@ Section optional.
Qed.
Global Instance type_eq_optional_neq_inst v1 v2 ty optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} :
TypedBinOp v1 (v1 ◁ᵥ ty) v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 :=
TypedBinOp v1 (v1 ◁ᵥ ty) v2 (v2 ◁ᵥ optty) (EqOp i32) ot1 ot2 :=
λ T, i2p (type_eq_optional_neq v1 v2 ty optty ot1 ot2 T).
Lemma type_neq_optional v1 v2 ty optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} T b :
opt_pre ty v1 v2 ∧
destruct_hint DHintInfo (DestructHintOptionalNe b) (⌜b⌝ -∗ v1 ◁ᵥ ty -∗ T (i2v (Z_of_bool true) i32) (t2mt (true @ boolean i32))) ∧
destruct_hint DHintInfo (DestructHintOptionalNe (¬ b)) (⌜¬ b⌝ -∗ v1 ◁ᵥ optty -∗ T (i2v (Z_of_bool false) i32) (t2mt (false @ boolean i32))) -∗
typed_bin_op v1 (v1 ◁ᵥ b @ (optional ty optty)) v2 (v2 ◁ᵥ optty) NeOp ot1 ot2 T.
typed_bin_op v1 (v1 ◁ᵥ b @ (optional ty optty)) v2 (v2 ◁ᵥ optty) (NeOp i32) ot1 ot2 T.
Proof.
unfold destruct_hint. iIntros "HT Hv1 Hv2" (Φ) "HΦ".