Commit 2c7772a9 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Add support for the comma operator.

parent 4ad473f2
Pipeline #46953 passed with stage
in 29 minutes and 10 seconds
......@@ -163,6 +163,22 @@ Section code.
Definition loc_206 : location_info := LocationInfo file_0 50 34 50 38.
Definition loc_209 : location_info := LocationInfo file_0 49 19 49 29.
Definition loc_212 : location_info := LocationInfo file_0 48 22 48 28.
Definition loc_217 : location_info := LocationInfo file_0 64 2 64 31.
Definition loc_218 : location_info := LocationInfo file_0 66 2 66 22.
Definition loc_219 : location_info := LocationInfo file_0 66 9 66 21.
Definition loc_220 : location_info := LocationInfo file_0 66 9 66 14.
Definition loc_221 : location_info := LocationInfo file_0 66 9 66 10.
Definition loc_222 : location_info := LocationInfo file_0 66 9 66 10.
Definition loc_223 : location_info := LocationInfo file_0 66 13 66 14.
Definition loc_224 : location_info := LocationInfo file_0 66 13 66 14.
Definition loc_225 : location_info := LocationInfo file_0 66 16 66 21.
Definition loc_226 : location_info := LocationInfo file_0 66 16 66 17.
Definition loc_227 : location_info := LocationInfo file_0 66 16 66 17.
Definition loc_228 : location_info := LocationInfo file_0 66 20 66 21.
Definition loc_229 : location_info := LocationInfo file_0 66 20 66 21.
Definition loc_230 : location_info := LocationInfo file_0 64 10 64 30.
Definition loc_231 : location_info := LocationInfo file_0 64 11 64 25.
Definition loc_232 : location_info := LocationInfo file_0 64 27 64 29.
(* Definition of function [test1]. *)
Definition impl_test1 : function := {|
......@@ -474,4 +490,22 @@ Section code.
]> $
)%E
|}.
(* Definition of function [test_comma]. *)
Definition impl_test_comma : function := {|
f_args := [
];
f_local_vars := [
("x", it_layout i32)
];
f_init := "#0";
f_code := (
<[ "#0" :=
"x" <-{ it_layout i32 }
LocInfoE loc_230 ((LocInfoE loc_231 (NULL)) ,{PtrOp, IntOp i32} (LocInfoE loc_232 (i2v 42 i32))) ;
locinfo: loc_218 ;
Return (LocInfoE loc_219 ((LocInfoE loc_220 ((LocInfoE loc_221 (use{it_layout i32} (LocInfoE loc_222 ("x")))) +{IntOp i32, IntOp i32} (LocInfoE loc_223 (use{it_layout i32} (LocInfoE loc_224 ("x")))))) ,{IntOp i32, IntOp i32} (LocInfoE loc_225 ((LocInfoE loc_226 (use{it_layout i32} (LocInfoE loc_227 ("x")))) -{IntOp i32, IntOp i32} (LocInfoE loc_228 (use{it_layout i32} (LocInfoE loc_229 ("x"))))))))
]> $
)%E
|}.
End code.
From refinedc.typing Require Import typing.
From refinedc.examples.tests Require Import generated_code.
From refinedc.examples.tests Require Import generated_spec.
Set Default Proof Using "Type".
(* Generated from [examples/tests.c]. *)
Section proof_test_comma.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [test_comma]. *)
Lemma type_test_comma :
typed_function impl_test_comma type_of_test_comma.
Proof.
Open Scope printing_sugar.
start_function "test_comma" ([]) => local_x.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "test_comma" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: print_sidecondition_goal "test_comma".
Qed.
End proof_test_comma.
......@@ -27,4 +27,8 @@ Section spec.
(* Specifications for function [test_bits]. *)
Definition type_of_test_bits :=
fn( () : (); True) () : (), (void); True.
(* Specifications for function [test_comma]. *)
Definition type_of_test_comma :=
fn( () : (); True) () : (), ((0) @ (int (i32))); True.
End spec.
generated_proof_return1.v
generated_proof_test1.v
generated_proof_test_bits.v
generated_proof_test_comma.v
generated_proof_test_ternary.v
generated_proof_unreachable.v
......@@ -58,3 +58,10 @@ void test_bits() {
assert(~(-2) == 1);
assert(~0 == -1);
}
[[rc::returns("{0} @ int<i32>")]]
int test_comma(){
int x = (NULL, 42);
return x + x, x - x;
}
......@@ -471,7 +471,7 @@ let rec translate_expr : bool -> op_type option -> ail_expr -> expr =
| Ge -> GeOp
| And -> not_impl loc "nested && operator"
| Or -> not_impl loc "nested || operator"
| Comma -> not_impl loc "binary operator (Comma)"
| Comma -> CommaOp
| Arithmetic(op) ->
arith_op := true;
match op with
......
......@@ -28,7 +28,7 @@ type un_op =
type bin_op =
| AddOp | SubOp | MulOp | DivOp | ModOp | AndOp | OrOp | XorOp | ShlOp
| ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp
| ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp | CommaOp
type value =
| Null
......
......@@ -122,6 +122,7 @@ let pp_bin_op : Coq_ast.bin_op pp = fun ff op ->
| GtOp -> ">"
| LeOp -> "≤"
| GeOp -> "≥"
| CommaOp -> ","
let rec pp_expr : Coq_ast.expr pp = fun ff e ->
let pp fmt = Format.fprintf ff fmt in
......@@ -145,19 +146,22 @@ let rec pp_expr : Coq_ast.expr pp = fun ff e ->
| BinOp(op,ty1,ty2,e1,e2) ->
begin
match (ty1, ty2, op) with
| (OpPtr(l), OpInt(_), AddOp) ->
| (_ , _ , CommaOp) ->
pp "(%a) %a{%a, %a} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
| (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) ->
| (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(_), _) ->
| (OpPtr(_), OpInt(_), _ ) ->
panic_no_pos "Binop [%a] not supported on pointers."
pp_bin_op op
| (OpInt(_), OpPtr(_), _) ->
| (OpInt(_), OpPtr(_), _ ) ->
panic_no_pos "Wrong ordering of integer pointer binop [%a]."
pp_bin_op op
| _ ->
| _ ->
pp "(%a) %a{%a, %a} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
end
......
......@@ -16,7 +16,7 @@ Inductive op_type : Set :=
(* 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
| ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp | Comma
(* Ptr is the second argument and pffset the first *)
| PtrOffsetOp (ly : layout) | PtrNegOffsetOp (ly : layout).
......@@ -318,6 +318,8 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
val_to_Z_weak v2 it = Some n2
val_of_Z (if it_signed it then n else n `mod` int_modulus it) it = Some v
eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
| CommaOp ot1 ot2 σ v1 v2:
eval_bin_op Comma ot1 ot2 σ v1 v2 v2
.
Inductive eval_un_op : un_op op_type state val val Prop :=
......
......@@ -46,6 +46,8 @@ Notation "e1 |{ ot1 , ot2 } e2" := (BinOp OrOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 |{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 ^{ ot1 , ot2 } e2" := (BinOp XorOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 ^{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 ,{ ot1 , ot2 } e2" := (BinOp Comma ot1 ot2 e1%E e2%E)
(at level 30, format "e1 ,{ ot1 , ot2 } e2") : expr_scope.
(* 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.
......
......@@ -623,6 +623,18 @@ Section typing.
TypedBinOp v1 P1 v2 P2 op ot1 ot2 | 1000 :=
λ T, i2p (typed_binop_simplify v1 P1 v2 P2 T o1 o2 ot1 ot2 op).
Lemma typed_binop_comma v1 v2 P (ty : type) ot1 ot2 `{!Movable ty} T:
(P - T v2 (t2mt ty)) -
typed_bin_op v1 P v2 (v2 ◁ᵥ ty) Comma ot1 ot2 T.
Proof.
iIntros "HT H1 H2" (Φ) "HΦ". iApply (wp_binop_det v2). iSplit.
- iIntros (??) "_ !%". split; [ by inversion 1 | move => ->; constructor ].
- iDestruct ("HT" with "H1") as "HT". iApply ("HΦ" $! v2 (t2mt ty) with "H2 HT").
Qed.
Global Instance typed_binop_comma_inst v1 v2 P (ty : type) ot1 ot2 `{!Movable ty}:
TypedBinOp v1 P v2 (v2 ◁ᵥ ty) Comma ot1 ot2 :=
λ T, i2p (typed_binop_comma v1 v2 P ty ot1 ot2 T).
Lemma typed_unop_simplify v P T n ot {SH : SimplifyHyp P (Some n)} op:
(SH (find_in_context (FindValP v) (λ P, typed_un_op v P op ot T))).(i2p_P) -
typed_un_op v P op ot T.
......
Supports Markdown
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