Skip to content
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

Update LlbcAstUtils.chain_statements #458

Merged
merged 2 commits into from
Nov 12, 2024
Merged

Update LlbcAstUtils.chain_statements #458

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9adb7b9
Update LlbcAstUtils.chain_statements
sonmarcho Nov 10, 2024
0aeeccb
Add Meta.safe_combine_span to Charon-ML
sonmarcho Nov 10, 2024
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
12 changes: 4 additions & 8 deletions charon-ml/src/LlbcAstUtils.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ let fun_decl_has_loops (fd : fun_decl) : bool =

(** Create a sequence *)
let mk_sequence (st1 : statement) (st2 : statement) : statement =
let span = MetaUtils.combine_span st1.span st2.span in
let span = MetaUtils.safe_combine_span st1.span st2.span in
let content = Sequence (st1, st2) in
{ span; content; comments_before = [] }

Expand All @@ -58,9 +58,9 @@ let rec chain_statements (st1 : statement) (st2 : statement) : statement =
(* Ignore the second statement, which won't be evaluated *) st1
| Switch switch ->
(* Insert inside the switch *)
let span = MetaUtils.combine_span st1.span st2.span in
let span = MetaUtils.safe_combine_span st1.span st2.span in
let content = Switch (chain_statements_in_switch switch st2) in
{ span; content; comments_before = [] }
{ span; content; comments_before = st1.comments_before }
| Sequence (st3, st4) ->
(* Insert at the end of the statement *)
mk_sequence st3 (chain_statements st4 st2)
Expand All @@ -79,11 +79,7 @@ and chain_statements_in_switch (switch : switch) (st : statement) : switch =
let branches =
List.map (fun (svl, br) -> (svl, chain_statements br st)) branches
in
let otherwise =
match otherwise with
| None -> None
| Some otherwise -> Some (chain_statements otherwise st)
in
let otherwise = Option.map (fun b -> chain_statements b st) otherwise in
Match (op, branches, otherwise)

(** Compute a map from function declaration ids to declaration groups. *)
Expand Down
26 changes: 16 additions & 10 deletions charon-ml/src/MetaUtils.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,19 @@ let loc_max (l0 : loc) (l1 : loc) : loc =
else l1

(** See the comments in [meta_utils.rs] in Charon. *)
let combine_span (m0 : span) (m1 : span) : span =
assert (m0.span.file = m1.span.file);
let span =
{
file = m0.span.file;
beg_loc = loc_min m0.span.beg_loc m1.span.beg_loc;
end_loc = loc_max m0.span.end_loc m1.span.end_loc;
}
in
{ span; generated_from_span = None }
let combine_span (m0 : span) (m1 : span) : span option =
if m0.span.file = m1.span.file then
let span =
{
file = m0.span.file;
beg_loc = loc_min m0.span.beg_loc m1.span.beg_loc;
end_loc = loc_max m0.span.end_loc m1.span.end_loc;
}
in
Some { span; generated_from_span = None }
else None

(** Safely combine two spans, even if they do not come from the same file -
if this happens, we simply use the first span. *)
let safe_combine_span (m0 : span) (m1 : span) : span =
match combine_span m0 m1 with None -> m0 | Some m -> m
Loading