Merge pull request kind2-mc#1054 from daniel-larraz/fix-normalize-gids

Normalize generated equations using proper context

src/lustre/lustreAbstractInterpretation.ml

@@ -231,52 +231,18 @@ and interpret_decl ty_ctx gids = function
 
 and interpret_contract_node ty_ctx (id, _, ins, outs, contract) =
   (* Setup the typing context *)
-  let constants_ctx = ins
-    |> List.map Ctx.extract_consts
-    |> (List.fold_left Ctx.union ty_ctx)
-  in
-  let input_ctx = ins
-    |> List.map Ctx.extract_arg_ctx
-    |> (List.fold_left Ctx.union ty_ctx)
-  in
-  let output_ctx = outs
-    |> List.map Ctx.extract_ret_ctx
-    |> (List.fold_left Ctx.union ty_ctx)
-  in
-  let ty_ctx = Ctx.union
-    (Ctx.union constants_ctx ty_ctx)
-    (Ctx.union input_ctx output_ctx)
-  in
+  let ty_ctx = TC.add_io_node_ctx ty_ctx ins outs in
   interpret_contract id empty_context ty_ctx contract
 
 and interpret_node ty_ctx gids (id, _, _, ins, outs, locals, items, contract) =
   (* Setup the typing context *)
-  let constants_ctx = ins
-    |> List.map Ctx.extract_consts
-    |> (List.fold_left Ctx.union ty_ctx)
-  in
-  let input_ctx = ins
-    |> List.map Ctx.extract_arg_ctx
-    |> (List.fold_left Ctx.union ty_ctx)
-  in
-  let output_ctx = outs
-    |> List.map Ctx.extract_ret_ctx
-    |> (List.fold_left Ctx.union ty_ctx)
-  in
-  let ty_ctx = Ctx.union
-    (Ctx.union constants_ctx ty_ctx)
-    (Ctx.union input_ctx output_ctx)
-  in
+  let ty_ctx = TC.add_io_node_ctx ty_ctx ins outs in
   let ctx = IMap.empty in
   let contract_ctx = match contract with
     | Some contract -> interpret_contract id ctx ty_ctx contract 
     | None -> empty_context
   in
-  let ty_ctx = List.fold_left
-    (fun ctx local -> TC.local_var_binding ctx local |> unwrap)
-    ty_ctx
-    locals 
-  in
+  let ty_ctx = TC.add_local_node_ctx ty_ctx locals |> unwrap in
   let gids_node = GeneratedIdentifiers.StringMap.find id gids in
   let ty_ctx = GeneratedIdentifiers.StringMap.fold
     (fun id (_, ty) ctx -> Ctx.add_ty ctx id ty) (gids_node.GeneratedIdentifiers.locals) ty_ctx

src/lustre/lustreArrayDependencies.ml

@@ -274,27 +274,7 @@ let rec check_inductive_array_dependencies ctx ns = function
 and check_node_decl ctx ns decl =
   let (_, _, _, inputs, outputs, locals, items, _) = decl in
   (* Setup the typing context *)
-  let constants_ctx = inputs
-    |> List.map Ctx.extract_consts
-    |> (List.fold_left Ctx.union ctx)
-  in
-  let input_ctx = inputs
-    |> List.map Ctx.extract_arg_ctx
-    |> (List.fold_left Ctx.union ctx)
-  in
-  let output_ctx = outputs
-    |> List.map Ctx.extract_ret_ctx
-    |> (List.fold_left Ctx.union ctx)
-  in
-  let ctx = Ctx.union
-    (Ctx.union constants_ctx ctx)
-    (Ctx.union input_ctx output_ctx)
-  in
-  let ctx = List.fold_left
-    (fun ctx local -> Chk.local_var_binding ctx local |> unwrap)
-    ctx
-    locals
-  in
+  let ctx = Chk.add_full_node_ctx ctx inputs outputs locals |> unwrap in
   let* (graph, pos_map, count, idx_len) = process_items ctx ns items in
   (* Format.eprintf "Initial graph: %a@." G.pp_print_graph graph; *)
   let graph = add_init_edges idx_len graph in

