Merge pull request #1013 from daniel-larraz/const-expr-checks

Fix type-checking of constant expressions

src/lustre/lustreNodeGen.ml

@@ -665,7 +665,7 @@ and compile_ast_type
     (* Old code does flattening here, but that flattening is only ever used
       once! And it is for a check, in lustreDeclarations line 423 *)
     if expand then
-      let upper = E.numeral_of_expr array_size in
+      let upper = Numeral.(max zero (E.numeral_of_expr array_size)) in
       let result = ref X.empty in
       for ix = 0 to (Numeral.to_int upper - 1) do
         result := X.fold
@@ -681,8 +681,11 @@ and compile_ast_type
     else
       let over_element_type j t a = X.add
         (j @ [X.ArrayVarIndex array_size])
-        (Type.mk_array t (if E.is_numeral array_size
-          then Type.mk_int_range (Some Numeral.zero) (Some (E.numeral_of_expr array_size))
+        (Type.mk_array t (
+          if E.is_numeral array_size
+          then
+            let array_size = Numeral.(max zero (E.numeral_of_expr array_size)) in
+            Type.mk_int_range (Some Numeral.zero) (Some array_size)
           else Type.t_int))
         a
       in

src/lustre/lustreSyntaxChecks.ml

@@ -101,7 +101,7 @@ let error_message kind = match kind with
   | NodeCallInRefinableContract (kind, node) -> "Illegal call to " ^ kind ^ " '"
     ^ HString.string_of_hstring node ^ "' in the cone of influence of this contract: " ^ kind ^ " "
     ^ HString.string_of_hstring node ^ " has a refinable contract"
-  | NodeCallInConstant id -> "Illegal node call or choose operator in definition of constant " ^ HString.string_of_hstring id
+  | NodeCallInConstant id -> "Illegal node call or choose operator in definition of constant '" ^ HString.string_of_hstring id ^ "'"
   | IllegalTemporalOperator (kind, variant) -> "Illegal " ^ kind ^ " in " ^ variant ^ " definition, "
     ^ variant ^ "s cannot have state"
   | IllegalImportOfStatefulContract contract -> "Illegal import of stateful contract '"
@@ -524,8 +524,10 @@ let no_dangling_identifiers ctx = function
     no_a_dangling_identifier ctx pos i
   | _ -> Ok ()
 
-let no_node_calls_in_constant pos i e = 
-  if LAH.expr_contains_call e then syntax_error pos (NodeCallInConstant i) else Ok ()
+let no_node_calls_in_constant i e =
+  if LAH.expr_contains_call e
+  then syntax_error (LAH.pos_of_expr e) (NodeCallInConstant i)
+  else Ok ()
 
 let no_quant_var_or_symbolic_index_in_node_call ctx = function
   | LA.Call (pos, i, args) ->
@@ -686,22 +688,21 @@ and check_declaration ctx = function
   | ConstDecl (span, decl) ->
     let check = match decl with
       | LA.FreeConst _ -> Ok ()
-      | UntypedConst (pos, i, e)
-      | TypedConst (pos, i, e, _) -> check_const_expr_decl pos i ctx e
+      | UntypedConst (_, i, e)
+      | TypedConst (_, i, e, _) -> check_const_expr_decl i ctx e
     in
     check >> Ok (LA.ConstDecl (span, decl))
   | NodeDecl (span, decl) -> check_node_decl ctx span decl
   | FuncDecl (span, decl) -> check_func_decl ctx span decl
   | ContractNodeDecl (span, decl) -> check_contract_node_decl ctx span decl
   | NodeParamInst (span, _) -> syntax_error span.start_pos UnsupportedParametricDeclaration
 
-and check_const_expr_decl pos i ctx expr =
-  let composed_checks pos i ctx e =
-    (no_temporal_operator "constant" e)
-      >> (no_dangling_identifiers ctx e)
-      >> (no_node_calls_in_constant pos i e)
+and check_const_expr_decl i ctx expr =
+  let composed_checks i ctx e =
+    (no_dangling_identifiers ctx e)
+    >> (no_node_calls_in_constant i e)
   in
-  check_expr ctx (composed_checks pos i) expr
+  check_expr ctx (composed_checks i) expr
 
 and common_node_equations_checks ctx e =
     (no_dangling_calls ctx e)
@@ -728,8 +729,8 @@ and check_output_items (pos, _id, _ty, clock) =
 
 and check_local_items ctx local = match local with
   | LA.NodeConstDecl (_, FreeConst _) -> Ok ()
-  | LA.NodeConstDecl (pos, UntypedConst (_, i, e)) -> check_const_expr_decl pos i ctx e
-  | LA.NodeConstDecl (pos, TypedConst (_, i, e, _)) -> check_const_expr_decl pos i ctx e
+  | LA.NodeConstDecl (_, UntypedConst (_, i, e)) -> check_const_expr_decl i ctx e
+  | LA.NodeConstDecl (_, TypedConst (_, i, e, _)) -> check_const_expr_decl i ctx e
   | NodeVarDecl (_, (_, _, _, LA.ClockTrue)) -> Ok ()
   | NodeVarDecl (_, (pos, i, _, _)) -> syntax_error pos (UnsupportedClockedLocal i)
 
@@ -884,8 +885,8 @@ and check_contract is_contract_node ctx f contract =
     | GhostConst decl -> (
       let check = match decl with
       | LA.FreeConst _ -> Ok ()
-      | UntypedConst (pos, i, e)
-      | TypedConst (pos, i, e, _) -> check_const_expr_decl pos i ctx e
+      | UntypedConst (_, i, e)
+      | TypedConst (_, i, e, _) -> check_const_expr_decl i ctx e
       in
       check >> Ok ()
     )