Merge branch 'develop' into polymorphic-type-decl

src/ic3ia/IC3IA.ml

@@ -940,11 +940,16 @@ let main fwd slice_to_prop prop in_sys param sys =
 
   let sys =
     if slice_to_prop then (
-      (* Only slice if the property does not contain instantiated variables *)
-      (* The current slicing procedure works on the input system, not the transition system *)
+      (* Only slice if the property was already present in the original input system.
+         The current slicing procedure works on the input system, not the transition system *)
       match prop.Property.prop_source with
-      | Assumption _ -> sys (* An instantiated var is also involved, local sofar var *)
       | Instantiated _ -> sys
+      (* Instantiated properties are only included in the transition system *)
+      | Assumption _ -> sys
+      (* An instantiated var, local sofar var, is involved. *)
+      | Generated (None, _) -> sys
+        (* Currently, only generated properties with an associated position were already
+           present in the original input system *)
       | _ -> fst (InputSystem.trans_sys_of_analysis ~slice_to_prop:prop in_sys param)
     )
     else sys

src/lustre/contractChecker.ml

@@ -400,22 +400,27 @@ let pp_print_realizability_result_json
     )
     | Unrealizable u_res -> (
       if Flags.Contracts.print_deadlock () then (
-        let trace, core =
-          compute_unviable_trace_and_core
-            analyze in_sys param sys u_res
-        in
-        (fun fmt ->
-          let cpd =
-            ME.loc_core_to_print_data in_sys sys core_desc None core
+        try (
+          let trace, core =
+            compute_unviable_trace_and_core
+              analyze in_sys param sys u_res
           in
-          Format.fprintf
-          fmt
-          ",@,%a,@,\
-          \"conflictingSet\" : %a"
-          (KEvent.pp_print_trace_json
-            ~object_name:"deadlockingTrace" in_sys param sys None true)
-          trace
-          (ME.pp_print_core_data_json in_sys param sys) cpd
+          (fun fmt ->
+            let cpd =
+              ME.loc_core_to_print_data in_sys sys core_desc None core
+            in
+            Format.fprintf
+            fmt
+            ",@,%a,@,\
+            \"conflictingSet\" : %a"
+            (KEvent.pp_print_trace_json
+              ~object_name:"deadlockingTrace" in_sys param sys None true)
+            trace
+            (ME.pp_print_core_data_json in_sys param sys) cpd
+          )
+        )
+        with Realizability.Trace_or_conflict_computation_failed _ -> (
+          (fun _ -> ())
         )
       )
       else (fun _ -> ())
@@ -458,21 +463,26 @@ let pp_print_realizability_result_xml
     )
     | Unrealizable u_res -> (
       if Flags.Contracts.print_deadlock () then (
-        let trace, core =
-          compute_unviable_trace_and_core
-            analyze in_sys param sys u_res
-        in
-        (fun fmt ->
-          let cpd =
-            ME.loc_core_to_print_data in_sys sys core_desc None core
+        try (
+          let trace, core =
+            compute_unviable_trace_and_core
+              analyze in_sys param sys u_res
           in
-          Format.fprintf
-          fmt
-          "@,%a@,%a"
-          (KEvent.pp_print_trace_xml
-            ~tag:"DeadlockingTrace" in_sys param sys None true)
-          trace
-          (ME.pp_print_core_data_xml ~tag:"ConflictingSet" in_sys param sys) cpd
+          (fun fmt ->
+            let cpd =
+              ME.loc_core_to_print_data in_sys sys core_desc None core
+            in
+            Format.fprintf
+            fmt
+            "@,%a@,%a"
+            (KEvent.pp_print_trace_xml
+              ~tag:"DeadlockingTrace" in_sys param sys None true)
+            trace
+            (ME.pp_print_core_data_xml ~tag:"ConflictingSet" in_sys param sys) cpd
+          )
+        )
+        with Realizability.Trace_or_conflict_computation_failed _ -> (
+          (fun _ -> ())
         )
       )
       else (fun _ -> ())

src/lustre/lustreAbstractInterpretation.ml

@@ -458,6 +458,7 @@ and interpret_structured_expr f node_id ctx ty_ctx ty proj expr =
       let g = interpret_structured_expr f node_id ctx ty_ctx ty in
       Ctx.traverse_group_expr_list g ty_ctx proj es
     )
+    | StructUpdate (_, e, _, _) -> interpret_expr_by_type node_id ctx ty_ctx ty proj e
     | _ -> assert false)
 
 and interpret_int_expr node_id ctx ty_ctx proj expr = 

src/lustre/lustreAstHelpers.ml

@@ -1653,3 +1653,8 @@ let name_of_prop pos name k =
     in
     Format.asprintf "%sProp%a" kind_str Lib.pp_print_line_and_column pos
     |> HString.mk_hstring
+
+let get_const_num_value = function
+  | Const (_, Num x) ->
+    int_of_string_opt (HString.string_of_hstring x)
+  | _ -> None

src/lustre/lustreAstHelpers.mli

@@ -186,3 +186,5 @@ val rename_contract_vars : expr -> expr
 
 val name_of_prop : Lib.position -> HString.t option -> LustreAst.prop_kind -> HString.t
 (** Get the name associated with a property *)
+
+val get_const_num_value : expr -> int option

src/lustre/lustreDeclarations.ml

@@ -1298,7 +1298,7 @@ and eval_node_contract_call
   known ctx scope inputs outputs locals is_candidate (
     call_pos, id, tys, in_params, out_params
   ) = 
-  if tys <> [] then fail_at_position call_pos "Contract calls with type parameters not supports in old frontend" else
+  if tys <> [] then fail_at_position call_pos "Contract calls with type parameters not supported in old frontend" else
 
   let id' = HString.string_of_hstring id in
   let ident = I.mk_string_ident id' in

src/lustre/lustreGenRefTypeImpNodes.ml

@@ -22,7 +22,7 @@ module Ctx = TypeCheckerContext
 let inputs_tag = ".inputs_"
 let contract_tag = ".contract_"
 let type_tag = ".type_"
-let poly_gen_node_tag = ".poly"
+let poly_gen_node_tag = ".poly_"
 
 let unwrap = function 
   | Ok x -> x 

src/lustre/lustreTypeChecker.ml

@@ -57,8 +57,10 @@ type error_kind = Unknown of string
   | Unsupported of string
   | UnequalArrayExpressionType
   | TypeMismatchOfRecordLabel of HString.t * tc_type * tc_type
-  | IlltypedRecordUpdate of tc_type
+  | IlltypedUpdateWithLabel of tc_type
+  | IlltypedUpdateWithIndex of tc_type
   | ExpectedLabel of LA.expr
+  | ExpectedIntegerLiteral of LA.expr
   | IlltypedArraySlice of tc_type
   | ExpectedIntegerTypeForSlice
   | IlltypedArrayIndex of tc_type
@@ -127,8 +129,10 @@ let error_message kind = match kind with
   | UnequalArrayExpressionType -> "All expressions must be of the same type in an Array"
   | TypeMismatchOfRecordLabel (label, ty1, ty2) -> "Type mismatch. Type of record label '" ^ (HString.string_of_hstring label)
     ^ "' is of type " ^ string_of_tc_type ty1 ^ " but the type of the expression is " ^ string_of_tc_type ty2
-  | IlltypedRecordUpdate ty -> "Cannot do an update on non-record type " ^ string_of_tc_type ty
+  | IlltypedUpdateWithLabel ty -> "Expected a record type but found " ^ string_of_tc_type ty
+  | IlltypedUpdateWithIndex ty -> "Expected a tuple type or an array type but found " ^ string_of_tc_type ty
   | ExpectedLabel e -> "Only labels can be used for record expressions but found " ^ LA.string_of_expr e
+  | ExpectedIntegerLiteral e -> "Expected an integer literal but found " ^ LA.string_of_expr e
   | IlltypedArraySlice ty -> "Slicing can only be done on an array type but found " ^ string_of_tc_type ty
   | ExpectedIntegerTypeForSlice -> "Slicing should have integer types"
   | IlltypedArrayIndex ty -> "Indexing can only be done on an array type but found " ^ string_of_tc_type ty
@@ -762,13 +766,13 @@ let rec infer_type_expr: tc_context -> HString.t option -> LA.expr -> (tc_type *
     check_array_size_expr ctx nname sup_expr
     >> R.ok (LA.ArrayType (pos, (b_ty, sup_expr)), warnings)
   )
-  | LA.StructUpdate (pos, r, i_or_ls, e) ->
+  | LA.StructUpdate (pos, ue, i_or_ls, e) ->
     if List.length i_or_ls != 1
     then type_error pos (Unsupported ("List of labels or indices for structure update is not supported"))
     else
       (match List.hd i_or_ls with
       | LA.Label (pos, l) ->  
-          infer_type_expr ctx nname r
+          infer_type_expr ctx nname ue
           >>= (function 
               | RecordType (_, _, flds) as r_ty, warnings1 ->
                   (let typed_fields = List.map (fun (_, i, ty) -> (i, ty)) flds in
@@ -779,8 +783,34 @@ let rec infer_type_expr: tc_context -> HString.t option -> LA.expr -> (tc_type *
                         (R.ok (r_ty, warnings1 @ warnings2))
                         (type_error pos (TypeMismatchOfRecordLabel (l, f_ty, e_ty)))
                     | None -> type_error pos (NotAFieldOfRecord l)))
-              | r_ty, _ -> type_error pos (IlltypedRecordUpdate r_ty))
-      | LA.Index (_, e) -> type_error pos (ExpectedLabel e))
+              | r_ty, _ -> type_error pos (IlltypedUpdateWithLabel r_ty))
+      | LA.Index (pos, i) ->
+        let* ue_ty, warnings1 = infer_type_expr ctx nname ue in
+        (match ue_ty with
+        | TupleType _ -> (
+          let* idx =
+            match LH.get_const_num_value i with
+            | Some n -> Ok n
+            | None -> type_error pos (ExpectedIntegerLiteral i)
+          in
+          let* e_ty, warnings2 = infer_type_expr ctx nname e in
+          let* warnings3 = check_type_tuple_proj pos ctx nname ue idx e_ty in
+          R.ok (ue_ty, warnings1 @ warnings2 @ warnings3)
+        )
+        | ArrayType (_, (b_ty, _)) -> (
+          let* index_type, warnings1 = infer_type_expr ctx nname i in
+          let* index_type = expand_type_syn_reftype_history ctx index_type in
+          if is_expr_int_type ctx nname i then
+            let* e_ty, warnings2 = infer_type_expr ctx nname e in
+            R.ifM (eq_lustre_type ctx b_ty e_ty)
+              (R.ok (ue_ty, warnings1 @ warnings2))
+              (type_error pos (ExpectedType (e_ty, b_ty)))
+          else
+            type_error pos (ExpectedIntegerTypeForArrayIndex index_type)
+        )
+        | _ -> type_error pos (IlltypedUpdateWithIndex ue_ty)
+        )
+      )
   | LA.ArrayIndex (pos, e, i) ->
     let* index_type, warnings1 = infer_type_expr ctx nname i in
     let* index_type = expand_type_syn_reftype_history ctx index_type in
