Skip to content

Commit

Permalink
[asl] Iterate over possible values in domain.
Browse files Browse the repository at this point in the history
  • Loading branch information
@HadrienRenaud
HadrienRenaud committed Aug 5, 2024
1 parent 1dd0a7f commit dd3f528
Show file tree
Hide file tree
Showing 9 changed files with 184 additions and 127 deletions.
4 changes: 1 addition & 3 deletions asllib/tests/division.t/run.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
22 changes: 1 addition & 21 deletions asllib/tests/typing.t/TPositive4-1.asl
View file
Original file line number Diff line number Diff line change
@@ -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

19 changes: 1 addition & 18 deletions asllib/tests/typing.t/TPositive4-2.asl
View file
Original file line number Diff line number Diff line change
@@ -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

19 changes: 1 addition & 18 deletions asllib/tests/typing.t/TPositive4-3.asl
View file
Original file line number Diff line number Diff line change
@@ -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

17 changes: 0 additions & 17 deletions asllib/tests/typing.t/TPositive4-4.asl
View file
Original file line number Diff line number Diff line change
@@ -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

10 changes: 10 additions & 0 deletions asllib/tests/typing.t/TPositive4-5.asl
View file
Original file line number Diff line number Diff line change
@@ -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

22 changes: 1 addition & 21 deletions asllib/tests/typing.t/TPositive4.asl
View file
Original file line number Diff line number Diff line change
@@ -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

27 changes: 7 additions & 20 deletions asllib/tests/typing.t/run.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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:
Expand Down
Loading

0 comments on commit dd3f528

Please sign in to comment.