src/lustre/lustreAstNormalizer.ml

@@ -831,19 +831,20 @@ let rec normalize ctx ai_ctx (decls:LustreAst.t) gids =
     interpretation = StringMap.empty;
     local_group_projection = -1 }
   in 
-  let gids, warnings = normalize_gids info gids in
   let over_declarations (nitems, accum, warnings_accum) item =
     clear_cache ();
-    let (normal_item, map, warnings) =
+    let (normal_item, accum, warnings) =
       normalize_declaration info accum item in
     (match normal_item with 
       | Some ni -> ni :: nitems
       | None -> nitems),
-    StringMap.merge union_keys2 map accum,
+    accum,
     warnings @ warnings_accum
-  in let ast, map, warnings = List.fold_left over_declarations
-    ([], gids, warnings) decls
-  in let ast = List.rev ast in
+  in
+  let ast, map, warnings =
+    List.fold_left over_declarations ([], gids, []) decls
+  in
+  let ast = List.rev ast in
 
   Debug.parse ("===============================================\n"
     ^^ "Generated Identifiers:\n%a\n\n"
@@ -860,36 +861,39 @@ let rec normalize ctx ai_ctx (decls:LustreAst.t) gids =
 
   Res.ok (ast, map, warnings)
 
-and normalize_declaration info map = function
-  | A.NodeDecl (span, decl) ->
-    let normal_decl, map, warnings = normalize_node info map decl in
-    Some (A.NodeDecl(span, normal_decl)), map, warnings
-  | FuncDecl (span, decl) ->
-    let normal_decl, map, warnings = normalize_node info map decl in
-    Some (A.FuncDecl (span, normal_decl)), map, warnings
-  | ContractNodeDecl (_, _) -> None, StringMap.empty, []
-  | decl -> Some decl, StringMap.empty, []
-
-and normalize_gids info gids_map = 
-  (* Convert gids_map to a new gids_map with normalized equations *)
-  let gids_map, warnings = StringMap.fold (fun id gids (gids_map, warnings)  -> 
+and normalize_gid_equations info gids_map node_id =
+  match StringMap.find_opt node_id gids_map with
+  | None -> empty(), []
+  | Some gids -> (
     (* Normalize all equations in gids *)
     let res = List.map (fun (_, _, lhs, expr) ->
       let nexpr, gids, warnings = normalize_expr info gids_map expr in
       gids, warnings, (info.quantified_variables, info.contract_scope, lhs, nexpr)
     ) gids.equations in
-    let gids_list, warnings2, eqs = split3 res in
+    let gids_list, warnings, eqs = split3 res in
     (* Take out old equations that were not normalized *)
     let gids = { gids with equations = [] } in
     let gids = List.fold_left (fun acc g -> union g acc) gids gids_list in
-    let warnings2 = List.flatten warnings2 in
     (* Keep equations generated during normalization *)
     let eqs2 = gids.equations in
     let gids = { gids with equations = eqs @ eqs2; } in
-    let gids_map = StringMap.add id gids gids_map in
-    (gids_map, warnings @ warnings2)
-  ) gids_map (gids_map, []) in
-  gids_map, warnings
+    (gids, List.flatten warnings)
+  )
+
+and normalize_declaration info map = function
+  | A.NodeDecl (span, decl) ->
+    let normal_decl, map, warnings = normalize_node info map decl in
+    Some (A.NodeDecl(span, normal_decl)), map, warnings
+  | FuncDecl (span, decl) ->
+    let normal_decl, map, warnings = normalize_node info map decl in
+    Some (A.FuncDecl (span, normal_decl)), map, warnings
+  | ContractNodeDecl (_, (id, _, ips, ops, _)) ->
+    let ctx = Chk.add_io_node_ctx info.context ips ops in
+    let info = { info with context = ctx } in
+    let ngids, warnings = normalize_gid_equations info map id in
+    let map = StringMap.add id ngids map in
+    None, map, warnings
+  | decl -> Some decl, map, []
 
 and normalize_node_contract info map cref inputs outputs (id, _, ivars, ovars, body) =
   let contract_ref = cref in
@@ -962,22 +966,7 @@ and normalize_ghost_declaration info map = function
 and normalize_node info map
     (node_id, is_extern, params, inputs, outputs, locals, items, contract) =
   (* Setup the typing context *)
-  let constants_ctx = inputs
-    |> List.map Ctx.extract_consts
-    |> (List.fold_left Ctx.union info.context)
-  in
-  let input_ctx = inputs
-    |> List.map Ctx.extract_arg_ctx
-    |> (List.fold_left Ctx.union info.context)
-  in
-  let output_ctx = outputs
-    |> List.map Ctx.extract_ret_ctx
-    |> (List.fold_left Ctx.union info.context)
-  in
-  let ctx = Ctx.union
-    (Ctx.union constants_ctx info.context)
-    (Ctx.union input_ctx output_ctx)
-  in
+  let ctx = Chk.add_io_node_ctx info.context inputs outputs in
   let ctx = Ctx.add_ty ctx ctr_id (A.Int dpos) in
   let info = { info with context = ctx } in
   (* Record subrange constraints on inputs, outputs *)
@@ -1002,14 +991,9 @@ and normalize_node info map
       (Some ncontracts), gids, warnings
     | None -> None, empty (), []
   in
-  (* Record subrange constraints on locals
-    and finish setting up the typing context for the node body *)
-  let ctx = List.fold_left
-    (fun ctx local -> Chk.local_var_binding ctx local |> unwrap)
-    ctx
-    locals
-  in
+  let ctx = Chk.add_local_node_ctx ctx locals |> unwrap in
   let info = { info with context = ctx } in
+  (* Record subrange constraints on locals *)
   let gids3 = locals
     |> List.filter (function
       | A.NodeVarDecl (_, (_, id, _, _)) -> 
@@ -1060,9 +1044,11 @@ and normalize_node info map
       gids4'.history_vars
       (empty ())
   in
-  let gids = union_list [gids1; gids2; gids3; gids4'; gids5'; gids6] in
-  let map = StringMap.singleton node_id gids in
-  (node_id, is_extern, params, inputs, outputs, locals, List.flatten nitems, ncontracts), map, warnings1 @ warnings2
+  let new_gids = union_list [gids1; gids2; gids3; gids4'; gids5'; gids6] in
+  let old_gids, warnings3 = normalize_gid_equations info map node_id in
+  let map = StringMap.add node_id (union old_gids new_gids) map in
+  (node_id, is_extern, params, inputs, outputs, locals, List.flatten nitems, ncontracts),
+  map, warnings1 @ warnings2 @ warnings3
 
 
 and desugar_history info expr =

src/lustre/lustreDesugarAnyOps.ml

@@ -220,40 +220,37 @@ let desugar_any_ops ctx decls =
   let decls =
   List.fold_left (fun decls decl ->
     match decl with
-    | A.NodeDecl (span, ((id, ext, params, inputs, outputs, locals, items, contract) as d)) -> 
+    | A.NodeDecl (span, (id, ext, params, inputs, outputs, locals, items, contract)) ->
     (
-      match Chk.get_node_ctx ctx d with 
-        | Ok ctx ->
-          let items, gen_nodes = List.map (desugar_node_item ctx id) items |> List.split in 
-          let contract, gen_nodes2 = desugar_contract ctx id contract in
-          let gen_nodes = List.flatten gen_nodes in
-          decls @ gen_nodes @ gen_nodes2 @ [A.NodeDecl (span, (id, ext, params, inputs, outputs, locals, items, contract))]
-        (* If there is an error in context collection, it will be detected later in type checking *)
-        | Error _ -> decl :: decls
+      match Chk.add_full_node_ctx ctx inputs outputs locals with
+      | Ok ctx ->
+        let items, gen_nodes = List.map (desugar_node_item ctx id) items |> List.split in
+        let contract, gen_nodes2 = desugar_contract ctx id contract in
+        let gen_nodes = List.flatten gen_nodes in
+        decls @ gen_nodes @ gen_nodes2 @ [A.NodeDecl (span, (id, ext, params, inputs, outputs, locals, items, contract))]
+      (* If there is an error in context collection, it will be detected later in type checking *)
+      | Error _ -> decl :: decls
     )
-    | A.FuncDecl (span, ((id, ext, params, inputs, outputs, locals, items, contract) as d)) -> 
+    | A.FuncDecl (span, (id, ext, params, inputs, outputs, locals, items, contract)) ->
     (
-      match Chk.get_node_ctx ctx d with 
-        | Ok ctx -> 
-          let items, gen_nodes = List.map (desugar_node_item ctx id) items |> List.split in 
-          let contract, gen_nodes2 = desugar_contract ctx id contract in
-          let gen_nodes = List.flatten gen_nodes in
-          decls @ gen_nodes @ gen_nodes2 @ [A.FuncDecl (span, (id, ext, params, inputs, outputs, locals, items, contract))]
-        (* If there is an error in context collection, it will be detected later in type checking *)
-        | Error _ -> decl :: decls
+      match Chk.add_full_node_ctx ctx inputs outputs locals with
+      | Ok ctx ->
+        let items, gen_nodes = List.map (desugar_node_item ctx id) items |> List.split in
+        let contract, gen_nodes2 = desugar_contract ctx id contract in
+        let gen_nodes = List.flatten gen_nodes in
+        decls @ gen_nodes @ gen_nodes2 @ [A.FuncDecl (span, (id, ext, params, inputs, outputs, locals, items, contract))]
+      (* If there is an error in context collection, it will be detected later in type checking *)
+      | Error _ -> decl :: decls
+    )
+    | A.ContractNodeDecl (span, (id, params, inputs, outputs, contract)) ->
+    (
+      let ctx = Chk.add_io_node_ctx ctx inputs outputs in
+      let contract, gen_nodes = desugar_contract ctx id (Some contract) in
+      let contract = match contract with
+        | Some contract -> contract
+        | None -> assert false in (* Must have a contract *)
+      decls @ gen_nodes @ [A.ContractNodeDecl (span, (id, params, inputs, outputs, contract))]
     )
-    | A.ContractNodeDecl (span, (id, params, inputs, outputs, contract)) -> 
-      (
-        match Chk.get_node_ctx ctx ((), (), (), inputs, outputs, [], (), ()) with (* Unit type params are unused in function *)
-          | Ok ctx -> 
-            let contract, gen_nodes = desugar_contract ctx id (Some contract) in
-            let contract = match contract with 
-              | Some contract -> contract 
-              | None -> assert false in (* Must have a contract *)
-            decls @ gen_nodes @ [A.ContractNodeDecl (span, (id, params, inputs, outputs, contract))]
-          (* If there is an error in context collection, it will be detected later in type checking *)
-          | Error _ -> decl :: decls
-      )
     | _ -> decl :: decls
   ) [] decls in 
   decls

src/lustre/lustreDesugarIfBlocks.ml

@@ -340,14 +340,14 @@ let rec desugar_node_item node_id ctx ni = match ni with
 
 (** Desugars an individual node declaration (removing IfBlocks). *)
 let desugar_node_decl ctx decl = match decl with
-  | A.FuncDecl (s, ((node_id, b, nps, cctds, ctds, nlds, nis, co) as d)) ->
-    let ctx = Chk.get_node_ctx ctx d |> unwrap in
+  | A.FuncDecl (s, (node_id, b, nps, cctds, ctds, nlds, nis, co)) ->
+    let ctx = Chk.add_full_node_ctx ctx cctds ctds nlds |> unwrap in
     let* nis = R.seq (List.map (desugar_node_item node_id ctx) nis) in
     let new_decls, nis, gids = split_and_flatten3 nis in
     let gids = List.fold_left GI.union (GI.empty ()) gids in
     R.ok (A.FuncDecl (s, (node_id, b, nps, cctds, ctds, new_decls @ nlds, nis, co)), GI.StringMap.singleton node_id gids) 
-  | A.NodeDecl (s, ((node_id, b, nps, cctds, ctds, nlds, nis, co) as d)) -> 
-    let ctx = Chk.get_node_ctx ctx d |> unwrap in
+  | A.NodeDecl (s, (node_id, b, nps, cctds, ctds, nlds, nis, co)) ->
+    let ctx = Chk.add_full_node_ctx ctx cctds ctds nlds |> unwrap in
     let* nis = R.seq (List.map (desugar_node_item node_id ctx) nis) in
     let new_decls, nis, gids = split_and_flatten3 nis in
     let gids = List.fold_left GI.union (GI.empty ()) gids in

src/lustre/lustreRemoveMultAssign.ml

@@ -163,14 +163,14 @@ let desugar_node_item ctx ni = match ni with
 
 (** Remove multiple assignment from if and frame blocks in a single declaration. *)
 let desugar_node_decl ctx decl = match decl with
-  | A.FuncDecl (s, ((node_id, b, nps, cctds, ctds, nlds, nis, co) as d)) ->
-    let ctx = Chk.get_node_ctx ctx d |> unwrap in
+  | A.FuncDecl (s, (node_id, b, nps, cctds, ctds, nlds, nis, co)) ->
+    let ctx = Chk.add_full_node_ctx ctx cctds ctds nlds |> unwrap in
     let res = List.map (desugar_node_item ctx) nis in
     let nis, gids = List.split res in
     let gids = List.fold_left GI.union (GI.empty ()) gids in
     A.FuncDecl (s, (node_id, b, nps, cctds, ctds, nlds, nis, co)), GI.StringMap.singleton node_id gids
-  | A.NodeDecl (s, ((node_id, b, nps, cctds, ctds, nlds, nis, co) as d)) -> 
-    let ctx = Chk.get_node_ctx ctx d |> unwrap in
+  | A.NodeDecl (s, (node_id, b, nps, cctds, ctds, nlds, nis, co)) ->
+    let ctx = Chk.add_full_node_ctx ctx cctds ctds nlds |> unwrap in
     let res = List.map (desugar_node_item ctx) nis in
     let nis, gids = List.split res in
     let gids = List.fold_left GI.union (GI.empty ()) gids in

src/lustre/lustreTypeChecker.ml

@@ -1724,30 +1724,34 @@ let rec type_check_group: tc_context -> LA.t ->  (unit, [> error]) result list
  * the top most declaration should be able to access 
  * the types of all the forward referenced indentifiers from the context*) 
 
-(** Collects a node's context. *)
-let get_node_ctx ctx (_, _, _, inputs, outputs, locals, _, _) =
-  let constants_ctx = inputs
+let add_io_node_ctx ctx inputs outputs =
+  let ctx = inputs
     |> List.map extract_consts
     |> (List.fold_left union ctx)
   in
-  let input_ctx = inputs
+  let ctx = inputs
     |> List.map extract_arg_ctx
     |> (List.fold_left union ctx)
   in
-  let output_ctx = outputs
+  let ctx = outputs
     |> List.map extract_ret_ctx
     |> (List.fold_left union ctx)
   in
-  let ctx = union
-    (union constants_ctx ctx)
-    (union input_ctx output_ctx) in
-  let rec helper ctx locals = match locals with
-    | local :: locals -> 
-      let* ctx = local_var_binding ctx local in 
+  ctx
+
+let add_local_node_ctx ctx locals =
+  let rec helper ctx = function
+    | local :: locals ->
+      let* ctx = local_var_binding ctx local in
       helper ctx locals
-    | [] -> R.ok ctx in
+    | [] -> R.ok ctx
+  in
   helper ctx locals
 
+let add_full_node_ctx ctx inputs outputs locals =
+  let ctx = add_io_node_ctx ctx inputs outputs in
+  add_local_node_ctx ctx locals
+
 
 let type_check_decl_grps: tc_context -> LA.t list -> (unit, [> error]) result list
   = fun ctx decls ->