-
Axiom wp_init_initlist_agg :
forall cls (
base :
ptr)
cv es ty Q,
-
decompose_type ty = (cv, Tnamed cls) ->
-
(let do_const Q :=
-
if q_const cv
-
then wp_make_const tu base (
Tnamed cls)
Q
-
else Q
+
Axiom wp_init_initlist_agg :
forall cls (
base :
ptr)
cv es ty Q,
+
decompose_type ty = (cv, Tnamed cls) ->
+
(let do_const Q :=
+
if q_const cv
+
then wp_make_const tu base (
Tnamed cls)
Q
+
else Q
in
-
match tu.(
types)
!! cls with
+
match tu.(
types)
!! cls with
|
Some (
Gstruct s) =>
-
match struct_inits s es with
+
match struct_inits s es with
|
Some inits =>
-
letI* := wp_struct_initializer_list tu s ρ cls base inits in
-
do_const (
Q FreeTemps.id)
+
letI* := wp_struct_initializer_list tu s ρ cls base inits in
+
do_const (
Q FreeTemps.id)
|
_ =>
False
end
|
Some (
Gunion u) =>
-
match union_inits u es with
+
match union_inits u es with
|
Some inits =>
-
letI* := wp_union_initializer_list tu u ρ cls base inits in
-
do_const (
Q FreeTemps.id)
+
letI* := wp_union_initializer_list tu u ρ cls base inits in
+
do_const (
Q FreeTemps.id)
|
_ =>
False
end
|
_ =>
False
end)
-
|-- wp_init ty base (
Einitlist es None ty)
Q.
+
|-- wp_init ty base (
Einitlist es None ty)
Q.
End with_resolve.
@@ -1987,7 +2011,7 @@
bedrock.lang.cpp.logic.expr
Section with_resolve__arrayloop.
-
Context `{
Σ :
cpp_logic} {
σ :
genv}.
+
Context `{
Σ :
cpp_logic} {
σ :
genv}.
Variable (
tu :
translation_unit).
@@ -2029,37 +2053,37 @@
bedrock.lang.cpp.logic.expr
injective and we don't expect the
N to be very large in practice so we pick
a very naive encoding.
*)
-
Definition N_to_bs (
n :
N) :
bs :=
+
Definition N_to_bs (
n :
N) :
bs :=
N.peano_rect (
fun _ =>
bs)
BS.EmptyString
- (
fun _ x =>
BS.String "1"
x)
n.
+ (
fun _ x =>
BS.String "1"
x)
n.
-
Definition arrayloop_loop_index (
n :
N) :
bs := "!loop_index"
++ N_to_bs n.
-
Definition opaque_val (
n :
N) :
bs := "%opaque"
++ N_to_bs n.
+
Definition arrayloop_loop_index (
n :
N) :
bs := "!loop_index"
++ N_to_bs n.
+
Definition opaque_val (
n :
N) :
bs := "%opaque"
++ N_to_bs n.
-
Axiom wp_lval_opaque_ref :
forall n ρ ty Q,
-
wp_lval tu ρ (
Evar (
opaque_val n)
ty)
Q
-
|-- wp_lval tu ρ (
Eopaque_ref n Lvalue ty)
Q.
+
Axiom wp_lval_opaque_ref :
forall n ρ ty Q,
+
wp_lval tu ρ (
Evar (
opaque_val n)
ty)
Q
+
|-- wp_lval tu ρ (
Eopaque_ref n Lvalue ty)
Q.
-
Axiom wp_xval_opaque_ref :
forall n ρ ty Q,
-
wp_lval tu ρ (
Evar (
opaque_val n)
ty)
Q
-
|-- wp_xval tu ρ (
Eopaque_ref n Xvalue ty)
Q.
+
Axiom wp_xval_opaque_ref :
forall n ρ ty Q,
+
wp_lval tu ρ (
Evar (
opaque_val n)
ty)
Q
+
|-- wp_xval tu ρ (
Eopaque_ref n Xvalue ty)
Q.
-
Axiom wp_operand_arrayloop_index :
forall ρ level ty Q,
-
Exists v,
-
((Exists q, _local ρ (
arrayloop_loop_index level)
-
|-> primR (
erase_qualifiers ty)
q v) **
-
True) //\\ Q v FreeTemps.id
-
|-- wp_operand tu ρ (
Earrayloop_index level ty)
Q.
+
Axiom wp_operand_arrayloop_index :
forall ρ level ty Q,
+
Exists v,
+
((Exists q, _local ρ (
arrayloop_loop_index level)
+
|-> primR (
erase_qualifiers ty)
q v) **
+
True) //\\ Q v FreeTemps.id
+
|-- wp_operand tu ρ (
Earrayloop_index level ty)
Q.
Definition _arrayloop_init
- (
ρ :
region) (
level :
N)
- (
targetp :
ptr) (
init :
Expr)
- (
ty :
type) (
Q :
epred)
+ (
ρ :
region) (
level :
N)
+ (
targetp :
ptr) (
init :
Expr)
+ (
ty :
type) (
Q :
epred)
- (
sz :
N) (
idx :
N)
+ (
sz :
N) (
idx :
N)
:
mpred :=
-
let loop_index :=
_local ρ (
arrayloop_loop_index level)
in
+
let loop_index :=
_local ρ (
arrayloop_loop_index level)
in
N.peano_rect (
fun _ :
N =>
N -> mpred)
- (
fun _ =>
Q)
- (
fun _ rest idx =>
+ (
fun _ =>
Q)
+ (
fun _ rest idx =>
-
loop_index |-> primR Tu64 (
cQp.c 1)
idx -*
-
wp_initialize tu ρ ty (
targetp .[ erase_qualifiers ty ! idx ])
init
- (
fun free =>
interp free $
-
loop_index |-> primR Tu64 (
cQp.c 1)
idx **
-
rest (
N.succ idx)))
sz idx.
-
-
-
Axiom wp_init_arrayloop_init :
forall oname level sz ρ (
trg :
ptr)
src init ety ty Q,
-
has_type_prop (
Vn sz)
Tu64 ->
-
is_array_of ty ety ->
-
wp_glval tu ρ src
- (
fun p free =>
-
Forall idxp,
-
trg |-> validR -*
-
_arrayloop_init (
Rbind (
opaque_val oname)
p
- (
Rbind (
arrayloop_loop_index level)
idxp ρ))
-
level trg init ety
- (
trg |-> type_ptrR (
Tarray ety sz)
-* Q free)
-
sz 0)
-
|-- wp_init tu ρ (
Tarray ety sz)
trg
- (
Earrayloop_init oname src level sz init ty)
Q.
+
loop_index |-> primR Tu64 (
cQp.c 1)
idx -*
+
wp_initialize tu ρ ty (
targetp .[ erase_qualifiers ty ! idx ])
init
+ (
fun free =>
interp free $
+
loop_index |-> primR Tu64 (
cQp.c 1)
idx **
+
rest (
N.succ idx)))
sz idx.
+
+
+
Axiom wp_init_arrayloop_init :
forall oname level sz ρ (
trg :
ptr)
src init ety ty Q,
+
has_type_prop (
Vn sz)
Tu64 ->
+
is_array_of ty ety ->
+
wp_glval tu ρ src
+ (
fun p free =>
+
Forall idxp,
+
trg |-> validR -*
+
_arrayloop_init (
Rbind (
opaque_val oname)
p
+ (
Rbind (
arrayloop_loop_index level)
idxp ρ))
+
level trg init ety
+ (
trg |-> type_ptrR (
Tarray ety sz)
-* Q free)
+
sz 0)
+
|-- wp_init tu ρ (
Tarray ety sz)
trg
+ (
Earrayloop_init oname src level sz init ty)
Q.
-
Definition wp_cond2 {
T} (
vc :
ValCat) (
wp :
translation_unit -> region -> Expr -> (T -> FreeTemps.t -> epred) -> mpred) :
Prop :=
-
forall tu ρ n ty common tst th el (
Q :
T -> FreeTemps -> mpred),
-
Forall p,
-
wp_initialize tu ρ (
type_of common)
p common (
fun free =>
-
let ρ' :=
Rbind (
opaque_val n)
p ρ in
-
wp_test tu ρ' tst (
fun c free'' =>
-
let free := (
free'' >*> FreeTemps.delete ty p >*> free)%
free in
-
if c
-
then wp tu ρ' th (
fun v free' =>
Q v (
free' >*> free))
-
else wp tu ρ' el (
fun v free' =>
Q v (
free' >*> free))))
-
|-- wp tu ρ (
Eif2 n common tst th el vc ty)
Q.
+
Definition wp_cond2 {
T} (
vc :
ValCat) (
wp :
translation_unit -> region -> Expr -> (T -> FreeTemps.t -> epred) -> mpred) :
Prop :=
+
forall tu ρ n ty common tst th el (
Q :
T -> FreeTemps -> mpred),
+
Forall p,
+
wp_initialize tu ρ (
type_of common)
p common (
fun free =>
+
let ρ' :=
Rbind (
opaque_val n)
p ρ in
+
wp_test tu ρ' tst (
fun c free'' =>
+
let free := (
free'' >*> FreeTemps.delete ty p >*> free)%
free in
+
if c
+
then wp tu ρ' th (
fun v free' =>
Q v (
free' >*> free))
+
else wp tu ρ' el (
fun v free' =>
Q v (
free' >*> free))))
+
|-- wp tu ρ (
Eif2 n common tst th el vc ty)
Q.
Axiom wp_lval_condition2 :
Reduce (
wp_cond2 Lvalue wp_lval).
@@ -2162,16 +2186,16 @@
bedrock.lang.cpp.logic.expr
end of the full expression because (in this trace), `C(1)` would be
constructing a temporary.
*)
-
Axiom wp_init_condition2 :
forall tu ρ n ty common tst th el vc p Q,
-
Forall p,
-
wp_initialize tu ρ (
type_of common)
p common (
fun free =>
-
let ρ' :=
Rbind (
opaque_val n)
p ρ in
-
wp_test tu ρ' tst (
fun c free'' =>
-
let free := (
free'' >*> FreeTemps.delete ty p >*> free)%
free in
-
if c
-
then wp_init tu ρ' ty p th (
fun free' =>
Q (
free' >*> free))
-
else wp_init tu ρ' ty p el (
fun free' =>
Q (
free' >*> free))))
-
|-- wp_init tu ρ ty p (
Eif2 n common tst th el vc ty)
Q.
+
Axiom wp_init_condition2 :
forall tu ρ n ty common tst th el vc p Q,
+
Forall p,
+
wp_initialize tu ρ (
type_of common)
p common (
fun free =>
+
let ρ' :=
Rbind (
opaque_val n)
p ρ in
+
wp_test tu ρ' tst (
fun c free'' =>
+
let free := (
free'' >*> FreeTemps.delete ty p >*> free)%
free in
+
if c
+
then wp_init tu ρ' ty p th (
fun free' =>
Q (
free' >*> free))
+
else wp_init tu ρ' ty p el (
fun free' =>
Q (
free' >*> free))))
+
|-- wp_init tu ρ ty p (
Eif2 n common tst th el vc ty)
Q.
End with_resolve__arrayloop.
diff --git a/docs/_static/coqdoc/indexpage.html b/docs/_static/coqdoc/indexpage.html
index 4dc285ca..aa18d1f2 100644
--- a/docs/_static/coqdoc/indexpage.html
+++ b/docs/_static/coqdoc/indexpage.html
@@ -66,7 +66,7 @@
Z |
_ |
other |
-
(9687 entries) |
+
(9689 entries) |
| Notation Index |
@@ -290,7 +290,7 @@
Z |
_ |
other |
-(604 entries) |
+(605 entries) |
| Projection Index |
@@ -514,7 +514,7 @@
Z |
_ |
other |
-(1470 entries) |
+(1471 entries) |
@@ -3407,6 +3407,7 @@
Global Index
expr_notations [library]
Expr.AddConst [constructor, in
bedrock.lang.cpp.logic.expr]
Expr.arrayloop_loop_index [definition, in
bedrock.lang.cpp.logic.expr]
+
Expr.can_represent_null [definition, in
bedrock.lang.cpp.logic.expr]
Expr.classify_cast [definition, in
bedrock.lang.cpp.logic.expr]
Expr.dispatch [definition, in
bedrock.lang.cpp.logic.expr]
Expr.dispatch_frame [lemma, in
bedrock.lang.cpp.logic.expr]
@@ -3513,6 +3514,7 @@
Global Index
Expr.wp_operand_cast_reinterpret [axiom, in
bedrock.lang.cpp.logic.expr]
Expr.wp_operand_cast_user [axiom, in
bedrock.lang.cpp.logic.expr]
Expr.wp_init_cast_user [axiom, in
bedrock.lang.cpp.logic.expr]
+
Expr.wp_operand_cast_null_int [axiom, in
bedrock.lang.cpp.logic.expr]
Expr.wp_operand_cast_null [axiom, in
bedrock.lang.cpp.logic.expr]
Expr.wp_operand_cast_integral [axiom, in
bedrock.lang.cpp.logic.expr]
Expr.wp_operand_cast_bitcast [axiom, in
bedrock.lang.cpp.logic.expr]
@@ -14898,6 +14900,7 @@
Axiom Index
Expr.wp_operand_cast_reinterpret [in
bedrock.lang.cpp.logic.expr]
Expr.wp_operand_cast_user [in
bedrock.lang.cpp.logic.expr]
Expr.wp_init_cast_user [in
bedrock.lang.cpp.logic.expr]
+
Expr.wp_operand_cast_null_int [in
bedrock.lang.cpp.logic.expr]
Expr.wp_operand_cast_null [in
bedrock.lang.cpp.logic.expr]
Expr.wp_operand_cast_integral [in
bedrock.lang.cpp.logic.expr]
Expr.wp_operand_cast_bitcast [in
bedrock.lang.cpp.logic.expr]
@@ -19196,6 +19199,7 @@
Definition Index
Expr_ind [in
bedrock.lang.cpp.syntax.expr]
Expr_rect [in
bedrock.lang.cpp.syntax.expr]
Expr.arrayloop_loop_index [in
bedrock.lang.cpp.logic.expr]
+
Expr.can_represent_null [in
bedrock.lang.cpp.logic.expr]
Expr.classify_cast [in
bedrock.lang.cpp.logic.expr]
Expr.dispatch [in
bedrock.lang.cpp.logic.expr]
Expr.fill_initlist [in
bedrock.lang.cpp.logic.expr]
@@ -20286,7 +20290,7 @@
Definition Index
Z |
_ |
other |
-
(9687 entries) |
+
(9689 entries) |
| Notation Index |
@@ -20510,7 +20514,7 @@ Definition Index
Z |
_ |
other |
-(604 entries) |
+(605 entries) |
| Projection Index |
@@ -20734,7 +20738,7 @@ Definition Index
Z |
_ |
other |
-(1470 entries) |
+(1471 entries) |