From 2c4eeaaaa631c4aa8f7925abb227112886d03313 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Wed, 4 Oct 2023 13:44:28 -0500 Subject: [PATCH 1/3] Abstract interpretation int range fixes --- src/lustre/lustreAbstractInterpretation.ml | 52 +++++++++++++++------- 1 file changed, 37 insertions(+), 15 deletions(-) diff --git a/src/lustre/lustreAbstractInterpretation.ml b/src/lustre/lustreAbstractInterpretation.ml index cadc1bc6f..c0bfc88b2 100644 --- a/src/lustre/lustreAbstractInterpretation.ml +++ b/src/lustre/lustreAbstractInterpretation.ml @@ -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 @@ -381,28 +385,46 @@ 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 + | IntRange (pos, None, None) -> Int pos | 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 From 73bb7a282ecba0fa84b5650176f526c4acd859a6 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Wed, 4 Oct 2023 13:47:19 -0500 Subject: [PATCH 2/3] Remove unused pattern match --- src/lustre/lustreAbstractInterpretation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lustre/lustreAbstractInterpretation.ml b/src/lustre/lustreAbstractInterpretation.ml index c0bfc88b2..64dd35606 100644 --- a/src/lustre/lustreAbstractInterpretation.ml +++ b/src/lustre/lustreAbstractInterpretation.ml @@ -419,7 +419,7 @@ and interpret_expr_by_type node_id ctx ty_ctx ty proj expr : LA.lustre_type = subrange_from_upper r | _ -> t) | IntRange (pos, None, None) -> Int pos - | Int _ | IntRange _ -> + | Int _ -> 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 From 51aef99f64ec78ee1a8a61f639406df059a8bff2 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Thu, 5 Oct 2023 11:28:49 -0500 Subject: [PATCH 3/3] Fix IntRange type without bounds in interpret_expr_by_type --- src/lustre/lustreAbstractInterpretation.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/lustre/lustreAbstractInterpretation.ml b/src/lustre/lustreAbstractInterpretation.ml index 64dd35606..91cec3ffa 100644 --- a/src/lustre/lustreAbstractInterpretation.ml +++ b/src/lustre/lustreAbstractInterpretation.ml @@ -418,8 +418,7 @@ and interpret_expr_by_type node_id ctx ty_ctx ty proj expr : LA.lustre_type = let r = Numeral.min r1 r2 in subrange_from_upper r | _ -> t) - | IntRange (pos, None, None) -> Int pos - | Int _ -> + | 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