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

Abstract interpretation int range fixes #1017

Merged
merged 3 commits into from
Oct 5, 2023
Merged

Abstract interpretation int range fixes #1017

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2c4eeaa
Abstract interpretation int range fixes
lorchrob Oct 4, 2023
73bb7a2
Remove unused pattern match
lorchrob Oct 4, 2023
51aef99
Fix IntRange type without bounds in interpret_expr_by_type
daniel-larraz Oct 5, 2023
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
51 changes: 36 additions & 15 deletions src/lustre/lustreAbstractInterpretation.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -151,26 +151,30 @@ let rec restrict_type_by ty restrict = match ty, restrict with
| (Some Const (_, Num l1)), (Some Const (_, Num l2)) ->
let l1 = Numeral.of_string (HString.string_of_hstring l1) in
let l2 = Numeral.of_string (HString.string_of_hstring l2) in
let lnum = Numeral.min l1 l2 in
let lnum = Numeral.max l1 l2 in
let l = HString.mk_hstring (Numeral.string_of_numeral lnum) in
Some (LA.Const (dpos, Num l)), not (Numeral.equal l1 lnum)
| Some _, None -> None, true
| _ -> None, false
| (Some _ as l), None -> l, false
| None, (Some _ as l) -> l, true
| _ -> None, false

in
let upper, is_restricted2 = match u1, u2 with
| (Some Const (_, Num u1)), (Some Const (_, Num u2)) ->
let u1 = Numeral.of_string (HString.string_of_hstring u1) in
let u2 = Numeral.of_string (HString.string_of_hstring u2) in
let unum = Numeral.max u1 u2 in
let unum = Numeral.min u1 u2 in
let u = HString.mk_hstring (Numeral.string_of_numeral unum) in
Some (LA.Const (dpos, Num u)), not (Numeral.equal u1 unum)
| Some _, None -> None, true
| _ -> None, false
| (Some _ as u), None -> u, false
| None, (Some _ as u) -> u, true
| _ -> None, false
in
(*IntRange (dpos, lower, upper)*)
let is_restricted = is_restricted1 || is_restricted2 in
IntRange (dpos, lower, upper), is_restricted
if (lower = None && upper = None)
then Int dpos, is_restricted
else IntRange (dpos, lower, upper), is_restricted
| IntRange _ as t, Int _ -> t, false
| Int _, (IntRange _ as t) -> t, true
| t, _ -> t, false
Expand Down Expand Up @@ -381,28 +385,45 @@ and interpret_expr_by_type node_id ctx ty_ctx ty proj expr : LA.lustre_type =
| Some l2, Some r2 ->
let l, r = Numeral.max l1 l2, Numeral.min r1 r2 in
subrange_from_bounds l r
| Some l2, None ->
let l = Numeral.max l1 l2 in
subrange_from_bounds l r1
| None, Some r2 ->
let r = Numeral.min r1 r2 in
subrange_from_bounds l1 r
| _ -> t)
| IntRange (_, (Some Const (_, Num l1)), None) as t ->
let l1 = Numeral.of_string (HString.string_of_hstring l1) in
let l2, _ = interpret_int_expr node_id ctx ty_ctx proj expr in
(match l2 with
| Some l2 ->
let l = Numeral.max l1 l2 in
let l2, r2 = interpret_int_expr node_id ctx ty_ctx proj expr in
(match l2, r2 with
| Some l2, Some r2 ->
let l = Numeral.max l1 l2 in
subrange_from_bounds l r2
| Some l2, None ->
let l = Numeral.max l1 l2 in
subrange_from_lower l
| None, Some r2 ->
subrange_from_bounds l1 r2
| _ -> t)
| IntRange (_, None, (Some Const (_, Num r1))) as t ->
let r1 = Numeral.of_string (HString.string_of_hstring r1) in
let _, r2 = interpret_int_expr node_id ctx ty_ctx proj expr in
(match r2 with
| Some r2 ->
let l2, r2 = interpret_int_expr node_id ctx ty_ctx proj expr in
(match l2, r2 with
| Some l2, Some r2 ->
let r = Numeral.min r1 r2 in
subrange_from_bounds l2 r
| Some l2, None ->
subrange_from_bounds l2 r1
| None, Some r2 ->
let r = Numeral.min r1 r2 in
subrange_from_upper r
| _ -> t)
| IntRange (_, None, None) as t -> t
| Int _ | IntRange _ ->
let l, r = interpret_int_expr node_id ctx ty_ctx proj expr in
(match l, r with
| Some l, Some r -> subrange_from_bounds l r
| Some l, None -> subrange_from_lower l
| None, Some r -> subrange_from_upper r
| _ -> LA.Int dpos)
| t -> t

Expand Down