Commit 8823bd56 authored by Michael Sammler's avatar Michael Sammler
Browse files

Control which sideconditions get shelved

parent 4ecc177a
Pipeline #52164 passed with stage
in 14 minutes and 25 seconds
......@@ -21,7 +21,7 @@ Section type.
repeat liRStep; liShow.
liInst Hevar γ.
repeat liRStep; liShow.
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
Unshelve. all: li_unshelve_sidecond; sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
Qed.
End type.
......@@ -1387,7 +1387,7 @@ let pp_proof : string -> func_def -> import list -> string list -> proof_kind
pp "@; all: print_typesystem_goal \"%s\" \"%s\"." def.func_name id
in
List.iter pp_do_step (List.cons "#0" (List.map fst invs_fb));
pp "@;Unshelve. all: sidecond_hook; prepare_sideconditions; ";
pp "@;Unshelve. all: li_unshelve_sidecond; sidecond_hook; prepare_sideconditions; ";
pp "normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.";
let tactics_items =
let is_all t =
......@@ -1409,6 +1409,7 @@ let pp_proof : string -> func_def -> import list -> string list -> proof_kind
in
List.iter (pp "@;+ %s") tactics_items;
pp "@;all: print_sidecondition_goal \"%s\"." def.func_name;
pp "@;Unshelve. all: try done; try apply: inhabitant; print_remaining_shelved_goal \"%s\"." def.func_name;
pp "@]@;Qed.";
(* Closing the section. *)
......
......@@ -22,7 +22,7 @@ Section proofs.
(* Establish the invariant *)
liInst Hevar id. iExists 0, 0.
iFrame. iSplit; [ done | by iApply ticket_range_empty ].
Unshelve. all: solve_goal.
Unshelve. all: li_unshelve_sidecond; sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
Qed.
(* Typing proof for [hyp_spin_lock]. *)
......@@ -268,10 +268,7 @@ Section proofs.
}
iIntros "_". repeat liRStep; liShow.
(* Solving side-conditions. *)
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
all: try (repeat match goal with [ H : _ |- _ ] => revert H end;
rewrite /LAST_TICKET /min_int /max_int /int_modulus /int_half_modulus;
rewrite /bits_per_int /bytes_per_int /bits_per_byte /=; lia).
Unshelve. all: li_unshelve_sidecond; sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
Qed.
(* Typing proof for [hyp_spin_unlock]. *)
......@@ -428,9 +425,6 @@ Section proofs.
(* Run the automation to finish the branch. *)
repeat liRStep; liShow.
(* Solving side-conditions. *)
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
all: try (repeat match goal with [ H : _ |- _ ] => revert H end;
rewrite /LAST_TICKET /min_int /max_int /int_modulus /int_half_modulus;
rewrite /bits_per_int /bytes_per_int /bits_per_byte /=; lia).
Unshelve. all: li_unshelve_sidecond; sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
Qed.
End proofs.
......@@ -13,6 +13,9 @@ Notation "'HIDDEN'" := (LET_ID _) (only printing).
Definition EVAR_ID {A} (x : A) : A := x.
Arguments EVAR_ID : simpl never.
Definition SHELVED_SIDECOND (P : Prop) : Prop := P.
Arguments SHELVED_SIDECOND : simpl never.
(** * Lemmas used by tactics *)
Section coq_tactics.
Context {Σ : gFunctors}.
......@@ -534,10 +537,23 @@ Ltac liTrue :=
| |- envs_entails _ True => notypeclasses refine (tac_true _)
end.
Ltac li_shelve_sidecond :=
idtac;
lazymatch goal with
| |- ?G => change_no_check (SHELVED_SIDECOND G); shelve
end.
Ltac li_unshelve_sidecond :=
idtac;
lazymatch goal with
| |- SHELVED_SIDECOND ?G => change_no_check G
| |- _ => shelve
end.
Ltac liFalse :=
lazymatch goal with
| |- envs_entails _ False => exfalso; shelve
| |- False => shelve
| |- envs_entails _ False => exfalso; li_shelve_sidecond
| |- False => li_shelve_sidecond
end.
(* There can be some goals where one should not call injection on an
......@@ -651,7 +667,7 @@ Ltac liSideCond :=
lazymatch goal with
| |- ?P _ =>
lazymatch P with
| shelve_hint _ => split; [ unfold shelve_hint; shelve |]
| shelve_hint _ => split; [ unfold shelve_hint; li_shelve_sidecond |]
| _ => first [
match P with
| context [via_vm_compute ?f ?a] =>
......@@ -671,7 +687,7 @@ Ltac liSideCond :=
(* We use done instead of fast_done here because solving more
sideconditions here is a bigger performance win than the overhead
of done. *)
| _ => split; [ first [ done | shelve ] | ]
| _ => split; [ first [ done | li_shelve_sidecond ] | ]
end ] end
| _ => fail "do_side_cond: unknown goal"
end.
......
From refinedc.typing Require Import type.
From refinedc.typing Require Import type globals.
From refinedc.lithium Require Import tactics.
From refinedc.typing.automation Require Import solvers.
......@@ -105,11 +105,8 @@ Ltac solve_goal_prepare_tac ::=
repeat match goal with | H : CASE_DISTINCTION_INFO _ _ _ |- _ => clear H end.
(** * Tactics for showing failures to the user *)
Ltac clear_for_print_goal :=
repeat match goal with | H : BLOCK_PRECOND _ _ |- _ => clear H end.
Ltac print_goal :=
clear_for_print_goal;
Ltac print_current_location :=
try lazymatch reverse goal with
| H : CURRENT_LOCATION ?l ?up_to_date |- _ =>
let rec print_loc_info l :=
......@@ -125,7 +122,9 @@ Ltac print_goal :=
end in
print_loc_info l;
clear H
end;
end.
Ltac print_case_distinction_info :=
repeat lazymatch reverse goal with
| H : CASE_DISTINCTION_INFO ?hint ?i ?l |- _ =>
lazymatch i with
......@@ -142,11 +141,25 @@ Ltac print_goal :=
| [] => idtac
end;
clear H
end;
idtac "Goal:";
end.
Ltac print_coq_hyps :=
try match reverse goal with
| H : ?X |- _ => idtac H ":" X; fail
end;
| H : ?X |- _ =>
lazymatch X with
| BLOCK_PRECOND _ _ => fail
| gFunctors => fail
| typeG _ => fail
| globalG _ => fail
| _ => idtac H ":" X; fail
end
end.
Ltac print_goal :=
print_current_location;
print_case_distinction_info;
idtac "Goal:";
print_coq_hyps;
idtac "---------------------------------------";
match goal with
| |- ?G => idtac G
......@@ -155,9 +168,32 @@ Ltac print_goal :=
idtac "".
Ltac print_typesystem_goal fn block :=
idtac "Type system got stuck in function" fn "in block" block "!";
print_goal; admit.
lazymatch goal with
| |- ?P ?Q =>
idtac "Cannot instantiate evar in" fn "in block" block "!";
print_current_location;
print_case_distinction_info;
idtac "Goal:";
print_coq_hyps;
idtac "---------------------------------------";
idtac P;
(* TODO: Should we print the continuation? It might confuse the user and
it usually is not helpful. *)
(* idtac ""; *)
(* idtac "Continuation:"; *)
(* idtac Q; *)
idtac "";
idtac "";
admit
| |- _ =>
idtac "Type system got stuck in function" fn "in block" block "!";
print_goal; admit
end.
Ltac print_sidecondition_goal fn :=
idtac "Cannot solve side condition in function" fn "!";
print_goal; admit.
Ltac print_remaining_shelved_goal fn :=
idtac "Shelved goal remaining in " fn "!";
print_goal; admit.
......@@ -1522,8 +1522,9 @@ Section typing.
TypedAnnotStmt (ShareAnnot) l (l ◁ₗ ty) :=
λ T, i2p (annot_share l ty T).
Definition STOPPED : iProp Σ := False.
Lemma annot_stop l β ty T:
(l ◁ₗ{β} ty - False) -
(l ◁ₗ{β} ty - STOPPED) -
typed_annot_stmt (StopAnnot) l (l ◁ₗ{β} ty) T.
Proof. iIntros "HT Hl". iDestruct ("HT" with "Hl") as %[]. Qed.
Global Instance annot_stop_inst l β ty:
......
......@@ -185,8 +185,8 @@ int add1(int a) {
not prove. Everything above the long line are the facts which are
known at this point in the program and below you can see the
statement which could not be proven. In this example, RefinedC
cannot prove [(n + 1) ∈ i32] which means that [n + 1] is
in the range of a signed 32bit integer ([i32]). As we have
cannot prove [n + 1 ≤ max_int i32] which means that [n + 1] is
in the range of a signed 32-bit integer ([i32]). As we have
discussed before, this condition is generated by typechecking of
the [+] since overflow is undefined behavior in the RefinedC C
semantics. If you now look at the facts we know, we can see that
......@@ -201,13 +201,13 @@ int add1(int a) {
Based on the next example, we want to get a better high-level
understanding how the typechecker of RefinedC works.
When a C program is translated into Coq by ail_to_coq, it is
When a C program is translated into Coq by the frontend, it is
transformed into a control flow graph representation.
Aside: If you are interested, you can look at the t1_basic_code.v
file to see the representation in Coq. This is only for
understanding what happens under the hood, you usually do not
interact with it directly.
Aside: If you are interested, you can look at the file
proofs/t01_basic/generated_code.v to see the representation
in Coq. This is only for understanding what happens under the
hood, you usually do not interact with it directly.
The high-level picture of how the the RefinedC typechecker works is
very simple: Typechecking starts at each basic block, which has an
......@@ -226,13 +226,12 @@ int add1(int a) {
following [min] function. Currently, it verifies without problems.
But try changing the condition in the [assert] and see what happens.
E.g. if you change the condition to [r == a] you should get an
E.g. if you change the first assert to [r == a] you should get an
error that RefinedC cannot prove [b = a] on the line of the assert.
If you look at the output of RefinedC, you should also see
something like:
Case distinction (DHintDestruct bool (bool_decide (a < b))) -
(false, DestructHintIfBool (bool_decide (a < b)))
Case distinction (if bool_decide (a < b)) -> false
at "tutorial/t01_basic.c" [ 256 : 7 - 256 : 12 ]
This kind of output gives us some information which case
......@@ -240,12 +239,12 @@ int add1(int a) {
i.e. from which path through the program this sidecondition arises.
In this example, we see that the case distinction comes from the [a
< b] inside the if statement via the location information in the
last line and also based on [DestructHintIfBool (bool_decide (a <
b))]. The [false] tells us that we are in the case where the check
last line and also based on [(if bool_decide (a < b))].
The [false] tells us that we are in the case where the check
failed, i.e. type checking went through the else branch.
Play a bit around with this example until you have an understanding
how typechecking in RefinedC works!
Play a bit around with this example until you have a better
understanding how typechecking in RefinedC works!
*/
[[rc::parameters("a : Z", "b : Z")]]
......@@ -260,8 +259,8 @@ int min(int a, int b) {
}
// try different conditions here (e.g. r == a, r > b) and see what
// happens
assert(r <= b); // these are C assertions
assert(r <= a);
assert(r <= b); // these are C assertions
return r;
}
......@@ -272,19 +271,19 @@ int min(int a, int b) {
As you can see, loops must have an annotated loop invariant.
ATTENTION: If you forget annotating a loop invariant, the
typechecker might happily go around the loop forever and never
terminate!
frontend will automatically generate a loop invariant that
is very likely wrong.
The main part of the loop invariant annotation is the [rc::inv_vars]
annotation. It specifies the types of the local variables at the
beginning of the loop, /before/ the check of the loop condition.
[rc::exists] gives Coq variables which might vary from iteration to
interation. Here, [n] is [a] plus how much we have already added.
interation. Here, [acc] is [va] plus how much we have already added.
[rc::constraints] gives additional constraints which have to hold
before the check of the loop condition. Here we have to make sure
that [n], the value stored in [a], is not negative, as otherwise the
that [acc], the value stored in [a], is not negative, as otherwise the
loop will underflow.
Note that RefinedC does not prove termination, so there is no need
......@@ -330,29 +329,29 @@ int looping_add(int a, int b) {
gets stuck. For this example, it should look something like
_ : block{ "#1" }
_ : i2v (va + vb - acc + 1) i32 ◁ᵥ (va + vb - acc + 1) @ int i32
_ : arg_b ◁ₗ (va + vb - acc + 1) @ int i32
_ : arg_a ◁ₗ acc @ int i32
_ : i2v (va + vb - acc + 1) i32 : (va + vb - acc + 1) @ int<i32>
_ : own arg_b : (va + vb - acc + 1) @ int<i32>
_ : own arg_a : acc @ int<i32>
--------------------------------------∗
The first line only tells us that there is a precondtion for block
"#1", but the other ones are more interesting:
arg_a ◁ₗ acc @ int i32
own arg_a : acc @ int<i32>
Tells us that the /location/ where [a] is stored has type [acc @ int
i32]. In general, RefinedC has two kinds of type assignments:
- The main type assignment of RefinedC is based on locations in
memory, sometimes also called places or lvalues. The location
type assignment [l ◁ₗ ty] states that location [l] stores
type assignment [own l : ty] states that location [l] stores
something of type [ty]. All local variables and arguments are
represented as locations in RefinedC, so most of the reasoning is
done using this type assignment. All types have a location type
assignment.
- The other type assignment is more traditional and assigns types
to values, i.e. [v ◁ᵥ ty]. While most types support this value
to values, i.e. [v : ty]. While most types support this value
type assignment (we call them "movable" types, some types don't
support it (we call them "immovable" types). For examples, you
might have a structures where one field points to another field
......@@ -414,7 +413,7 @@ void init_int_test(int* out) {
Structs are represented with the [struct<struct_layout, field
types...>] RefinedC type. The [struct_layout], which corresponds to
C type of the struct, is necessary since it contains the names of
the fields and their sizes. ail_to_coq automatically generates the
the fields and their sizes. The frontend automatically generates the
layout for each structure in the source file as [struct_<name of
the struct>], i.e. in this example as [struct_basic]. Operations on
structures, e.g. initializing, accessing fields, copying structures
......@@ -434,5 +433,5 @@ void struct_test(struct basic* out) {
/**
However, most of the time you will not work with the [struct] type
directly, but use annotations on structures to define new types, as
we will see in t3_list.c...
we will see in t03_list.c...
*/
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