From 3943ad074a7b488d2eb3deb474a6450b0879f4e6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 10 Nov 2024 14:11:46 +0100 Subject: [PATCH 1/4] Fix a bug in the pre-pass which eliminates the breaks --- compiler/InterpreterLoops.ml | 2 +- compiler/PrePasses.ml | 63 +++++++++++++++++++++++++++++------- 2 files changed, 52 insertions(+), 13 deletions(-) diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index c33c34a6..b252e299 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -395,7 +395,7 @@ let eval_loop (config : config) (span : span) (eval_loop_body : stl_cm_fun) : in (* We want to make sure the loop will *not* manipulate shared avalues - containing themselves shared loans (i.e., nested shared loans in + themselves containing shared loans (i.e., nested shared loans in the abstractions), because it complexifies the matches between values (when joining environments, or checking that two environments are equivalent). diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml index 43364979..3bf4e058 100644 --- a/compiler/PrePasses.ml +++ b/compiler/PrePasses.ml @@ -191,7 +191,33 @@ let remove_useless_cf_merges (crate : crate) (f : fun_decl) : fun_decl = } }; ]} - *) + + We also insert the statements occurring after branchings (matches or + if then else) inside the branches. For instance: + {[ + if b { + s0; + } + else { + s1; + } + return; + + ~~> + + if b { + s0; + return; + } + else { + s1; + return; + } + ]} + + This is necessary because loops might appear inside branchings: if we don't + do this some paths inside the loop might not end with a break/continue/return.Aeneas + *) let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl = let f0 = f in @@ -229,7 +255,11 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl = | Break i -> cassert __FILE__ __LINE__ (i = 0) st.span "Breaks to outer loops are not supported yet"; - { st with content = nst.content } + { + st with + content = nst.content; + comments_before = st.comments_before @ nst.comments_before; + } | _ -> super#visit_statement entered_loop st end in @@ -237,27 +267,36 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl = in (* The visitor *) - let obj = + let replace_visitor = object inherit [_] map_statement as super - method! visit_Sequence env st1 st2 = - match st1.content with - | Loop _ -> - cassert __FILE__ __LINE__ - (statement_has_no_loop_break_continue st2) - st2.span "Sequences of loops are not supported yet"; - (replace_breaks_with st1 st2).content - | _ -> super#visit_Sequence env st1 st2 + method! visit_statement env st = + match st.content with + | Sequence (st1, st2) -> begin + match st1.content with + | Loop _ -> + cassert __FILE__ __LINE__ + (statement_has_no_loop_break_continue st2) + st2.span "Sequences of loops are not supported yet"; + super#visit_statement env (replace_breaks_with st st2) + | Switch _ -> + (* This pushes st2 inside of the switch *) + super#visit_statement env (chain_statements st1 st2) + | _ -> super#visit_statement env st + end + | _ -> super#visit_statement env st end in (* Map *) let body = match f.body with - | Some body -> Some { body with body = obj#visit_statement () body.body } + | Some body -> + Some { body with body = replace_visitor#visit_statement () body.body } | None -> None in + let f = { f with body } in log#ldebug (lazy From 5f962ac8a0d0a0bf9113512e8287352f38ab14f4 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 10 Nov 2024 14:20:44 +0100 Subject: [PATCH 2/4] Update the Charon pin --- charon-pin | 2 +- flake.lock | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/charon-pin b/charon-pin index 71cfa8b5..0b08d20e 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -2193aa00fd89e991226ada10d8a8f66e0594f212 +0aeeccbc051a63963badfd635d13c79c2ecdf6d0 diff --git a/flake.lock b/flake.lock index d7353269..c8927663 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1730738130, - "narHash": "sha256-Gr81tQuo+IKZ87rMz1oMpJ+ccgGh7sAjQXe5jJsYWzc=", + "lastModified": 1731244776, + "narHash": "sha256-alkiHq7Di8N1Abjw7NAJ29s7ztcNCwIwVQmL/1vxUoM=", "owner": "aeneasverif", "repo": "charon", - "rev": "2193aa00fd89e991226ada10d8a8f66e0594f212", + "rev": "0aeeccbc051a63963badfd635d13c79c2ecdf6d0", "type": "github" }, "original": { @@ -285,11 +285,11 @@ ] }, "locked": { - "lastModified": 1730773675, - "narHash": "sha256-pULo7GryzLkqGveWvnNWVz1Kk6EJqvq+HQeSkwvr7DA=", + "lastModified": 1731119076, + "narHash": "sha256-2eVhmocCZHJlFAz6Mt3EwPdFFVAtGgIySJc1EHQVxcc=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "e19e9d54fac1e53f73411ebe22d19f946b1ba0bd", + "rev": "23c4b3ba5f806fcf25d5a3b6b54fa0d07854c032", "type": "github" }, "original": { From 5a54f85f14e6068932aa756d10788343bdbf81f6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 10 Nov 2024 14:39:21 +0100 Subject: [PATCH 3/4] Fix a bug in InterpreterLoopsMatchCtxs.match_ctxs --- compiler/InterpreterLoopsMatchCtxs.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 60429d8e..9a6d1a81 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -1410,9 +1410,13 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets) log#ldebug (lazy "match_abstractions: matching values"); let _ = - List.map - (fun (v0, v1) -> M.match_typed_avalues ctx0 ctx1 v0 v1) - (List.combine avalues0 avalues1) + if List.length avalues0 <> List.length avalues1 then + raise + (Distinct "Region abstractions with not the same number of values") + else + List.map + (fun (v0, v1) -> M.match_typed_avalues ctx0 ctx1 v0 v1) + (List.combine avalues0 avalues1) in log#ldebug (lazy "match_abstractions: values matched OK"); () From 5b1910e6631e8ff71caafb4eaaab488681f82dd6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 12 Nov 2024 17:10:52 +0100 Subject: [PATCH 4/4] Update the Charon pin --- charon-pin | 2 +- flake.lock | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/charon-pin b/charon-pin index 0b08d20e..eab4573a 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -0aeeccbc051a63963badfd635d13c79c2ecdf6d0 +5d2b6ceba0f5fb83f700baeea8d31df4027d06bf diff --git a/flake.lock b/flake.lock index c8927663..4e5755f8 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1731244776, - "narHash": "sha256-alkiHq7Di8N1Abjw7NAJ29s7ztcNCwIwVQmL/1vxUoM=", + "lastModified": 1731419532, + "narHash": "sha256-HamrvorfoYjSs0IEip6tch+lHk6x4/ai6aVaf6tXeHo=", "owner": "aeneasverif", "repo": "charon", - "rev": "0aeeccbc051a63963badfd635d13c79c2ecdf6d0", + "rev": "5d2b6ceba0f5fb83f700baeea8d31df4027d06bf", "type": "github" }, "original": { @@ -285,11 +285,11 @@ ] }, "locked": { - "lastModified": 1731119076, - "narHash": "sha256-2eVhmocCZHJlFAz6Mt3EwPdFFVAtGgIySJc1EHQVxcc=", + "lastModified": 1731378398, + "narHash": "sha256-a0QWaiX8+AJ9/XBLGMDy6c90GD7HzpxKVdlFwCke5Pw=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "23c4b3ba5f806fcf25d5a3b6b54fa0d07854c032", + "rev": "0ae9fc2f2fe5361837d59c0bdebbda176427111e", "type": "github" }, "original": {