diff --git a/Makefile b/Makefile index 59bb561f..3a85d3c0 100644 --- a/Makefile +++ b/Makefile @@ -17,10 +17,10 @@ OPAM := opam LIT := lit # Control verbosity of testing -LIT_VERBOSITY = --succinct -# LIT_VERBOSITY = --verbose -DUNE_VERBOSITY = ALCOTEST_COMPACT=1 -# DUNE_VERBOSITY = +# LIT_VERBOSITY = --succinct +LIT_VERBOSITY = --verbose +# DUNE_VERBOSITY = ALCOTEST_COMPACT=1 +DUNE_VERBOSITY = build:: $(DUNE) build diff --git a/libASL/asl_fmt.ml b/libASL/asl_fmt.ml index 44a45895..5a1bce9c 100644 --- a/libASL/asl_fmt.ml +++ b/libASL/asl_fmt.ml @@ -226,7 +226,7 @@ let rec ty (fmt : PP.formatter) (x : AST.ty) : unit = | Type_Array (ixty, ety) -> kw_array fmt; nbsp fmt; - brackets fmt (fun _ -> ixtype fmt ixty); + ixtype fmt ixty; nbsp fmt; kw_of fmt; nbsp fmt; @@ -295,7 +295,7 @@ and change (fmt : PP.formatter) (x : AST.change) : unit = and ixtype (fmt : PP.formatter) (x : AST.ixtype) : unit = match x with | Index_Enum tc -> tycon fmt tc - | Index_Int sz -> expr fmt sz + | Index_Int sz -> brackets fmt (fun _ -> expr fmt sz) and expr (fmt : PP.formatter) (x : AST.expr) : unit = ( match x with diff --git a/libASL/asl_parser.messages b/libASL/asl_parser.messages index 5943d703..ea29d8f0 100644 --- a/libASL/asl_parser.messages +++ b/libASL/asl_parser.messages @@ -266,7 +266,7 @@ Malformed array type. The syntax of array types is "array [ ] of " or - "array [ ] of " + "array of " expr_command_start: ID AS ARRAY LBRACK WHILE ## @@ -1266,7 +1266,7 @@ Missing "]" in array type. The syntax of array types is "array [ ] of " or - "array [ ] of " + "array of " expr_command_start: ID AS ARRAY LBRACK BITSLIT RBRACK WHILE ## @@ -1282,7 +1282,7 @@ Missing "]" in array type. The syntax of array types is "array [ ] of " or - "array [ ] of " + "array of " expr_command_start: ID AS ARRAY LBRACK BITSLIT RBRACK OF WHILE ## @@ -1298,31 +1298,6 @@ Missing "of" in array type. The syntax of array types is "array [ $2 ] of " -expr_command_start: ID AS ARRAY LBRACK ID WHILE -## -## Ends in an error in state: 122. -## -## aexpr -> ident . [ XOR STAR SLASH REM RBRACK QUOT PLUS_PLUS PLUS OR MOD MINUS_MINUS_GT MINUS LT_MINUS_GT LT_LT LT_EQ LT LBRACK IN GT_GT GT_EQ GT EQ_EQ DOT DIVRM DIV CARET BAR_BAR BANG_EQ AS AND AMPERSAND_AMPERSAND ] -## aexpr -> ident . LPAREN loption(separated_nonempty_list(COMMA,arg)) RPAREN throws [ XOR STAR SLASH REM RBRACK QUOT PLUS_PLUS PLUS OR MOD MINUS_MINUS_GT MINUS LT_MINUS_GT LT_LT LT_EQ LT LBRACK IN GT_GT GT_EQ GT EQ_EQ DOT DIVRM DIV CARET BAR_BAR BANG_EQ AS AND AMPERSAND_AMPERSAND ] -## aexpr -> ident . QUERY LPAREN loption(separated_nonempty_list(COMMA,arg)) RPAREN [ XOR STAR SLASH REM RBRACK QUOT PLUS_PLUS PLUS OR MOD MINUS_MINUS_GT MINUS LT_MINUS_GT LT_LT LT_EQ LT LBRACK IN GT_GT GT_EQ GT EQ_EQ DOT DIVRM DIV CARET BAR_BAR BANG_EQ AS AND AMPERSAND_AMPERSAND ] -## aexpr -> ident . LPAREN loption(separated_nonempty_list(COMMA,arg)) RPAREN LBRACE separated_nonempty_list(COMMA,field_assignment) RBRACE [ XOR STAR SLASH REM RBRACK QUOT PLUS_PLUS PLUS OR MOD MINUS_MINUS_GT MINUS LT_MINUS_GT LT_LT LT_EQ LT LBRACK IN GT_GT GT_EQ GT EQ_EQ DOT DIVRM DIV CARET BAR_BAR BANG_EQ AS AND AMPERSAND_AMPERSAND ] -## aexpr -> ident . LBRACE separated_nonempty_list(COMMA,field_assignment) RBRACE [ XOR STAR SLASH REM RBRACK QUOT PLUS_PLUS PLUS OR MOD MINUS_MINUS_GT MINUS LT_MINUS_GT LT_LT LT_EQ LT LBRACK IN GT_GT GT_EQ GT EQ_EQ DOT DIVRM DIV CARET BAR_BAR BANG_EQ AS AND AMPERSAND_AMPERSAND ] -## ixtype -> ident . [ RBRACK ] -## -## The known suffix of the stack is as follows: -## ident -## - -Malformed expression starting with identifier. -The syntax of expressions that start with an identifier is - "$0" - variable read or call getter function -or - "$0()" - function call -or - "$0{}" - record expression -or - "$0(){}" - record expression - expr_command_start: LBRACK ID COMMA ID RPAREN ## ## Ends in an error in state: 197. diff --git a/libASL/asl_parser.mly b/libASL/asl_parser.mly index 9ef04223..74ceaa11 100644 --- a/libASL/asl_parser.mly +++ b/libASL/asl_parser.mly @@ -236,7 +236,7 @@ variable_declaration: { Decl_Const(v, ty, e, Range($symbolstartpos, $endpos)) } ixtype: -| ident = ident { Index_Enum(ident) } +| TYPE ident = ident { Index_Enum(ident) } | expr = expr { Index_Int(expr) } throws: diff --git a/libASL/tcheck.ml b/libASL/tcheck.ml index e6f98a3d..37067cc0 100644 --- a/libASL/tcheck.ml +++ b/libASL/tcheck.ml @@ -1072,6 +1072,9 @@ let rec synthesize_type | Type_Constructor (tc1, es1), Type_Constructor (tc2, es2) when tc1 = tc2 -> assert (List.length es1 = List.length es2); List.iter2 (synthesize_equality s) es1 es2 + | Type_Array (Index_Int n1, elty1), Type_Array (Index_Int n2, elty2) -> + synthesize_equality s n1 n2; + synthesize_type env loc s elty1 elty2 | Type_Array (_, elty1), Type_Array (_, elty2) -> synthesize_type env loc s elty1 elty2 | Type_Tuple tys1, Type_Tuple tys2 -> diff --git a/tests/asl_test.ml b/tests/asl_test.ml index f95a0301..8e8ef02e 100644 --- a/tests/asl_test.ml +++ b/tests/asl_test.ml @@ -236,7 +236,7 @@ let tests : unit Alcotest.test_case list = var (h : integer, i : boolean) = (1, TRUE); var (j : integer, - : boolean) = (1, TRUE); var arr1 : array [8] of integer; - var arr2 : array [boolean] of integer; + var arr2 : array [type boolean] of integer; let m : bits(8*N) = UNKNOWN : bits(8*N); let n : bits(8*N) = Zeros(8*N); diff --git a/tests/lit/tcheck/array_param_00.asl b/tests/lit/tcheck/array_param_00.asl new file mode 100644 index 00000000..a9fad497 --- /dev/null +++ b/tests/lit/tcheck/array_param_00.asl @@ -0,0 +1,17 @@ +// RUN: %asli --batchmode %s +// Copyright (C) 2025-2025 Intel Corporation + +func F(x : array [size] of integer) => integer +begin + var sum = 0; + for i = 0 to size-1 do + sum = sum + x[i]; + end + return sum; +end + +func main() => integer +begin + let x : integer = (F(array (1,2,3))); + let y : integer = (F(array (1))); +end