Skip to content

Feature exception #806

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

Jump to bottom
Open
lyonel2017 wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Feature exception #806

lyonel2017 wants to merge 1 commit into from

Conversation

@lyonel2017
Copy link
Contributor

@lyonel2017 lyonel2017 commented Sep 9, 2025 •
edited
Loading

This PR introduce exceptions for Hoare Logic.

We can define exception :

exception assume.
exception assert.

We can raise exception using raise assume or raise (x = 3) assert (raise an exception when a condition is not true):

module M ={
  proc f (x:int) : int = {
    raise (x = 3) assert;
    x <- 1;
    if (x = 3)  {
       raise assume;
    }
    if (x=3) {
        raise assert;
      }
  return x;
  }
}.

We can define postconditions for each exception and a default postcondition:

lemma assume_assert : hoare [M.f : pre ==> post | assume:p1 |assert: p2 | p3].

Examples are available in examples/exception.ec.

@lyonel2017 lyonel2017 force-pushed the feature-exception branch 2 times, most recently from 415a5d1 to b415379 Compare September 21, 2025 19:49
@lyonel2017 lyonel2017 requested a review from strub September 21, 2025 19:49
@lyonel2017 lyonel2017 force-pushed the feature-exception branch 4 times, most recently from b717865 to 7e145ca Compare September 22, 2025 20:48
@lyonel2017 lyonel2017 force-pushed the feature-exception branch 4 times, most recently from cac4299 to 8a1385e Compare October 3, 2025 09:53
@lyonel2017 lyonel2017 force-pushed the feature-exception branch 2 times, most recently from 1185838 to ee89281 Compare November 1, 2025 11:50
@lyonel2017 lyonel2017 force-pushed the feature-exception branch 2 times, most recently from ae978f0 to 2fa2c24 Compare December 19, 2025 17:25
@lyonel2017 lyonel2017 marked this pull request as ready for review December 23, 2025 18:45
@lyonel2017 lyonel2017 requested a review from bgregoir December 23, 2025 18:45
bgregoir
bgregoir reviewed Dec 25, 2025
View reviewed changes
examples/exception.ec
proof.
proc.
wp.
auto => &hr <- />. smt.
Copy link
Contributor

@bgregoir bgregoir Dec 24, 2025

Choose a reason for hiding this comment

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

use smt(). instead of smt.
or

auto => /> /#.

examples/exception.ec
proof.
proc.
wp.
auto => &hr <- />. smt.
Copy link
Contributor

@bgregoir bgregoir Dec 24, 2025

Choose a reason for hiding this comment

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

same here

src/ecAst.ml
es_sr : stmt;
es_po : form; }

and post = (form * (EcPath.path, form) DMap.t * form option)
Copy link
Contributor

@bgregoir bgregoir Dec 24, 2025

Choose a reason for hiding this comment

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

Maybe we can remove form option if we create a special path "_".
Having special path can be useful also if we want to have return anywhere in the code: we can have a return exception. Similarly if we want to add "break".

Copy link
Contributor

@bgregoir bgregoir Dec 24, 2025

Choose a reason for hiding this comment

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

It would be good to use a different name than post. Maybe hoare_post.

src/ecAst.ml

let lift_hs_ss_inv (f: ss_inv -> hs_inv -> 'a) : inv -> inv -> 'a =
let f inv1 inv2 = match inv1, inv2 with
| Inv_ss ss1, Inv_hs ss2 -> f ss1 ss2
Copy link
Contributor

@bgregoir bgregoir Dec 24, 2025

Choose a reason for hiding this comment

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

ss2 seems to be a strange name for a hs_inv

src/ecAst.ml
let lift_hs_ss_inv (f: ss_inv -> hs_inv -> 'a) : inv -> inv -> 'a =
let f inv1 inv2 = match inv1, inv2 with
| Inv_ss ss1, Inv_hs ss2 -> f ss1 ss2
| _ -> failwith "expected only single sided invariants" in
Copy link
Contributor

@bgregoir bgregoir Dec 24, 2025

Choose a reason for hiding this comment

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

The error message does not reflect the pattern matching.

src/phl/ecPhlCase.ml
~tbh:err
~te:(t_equiv_case ?simplify f)
tc
| _ -> tc_error !!tc "exception are not supported"
Copy link
Contributor

@bgregoir bgregoir Dec 24, 2025

Choose a reason for hiding this comment

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

This should be an assert false

src/phl/ecPhlEager.ml
if not (Mpv2.subset eqm eqXs) then raise EqObsInError;
let eqi = Mpv2.union eqIs eqnm in
(fhyps, Mpv2.add_eqs env el er eqi)
| Sraise _e1, Sraise _e2 -> assert false (* FIXME *)
Copy link
Contributor

@bgregoir bgregoir Dec 24, 2025

Choose a reason for hiding this comment

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

Use a good error message.

src/phl/ecPhlUpto.ml
let check_branch (_, s) = check_bad_true env bad s.s_node in
List.iter (check_branch) bs
| Sassert _ -> ()
| Sraise _ -> assert false
Copy link
Contributor

@bgregoir bgregoir Dec 25, 2025

Choose a reason for hiding this comment

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

use a correct error message

src/phl/ecPhlWhile.ml

| Sassert e ->
(w, e_read_r env r e, c)
| Sraise _ -> assert false
Copy link
Contributor

@bgregoir bgregoir Dec 25, 2025

Choose a reason for hiding this comment

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

use a correct error message

src/phl/ecPhlWp.ml
| Not_found ->
match d with
| Some d -> d
| None -> tacuerror "unknow exception %a" EcPrinting.pp_path e
Copy link
Contributor

@bgregoir bgregoir Dec 25, 2025

Choose a reason for hiding this comment

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

Improve error message

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@bgregoir bgregoir bgregoir left review comments

@strub strub Awaiting requested review from strub

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@lyonel2017 @bgregoir