Skip to content

improved warnings for uptobad #763

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

improved warnings for uptobad #763

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 28 additions & 14 deletions src/phl/ecPhlUpto.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,11 @@ open EcCoreLib.CI_Real
let e_true = expr_of_form mhr f_true
let e_false = expr_of_form mhr f_false

let warn_uptobad env s =
EcEnv.notify ~immediate:true env `Warning
"Uptobad failed: %s" s


let is_lv_bad env bad x =
match bad with
| None -> false
Expand All @@ -27,14 +32,15 @@ let is_lv_bad env bad x =
let is_bad be env bad x e =
is_lv_bad env bad x && EqTest.for_expr env e be


let is_bad_true = is_bad e_true

let is_bad_false = is_bad e_false

let check_not_bad env bad lv =
match lv with
| LvVar _ -> not (is_lv_bad env bad lv)
| LvTuple xs -> not (List.exists (fun xt -> is_lv_bad env bad (LvVar xt)) xs)
| LvVar _ -> not (is_lv_bad env bad lv)
| LvTuple xs -> not (List.exists (fun xt -> is_lv_bad env bad (LvVar xt)) xs)

let rec s_upto_r env alpha bad s1 s2 =
match s1, s2 with
Expand All @@ -43,7 +49,7 @@ let rec s_upto_r env alpha bad s1 s2 =
is_bad_true env bad x1 e1 && is_bad_true env bad x2 e2 -> true
| i1 :: s1, i2 :: s2 ->
i_upto env alpha bad i1 i2 && s_upto_r env alpha bad s1 s2
| _, _ -> false
| _, _ -> warn_uptobad env "functions do not have the same structure";false

and s_upto env alpha bad s1 s2 = s_upto_r env alpha bad s1.s_node s2.s_node

Expand All @@ -54,7 +60,9 @@ and i_upto env alpha bad i1 i2 =
| Srnd (lv1, _), Srnd (lv2, _) ->
check_not_bad env bad lv1 &&
check_not_bad env bad lv2 &&
EqTest.for_instr env ~alpha i1 i2
if EqTest.for_instr env ~alpha i1 i2
then true
else (warn_uptobad env "instructions do not match"; false)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should print the two instructions here, this can be done using EcPrinting.pp_instr.


| Scall (lv1, f1, e1), Scall (lv2, f2, e2) ->
omap_dfl (check_not_bad env bad) true lv1 &&
Expand All @@ -64,12 +72,18 @@ and i_upto env alpha bad i1 i2 =
f_upto env bad f1 f2

| Sif (a1, b1, c1), Sif(a2, b2, c2) ->
EqTest.for_expr env a1 a2 &&
(if EqTest.for_expr env a1 a2
then true
else (warn_uptobad env "if statement conditions do not match"; false)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same remark, with EcPrinting.pp_expr

)&&
s_upto env alpha bad b1 b2 &&
s_upto env alpha bad c1 c2

| Swhile(a1,b1), Swhile(a2,b2) ->
EqTest.for_expr env a1 a2 &&
(if EqTest.for_expr env a1 a2
then true
else (warn_uptobad env "while statement conditions do not match"; false)
)&&
s_upto env alpha bad b1 b2

| Smatch(e1,bs1), Smatch(e2,bs2) when List.length bs1 = List.length bs2 -> begin
Expand All @@ -88,7 +102,7 @@ and i_upto env alpha bad i1 i2 =
try
EqTest.for_expr env ~alpha e1 e2
&& List.all2 (check_branch) bs1 bs2
with E.NotConv -> false
with E.NotConv -> warn_uptobad env "match statement mismatch";false
end

| Sassert a1, Sassert a2 ->
Expand All @@ -97,7 +111,7 @@ and i_upto env alpha bad i1 i2 =
| Sabstract id1, Sabstract id2 ->
EcIdent.id_equal id1 id2

| _, _ -> false
| _, _ -> warn_uptobad env "statement mismatch";false

and f_upto env bad f1 f2 =
let f1 = NormMp.norm_xfun env f1 in
Expand All @@ -121,7 +135,7 @@ and f_upto env bad f1 f2 =
EcPV.PV.check_depend env fv (m_functor f1.x_top); true) true bad &&
List.all2 (f_upto env bad) (OI.allowed o1) (OI.allowed o2)

| _, _ -> false
| _, _ -> warn_uptobad env "function kind mismatch";false

let rec s_upto_init env alpha bad s1 s2 =
match s1, s2 with
Expand All @@ -131,7 +145,7 @@ let rec s_upto_init env alpha bad s1 s2 =
s_upto_r env alpha (Some bad) s1 s2
| i1 :: s1, i2 :: s2 ->
i_upto env alpha None i1 i2 && s_upto_init env alpha bad s1 s2
| _, _ -> false
| _, _ -> warn_uptobad env "entry point functions do not have the same structure";false

let f_upto_init env bad f1 f2 =
let f1 = NormMp.norm_xfun env f1 in
Expand All @@ -147,12 +161,12 @@ let f_upto_init env bad f1 f2 =
let body1 = fd1.f_body and body2 = fd2.f_body in
List.all2 check_param fd1.f_locals fd2.f_locals &&
oall2 (EqTest.for_expr env) fd1.f_ret fd2.f_ret &&
( s_upto_init env alpha bad body1.s_node body2.s_node ||
s_upto env alpha (Some bad) body1 body2)
(s_upto_init env alpha bad body1.s_node body2.s_node ||
s_upto env alpha (Some bad) body1 body2)

| FBabs _, FBabs _ -> f_upto env (Some bad) f1 f2

| _, _ -> false
| _, _ -> warn_uptobad env "entry point function kind mismatch";false

let destr_bad f =
match destr_pvar f with
Expand Down Expand Up @@ -185,7 +199,7 @@ let t_uptobad_r tc =
tc_error !!tc ~who:"byupto" "the event should have the form \"E /\ !bad\" or \"!bad\""
in
if not (f_upto_init env bad pr1.pr_fun pr2.pr_fun) then
tc_error !!tc ~who:"byupto" "the two function are not equal upto bad";
tc_error !!tc ~who:"byupto" "up to bad tactic failed";
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have tried this, patch and I see not error message, excepted up to bad tactic failed.
Did you see something else?
I not use to the function EcEnv.notify. Can someone provide hint ?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that proof general does not display the warnings when there is an error. Anyway, the notify mechanism should not be used for extending the error message. Assume that you do a try upto, then you will end with a lot of warning messages that you don't want to see.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe we should brainstorm a bit about how to manage the communication with the user when launching tactics that do complex analysis. This includes upto, but also circuit-based analysis, sim, etc.
Clearly we need a bit more than yes/no as an answer because these tactics typically require some trial and error before the analysis goes through.
This could be a different mechanism than applying the tactic? Something in the same plane as search for example?

FApi.xmutate1 tc `HlUpto []

let t_uptobad = FApi.t_low0 "upto-bad" t_uptobad_r
Expand Down