@@ -979,22 +1009,46 @@ and check_type_expr: tc_context -> HString.t option -> LA.expr -> tc_type -> ([>
             (type_error pos UnequalArrayExpressionType))
 
   (* Update of structured expressions *)
-  | StructUpdate (pos, r, i_or_ls, e) ->
+  | StructUpdate (pos, ue, i_or_ls, e) ->
     if List.length i_or_ls != 1
     then type_error pos (Unsupported ("List of labels or indices for structure update is not supported"))
-    else (match List.hd  i_or_ls with
-          | LA.Label (pos, l) ->  
-            let* r_ty, warnings1 = infer_type_expr ctx nname r in (
-              match r_ty with
-              | RecordType (_, _, flds) ->
-                (let typed_fields = List.map (fun (_, i, ty) -> (i, ty)) flds in
-                  (match (List.assoc_opt l typed_fields) with
-                  | Some ty -> 
-                    let* warnings2 = check_type_expr ctx nname e ty in 
-                    R.ok (warnings1 @ warnings2)
-                  | None -> type_error pos (NotAFieldOfRecord l)))
-              | _ -> type_error pos (IlltypedRecordUpdate r_ty))
-          | LA.Index (_, e) -> type_error pos (ExpectedLabel e))
+    else
+      (match List.hd i_or_ls with
+      | LA.Label (pos, l) ->
+        let* r_ty, warnings1 = infer_type_expr ctx nname ue in (
+          match r_ty with
+          | RecordType (_, _, flds) ->
+            (let typed_fields = List.map (fun (_, i, ty) -> (i, ty)) flds in
+              (match (List.assoc_opt l typed_fields) with
+              | Some ty ->
+                let* warnings2 = check_type_expr ctx nname e ty in
+                R.ok (warnings1 @ warnings2)
+              | None -> type_error pos (NotAFieldOfRecord l)))
+          | _ -> type_error pos (IlltypedUpdateWithLabel r_ty))
+      | LA.Index (_, i) ->
+        let* ue_ty, warnings1 = infer_type_expr ctx nname ue in
+        (match ue_ty with
+        | TupleType _ -> (
+          let* idx =
+            match LH.get_const_num_value i with
+            | Some n -> Ok n
+            | None -> type_error pos (ExpectedIntegerLiteral i)
+          in
+          let* e_ty, warnings2 = infer_type_expr ctx nname e in
+          let* warnings3 = check_type_tuple_proj pos ctx nname ue idx e_ty in
+          R.ok (warnings1 @ warnings2 @ warnings3)
+        )
+        | ArrayType (_, (b_ty, _)) -> (
+          let* index_type, warnings1 = infer_type_expr ctx nname i in
+          let* index_type = expand_type_syn_reftype_history ctx index_type in
+          if is_expr_int_type ctx nname i then
+            let* warnings2 = check_type_expr ctx nname e b_ty in
+            R.ok (warnings1 @ warnings2)
+          else
+            type_error pos (ExpectedIntegerTypeForArrayIndex index_type)
+        )
+        | _ -> type_error pos (IlltypedUpdateWithIndex ue_ty)
+        ))
 
   (* Array constructor*)
   | ArrayConstr (pos, b_exp, sup_exp) ->

src/lustre/lustreTypeChecker.mli

@@ -42,8 +42,10 @@ type error_kind = Unknown of string
   | Unsupported of string
   | UnequalArrayExpressionType
   | TypeMismatchOfRecordLabel of HString.t * tc_type * tc_type
-  | IlltypedRecordUpdate of tc_type
+  | IlltypedUpdateWithLabel of tc_type
+  | IlltypedUpdateWithIndex of tc_type
   | ExpectedLabel of LA.expr
+  | ExpectedIntegerLiteral of LA.expr
   | IlltypedArraySlice of tc_type
   | ExpectedIntegerTypeForSlice
   | IlltypedArrayIndex of tc_type

src/lustre/typeCheckerContext.ml

@@ -218,7 +218,7 @@ let lookup_node_ty_vars: tc_context -> LA.ident -> HString.t list option
 
 let lookup_node_ty_args: tc_context -> LA.ident -> LA.lustre_type list option
   = fun ctx i -> IMap.find_opt i (ctx.ty_args)
-(** Lookup a node's type variables *)
+(** Lookup a node's type arguments *)
 
 let lookup_contract_ty_vars: tc_context -> LA.ident -> HString.t list option
   = fun ctx i -> IMap.find_opt i (ctx.contract_ty_vars)
@@ -274,7 +274,7 @@ let add_ty_vars_ty: tc_context -> LA.ident -> LA.ident list -> tc_context
 let add_ty_args_node: tc_context -> LA.ident -> LA.lustre_type list -> tc_context
   = fun ctx i ty_args -> 
     {ctx with ty_args = IMap.add i ty_args (ctx.ty_args)}
-(**  Add the type variables of the node *)
+(**  Add the type arguments of the node *)
 
 let add_ty_vars_contract: tc_context -> LA.ident -> LA.ident list -> tc_context
   = fun ctx i contract_ty_vars -> 

src/lustre/typeCheckerContext.mli

@@ -149,7 +149,7 @@ val add_ty_args_node: tc_context -> HString.t -> LA.lustre_type list -> tc_conte
 (** Add node/function type arguments into the typing context *)
 
 val add_ty_vars_contract: tc_context -> HString.t -> HString.t list -> tc_context 
-(** Add node/function type variables into the typing context *)
+(** Add contract type variables into the typing context *)
 
 val add_node_param_attr: tc_context -> LA.ident -> LA.const_clocked_typed_decl list -> tc_context
 (** Track whether node parameters are constant or not *)

tests/regression/success/struct_update.lus

@@ -0,0 +1,10 @@
+
+type MyPair = [int, bool];
+
+node N(A:int^3; p1: MyPair) returns (B: int^3; p2: MyPair);
+let
+  B = (A with [0] = 1);
+  p2 = (p1 with .%1 = true);
+  check B[0] = 1;
+  check p2.%1;
+tel