From dd3f528d1a3bbda778136e9467b4d4da677e2f47 Mon Sep 17 00:00:00 2001 From: Hadrien Renaud Date: Thu, 1 Aug 2024 18:56:44 +0100 Subject: [PATCH] [asl] Iterate over possible values in domain. --- asllib/tests/division.t/run.t | 4 +- asllib/tests/typing.t/TPositive4-1.asl | 22 +--- asllib/tests/typing.t/TPositive4-2.asl | 19 +-- asllib/tests/typing.t/TPositive4-3.asl | 19 +-- asllib/tests/typing.t/TPositive4-4.asl | 17 --- asllib/tests/typing.t/TPositive4-5.asl | 10 ++ asllib/tests/typing.t/TPositive4.asl | 22 +--- asllib/tests/typing.t/run.t | 27 +--- asllib/types.ml | 171 +++++++++++++++++++++++-- 9 files changed, 184 insertions(+), 127 deletions(-) create mode 100644 asllib/tests/typing.t/TPositive4-5.asl diff --git a/asllib/tests/division.t/run.t b/asllib/tests/division.t/run.t index 9b5762a6c3..6fbc353cbc 100644 --- a/asllib/tests/division.t/run.t +++ b/asllib/tests/division.t/run.t @@ -108,9 +108,7 @@ Example with constant: Other example from typing.t: $ aslref --no-exec TNegative9-1.asl - File TNegative9-1.asl, line 3, characters 4 to 59: - ASL Typing error: a subtype of bits(N) was expected, - provided bits((N * (3 DIV 4))). + ASL Static error: Illegal application of operator DIV for values 3 and 4. [1] $ aslref --no-exec TPositive9.asl diff --git a/asllib/tests/typing.t/TPositive4-1.asl b/asllib/tests/typing.t/TPositive4-1.asl index 4c2a5b3e7e..2c44f40cb7 100644 --- a/asllib/tests/typing.t/TPositive4-1.asl +++ b/asllib/tests/typing.t/TPositive4-1.asl @@ -1,27 +1,7 @@ -func foo () => integer {8, 16} -begin return 8; end - -let LET_ALLOWED_NUMS_A = 8; let LET_ALLOWED_NUMS_B : integer {8,16} = 8; -let LET_ALLOWED_NUMS_C : integer {8,16} = foo(); -constant CONST_ALLOWED_NUMS : integer {8,16} = 8; -// config CONFIG_ALLOWED_NUMS : integer {8,16} = foo(); -var VAR_ALLOWED_NUMS : integer {8} = 8; func positive4() begin - let testA : integer {LET_ALLOWED_NUMS_A} = 8; // NOTE its the type of LET_ALLOWED_NUMS_A (ie integer {8}) NOT its value that's - // used to determine the demain of testA - // let testB : integer {LET_ALLOWED_NUMS_B} = 16; // This is valid as testB is of type integer {8,16}, NOT integer {8} - let testC : integer {LET_ALLOWED_NUMS_C} = 16; // This is valid as testC is of type integer {8,16}, regardless of what foo() - // returns - - // testD is of type integer {0..16} because this is the union of integer {0..8} and integer {0..16} - let testD : integer {0..LET_ALLOWED_NUMS_C} = 3; - let testE : integer {0..16} = testD; - - // configs can also be used and follow the same rules as lets - let testF : integer {CONFIG_ALLOWED_NUMS} = 16; - let testG : integer {0..CONFIG_ALLOWED_NUMS} = 3; + let testB : integer {LET_ALLOWED_NUMS_B} = 16; end diff --git a/asllib/tests/typing.t/TPositive4-2.asl b/asllib/tests/typing.t/TPositive4-2.asl index d1f77957f6..9141b98f4d 100644 --- a/asllib/tests/typing.t/TPositive4-2.asl +++ b/asllib/tests/typing.t/TPositive4-2.asl @@ -1,27 +1,10 @@ func foo () => integer {8, 16} begin return 8; end -let LET_ALLOWED_NUMS_A = 8; -let LET_ALLOWED_NUMS_B : integer {8,16} = 8; let LET_ALLOWED_NUMS_C : integer {8,16} = foo(); -constant CONST_ALLOWED_NUMS : integer {8,16} = 8; -// config CONFIG_ALLOWED_NUMS : integer {8,16} = foo(); -var VAR_ALLOWED_NUMS : integer {8} = 8; func positive4() begin - let testA : integer {LET_ALLOWED_NUMS_A} = 8; // NOTE its the type of LET_ALLOWED_NUMS_A (ie integer {8}) NOT its value that's - // used to determine the demain of testA - // let testB : integer {LET_ALLOWED_NUMS_B} = 16; // This is valid as testB is of type integer {8,16}, NOT integer {8} - // let testC : integer {LET_ALLOWED_NUMS_C} = 16; // This is valid as testC is of type integer {8,16}, regardless of what foo() - // returns - - // testD is of type integer {0..16} because this is the union of integer {0..8} and integer {0..16} - let testD : integer {0..LET_ALLOWED_NUMS_C} = 3; - let testE : integer {0..16} = testD; - - // configs can also be used and follow the same rules as lets - let testF : integer {CONFIG_ALLOWED_NUMS} = 16; - let testG : integer {0..CONFIG_ALLOWED_NUMS} = 3; + let testC : integer {LET_ALLOWED_NUMS_C} = 16; end diff --git a/asllib/tests/typing.t/TPositive4-3.asl b/asllib/tests/typing.t/TPositive4-3.asl index 9eefc5d5fe..64be5cc3d6 100644 --- a/asllib/tests/typing.t/TPositive4-3.asl +++ b/asllib/tests/typing.t/TPositive4-3.asl @@ -1,28 +1,11 @@ func foo () => integer {8, 16} begin return 8; end -let LET_ALLOWED_NUMS_A = 8; -let LET_ALLOWED_NUMS_B : integer {8,16} = 8; let LET_ALLOWED_NUMS_C : integer {8,16} = foo(); -constant CONST_ALLOWED_NUMS : integer {8,16} = 8; -// config CONFIG_ALLOWED_NUMS : integer {8,16} = foo(); -var VAR_ALLOWED_NUMS : integer {8} = 8; func positive4() begin - let testA : integer {LET_ALLOWED_NUMS_A} = 8; // NOTE its the type of LET_ALLOWED_NUMS_A (ie integer {8}) NOT its value that's - // used to determine the demain of testA - // let testB : integer {LET_ALLOWED_NUMS_B} = 16; // This is valid as testB is of type integer {8,16}, NOT integer {8} - // let testC : integer {LET_ALLOWED_NUMS_C} = 16; // This is valid as testC is of type integer {8,16}, regardless of what foo() - // returns - - // testD is of type integer {0..16} because this is the union of integer {0..8} and integer {0..16} - // let testD : integer {0..LET_ALLOWED_NUMS_C} = 3; - let testD : integer {0..LET_ALLOWED_NUMS_C} = UNKNOWN: integer {0..LET_ALLOWED_NUMS_C}; + let testD : integer {0..LET_ALLOWED_NUMS_C} = 3; let testE : integer {0..16} = testD; - - // configs can also be used and follow the same rules as lets - let testF : integer {CONFIG_ALLOWED_NUMS} = 16; - let testG : integer {0..CONFIG_ALLOWED_NUMS} = 3; end diff --git a/asllib/tests/typing.t/TPositive4-4.asl b/asllib/tests/typing.t/TPositive4-4.asl index 217f5a648d..f97da1dca7 100644 --- a/asllib/tests/typing.t/TPositive4-4.asl +++ b/asllib/tests/typing.t/TPositive4-4.asl @@ -1,28 +1,11 @@ func foo () => integer {8, 16} begin return 8; end -let LET_ALLOWED_NUMS_A = 8; -let LET_ALLOWED_NUMS_B : integer {8,16} = 8; -let LET_ALLOWED_NUMS_C : integer {8,16} = foo(); -constant CONST_ALLOWED_NUMS : integer {8,16} = 8; config CONFIG_ALLOWED_NUMS : integer {8,16} = foo(); -var VAR_ALLOWED_NUMS : integer {8} = 8; func positive4() begin - let testA : integer {LET_ALLOWED_NUMS_A} = 8; // NOTE its the type of LET_ALLOWED_NUMS_A (ie integer {8}) NOT its value that's - // used to determine the demain of testA - // let testB : integer {LET_ALLOWED_NUMS_B} = 16; // This is valid as testB is of type integer {8,16}, NOT integer {8} - // let testC : integer {LET_ALLOWED_NUMS_C} = 16; // This is valid as testC is of type integer {8,16}, regardless of what foo() - // returns - - // testD is of type integer {0..16} because this is the union of integer {0..8} and integer {0..16} - // let testD : integer {0..LET_ALLOWED_NUMS_C} = 3; - // let testD : integer {0..LET_ALLOWED_NUMS_C} = UNKNOWN: integer {0..LET_ALLOWED_NUMS_C}; - // let testE : integer {0..16} = testD; - // configs can also be used and follow the same rules as lets let testF : integer {CONFIG_ALLOWED_NUMS} = 16; - let testG : integer {0..CONFIG_ALLOWED_NUMS} = 3; end diff --git a/asllib/tests/typing.t/TPositive4-5.asl b/asllib/tests/typing.t/TPositive4-5.asl new file mode 100644 index 0000000000..3639f7d3ce --- /dev/null +++ b/asllib/tests/typing.t/TPositive4-5.asl @@ -0,0 +1,10 @@ +func foo () => integer {8, 16} +begin return 8; end + +config CONFIG_ALLOWED_NUMS : integer {8,16} = foo(); + +func positive4() +begin + let testG : integer {0..CONFIG_ALLOWED_NUMS} = 3; +end + diff --git a/asllib/tests/typing.t/TPositive4.asl b/asllib/tests/typing.t/TPositive4.asl index e274a0ea2f..9caaa6a20d 100644 --- a/asllib/tests/typing.t/TPositive4.asl +++ b/asllib/tests/typing.t/TPositive4.asl @@ -1,27 +1,7 @@ -func foo () => integer {8, 16} -begin return 8; end - let LET_ALLOWED_NUMS_A = 8; -let LET_ALLOWED_NUMS_B : integer {8,16} = 8; -let LET_ALLOWED_NUMS_C : integer {8,16} = foo(); -constant CONST_ALLOWED_NUMS : integer {8,16} = 8; -config CONFIG_ALLOWED_NUMS : integer {8,16} = foo(); -var VAR_ALLOWED_NUMS : integer {8} = 8; func positive4() begin - let testA : integer {LET_ALLOWED_NUMS_A} = 8; // NOTE its the type of LET_ALLOWED_NUMS_A (ie integer {8}) NOT its value that's - // used to determine the demain of testA - let testB : integer {LET_ALLOWED_NUMS_B} = 16; // This is valid as testB is of type integer {8,16}, NOT integer {8} - let testC : integer {LET_ALLOWED_NUMS_C} = 16; // This is valid as testC is of type integer {8,16}, regardless of what foo() - // returns - - // testD is of type integer {0..16} because this is the union of integer {0..8} and integer {0..16} - let testD : integer {0..LET_ALLOWED_NUMS_C} = 3; - let testE : integer {0..16} = testD; - - // configs can also be used and follow the same rules as lets - let testF : integer {CONFIG_ALLOWED_NUMS} = 16; - let testG : integer {0..CONFIG_ALLOWED_NUMS} = 3; + let testA : integer {LET_ALLOWED_NUMS_A} = 8; end diff --git a/asllib/tests/typing.t/run.t b/asllib/tests/typing.t/run.t index addbd305b4..4752906c7d 100644 --- a/asllib/tests/typing.t/run.t +++ b/asllib/tests/typing.t/run.t @@ -41,30 +41,23 @@ Propagation of constrained integers Use of global vars in constraints $ aslref --no-exec TPositive4.asl - File TPositive4.asl, line 15, characters 4 to 54: + $ aslref --no-exec TPositive4-1.asl + File TPositive4-1.asl, line 5, characters 4 to 54: ASL Typing error: a subtype of integer {8} was expected, provided integer {16}. [1] - $ aslref --no-exec TPositive4-1.asl - File TPositive4-1.asl, line 16, characters 4 to 54: + $ aslref --no-exec TPositive4-2.asl + File TPositive4-2.asl, line 8, characters 4 to 54: ASL Typing error: a subtype of integer {LET_ALLOWED_NUMS_C} was expected, provided integer {16}. [1] - $ aslref --no-exec TPositive4-2.asl - File TPositive4-2.asl, line 20, characters 4 to 53: - ASL Typing error: a subtype of integer {0..LET_ALLOWED_NUMS_C} was expected, - provided integer {3}. - [1] $ aslref --no-exec TPositive4-3.asl - File TPositive4-3.asl, line 22, characters 4 to 57: - ASL Typing error: a subtype of integer {0..16} was expected, - provided integer {0..LET_ALLOWED_NUMS_C}. - [1] $ aslref --no-exec TPositive4-4.asl - File TPositive4-4.asl, line 25, characters 4 to 54: + File TPositive4-4.asl, line 9, characters 4 to 54: ASL Typing error: a subtype of integer {CONFIG_ALLOWED_NUMS} was expected, provided integer {16}. [1] + $ aslref --no-exec TPositive4-5.asl $ aslref --no-exec TReconsider4-0.asl File TReconsider4-0.asl, line 13, characters 4 to 54: ASL Typing error: a subtype of integer {8} was expected, @@ -111,10 +104,6 @@ Named types Loops $ aslref --no-exec TPositive8.asl - File TPositive8.asl, line 16, characters 8 to 40: - ASL Typing error: a subtype of integer {0..15} was expected, - provided integer {0..N}. - [1] $ aslref --no-exec TPositive8-1.asl File TPositive8-1.asl, line 5, characters 8 to 40: ASL Typing error: a subtype of integer {8..31} was expected, @@ -147,9 +136,7 @@ Bit vector widths defined by constrained integers ASL Typing error: a subtype of bits(8) was expected, provided bits(16). [1] $ aslref --no-exec TNegative9-1.asl - File TNegative9-1.asl, line 3, characters 4 to 59: - ASL Typing error: a subtype of bits(N) was expected, - provided bits((N * (3 DIV 4))). + ASL Static error: Illegal application of operator DIV for values 3 and 4. [1] $ aslref --no-exec TNegative9-2.asl File TNegative9-2.asl, line 3, characters 4 to 35: diff --git a/asllib/types.ml b/asllib/types.ml index 60dd4cc245..cd498ce0c0 100644 --- a/asllib/types.ml +++ b/asllib/types.ml @@ -296,11 +296,9 @@ module Domain = struct match e.desc with | E_Literal v -> of_literal v | E_Var x -> ( - try StaticEnv.lookup_constants env x |> of_literal + try SEnv.lookup_constants env x |> of_literal with Not_found -> ( - try - let ty = StaticEnv.type_of env x in - of_type env ty + try SEnv.type_of env x |> of_type env with Not_found -> Error.fatal_from e (Error.UndefinedIdentifier x))) | E_Unop (NEG, e') -> of_expr env (E_Binop (MINUS, !$0, e') |> add_pos_from e) @@ -375,17 +373,172 @@ module Domain = struct let compare _d1 _d2 = assert false - let syntax_is_subset env is1 is2 = - (* TODO: improve for basic cases. *) - constraints_equal env is1 is2 + module Iterators = struct + type approx = Over | Under + + exception CannotOverApproximate + + let assert_under approx acc = + if approx = Over then raise CannotOverApproximate else acc + + let fold_zs = + let rec aux f z1 z2 acc = + if Z.lt z2 z1 then acc else f z1 acc |> aux f (Z.succ z1) z2 + in + fun f z1 z2 acc -> + if Z.equal z1 z2 then f z1 acc + else acc |> f z1 |> f z2 |> aux f (Z.succ z1) (Z.pred z2) + + let rec expr_fold : + 'acc. _ -> _ -> (literal -> 'acc -> 'acc) -> _ -> 'acc -> 'acc = + fun approx env f e acc -> + let e = StaticModel.try_normalize env e in + match e.desc with + | E_Literal l -> f l acc + | E_Var x -> + if approx = Over then + let t = try SEnv.type_of env x with Not_found -> assert false in + type_fold Over env f t acc + else acc + | E_Unop (op, e) -> + let f' z = Operations.unop_values e Error.Static op z |> f in + expr_fold approx env f' e acc + | E_Binop (op, e1, e2) -> + let f1 z2 z1 = Operations.binop_values e Error.Static op z1 z2 |> f in + let f2 z2 = expr_fold approx env (f1 z2) e1 in + expr_fold approx env f2 e2 acc + | E_Unknown t -> type_fold approx env f t acc + | E_Cond (e1, e2, e3) -> + let f' = function + | L_Bool b -> expr_fold approx env f (if b then e2 else e3) + | _ -> + assert false (* Type error - should have been caught earlier. *) + in + expr_fold approx env f' e1 acc + | E_GetArray _ | E_GetField _ | E_GetFields _ | E_GetItem _ | E_Record _ + | E_Tuple _ -> + (* Not supported: aggregate types. *) + assert_under approx acc + | E_ATC (_, _) + | E_Slice (_, _) + | E_Pattern (_, _) + | E_Call (_, _, _) + | E_Concat _ -> + (* Not yet implemented *) + assert_under approx acc + + and type_fold : + 'acc. _ -> _ -> (literal -> 'acc -> 'acc) -> _ -> 'acc -> 'acc = + fun approx env f t acc -> + let t = make_anonymous env t in + match t.desc with + | T_Real | T_String | T_Int (UnConstrained | UnderConstrained _) -> + assert_under approx acc (* We can't iterate on all of those. *) + | T_Int (WellConstrained cs) -> constraints_fold approx env f cs acc + | T_Bool -> acc |> f (L_Bool true) |> f (L_Bool false) + | T_Bits (e_len, _) -> + let f1 length z = L_BitVector (Bitvector.of_z length z) |> f in + let f2 = function + | L_Int z when Z.fits_int z && Z.sign z >= 0 -> + let length = Z.to_int z in + let max = Z.shift_left Z.one length |> Z.pred in + fold_zs (f1 length) Z.zero max + | L_Int _ -> Fun.id (* Those are delayed until runtime. *) + | _ -> assert false (* Type error. *) + in + expr_fold approx env f2 e_len acc + | T_Enum li -> + List.fold_left + (fun acc x -> + expr_fold approx env f (E_Var x |> add_pos_from t) acc) + acc li + | T_Tuple _ | T_Array (_, _) | T_Record _ | T_Exception _ -> + (* Non supported: aggregate types. *) + assert_under approx acc + | T_Named _ -> assert false (* Error in output of [make_anonmymous]. *) + + and constraint_fold : + 'acc. _ -> _ -> (literal -> 'acc -> 'acc) -> _ -> 'acc -> 'acc = + fun approx env f c acc -> + match c with + | Constraint_Exact e -> expr_fold approx env f e acc + | Constraint_Range (e1, e2) -> + let z1, z2 = + match approx with + | Over -> (get_min env e1, get_max env e2) + | Under -> (get_max env e1, get_min env e2) + in + let f z = f (L_Int z) in + fold_zs f z1 z2 acc + + and constraints_fold : + 'acc. _ -> _ -> (literal -> 'acc -> 'acc) -> _ -> 'acc -> 'acc = + fun approx env f li acc -> + List.fold_left (fun acc c -> constraint_fold approx env f c acc) acc li + + and get_min env e = + expr_fold Over env + (function L_Int z1 -> Z.min z1 | _ -> assert false) + e + Z.(shift_left one 30) + + and get_max env e = + expr_fold Over env + (function L_Int z1 -> Z.max z1 | _ -> assert false) + e + Z.(shift_left minus_one 30) + + let constraints_for_all env is f = + let exception FalseFound in + let f' l _acc = f l || raise FalseFound in + try constraints_fold Over env f' is true + with CannotOverApproximate | FalseFound -> false + + let constraints_exists env is f = + let exception TrueFound in + let f' l _acc = f l && raise TrueFound in + try constraints_fold Under env f' is false with + | CannotOverApproximate -> false + | TrueFound -> true + end + + let int_set_for_all = + let interval_iter elt_iter interval = + let x = IntSet.Interval.x interval and y = IntSet.Interval.y interval in + (* We try the extremities first, in case it's linear. *) + elt_iter x; + elt_iter y; + let n = Z.(sub y x |> to_int) in + for i = 0 to n do + Z.of_int i |> Z.add x |> elt_iter + done + in + let exception FalseFound in + fun is f -> + let elt_iter z = if f z then () else raise FalseFound in + try + IntSet.iter (interval_iter elt_iter) is; + true + with FalseFound -> false let int_set_is_subset env is1 is2 = match (is1, is2) with | _, Top -> true | Top, _ -> false | Finite is1, Finite is2 -> IntSet.(is_empty (diff is1 is2)) - | FromSyntax is1, FromSyntax is2 -> syntax_is_subset env is1 is2 - | _ -> false + | FromSyntax is1, FromSyntax is2 -> + constraints_equal env is1 is2 + || Iterators.constraints_for_all env is1 @@ fun l1 -> + Iterators.constraints_exists env is2 @@ fun l2 -> literal_equal l1 l2 + | Finite is1, FromSyntax is2 -> ( + int_set_for_all is1 @@ fun z1 -> + Iterators.constraints_exists env is2 @@ function + | L_Int z2 -> Z.equal z1 z2 + | _ -> false) + | FromSyntax is1, Finite is2 -> ( + Iterators.constraints_for_all env is1 @@ function + | L_Int z1 -> IntSet.mem z1 is2 + | _ -> false) let is_subset env d1 d2 = let () =