From df94cd73c3919c235cac2d9835bfdca778b80e71 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Fri, 5 Jul 2019 15:04:18 -0700
Subject: [PATCH] - More systematic translation for mutation - copy_var_decl
now keeps the generated type
---
src/corelang.ml | 22 +++++++------
src/lustre_types.ml | 7 ++++-
src/mutation.ml | 77 ++++++++++++++++++++-------------------------
3 files changed, 53 insertions(+), 53 deletions(-)
diff --git a/src/corelang.ml b/src/corelang.ml
index 82f45f38..541725aa 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -719,7 +719,17 @@ let get_node_interface nd =
(* Renaming / Copying *)
let copy_var_decl vdecl =
- mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig (vdecl.var_id, vdecl.var_dec_type, vdecl.var_dec_clock, vdecl.var_dec_const, vdecl.var_dec_value, vdecl.var_parent_nodeid)
+ mkvar_decl
+ vdecl.var_loc
+ ~orig:vdecl.var_orig
+ (
+ vdecl.var_id,
+ vdecl.var_dec_type,
+ vdecl.var_dec_clock,
+ vdecl.var_dec_const,
+ vdecl.var_dec_value,
+ vdecl.var_parent_nodeid
+ )
let copy_const cdecl =
{ cdecl with const_type = Types.new_var () }
@@ -802,18 +812,12 @@ let rec rename_carrier rename cck =
Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
| Expr_appl (i, e', i') ->
Expr_appl (f_node i, re e', Utils.option_map re i')
-
- let rename_dec_type f_node f_var t = t (* TODO : do we really want to rename a declared type ?
- Types.rename_dim_type (Dimension.rename f_node f_var) t*)
-
- let rename_dec_clock f_node f_var c = c (* TODO : do we really want to rename a declared clock ? assert false
- Clocks.rename_clock_expr f_var c*)
let rename_var f_node f_var v = {
(copy_var_decl v) with
var_id = f_var v.var_id;
- var_dec_type = rename_dec_type f_node f_var v.var_dec_type;
- var_dec_clock = rename_dec_clock f_node f_var v.var_dec_clock
+ var_type = v.var_type;
+ var_clock = v.var_clock;
}
let rename_vars f_node f_var = List.map (rename_var f_node f_var)
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index 58764678..7170eefa 100644
--- a/src/lustre_types.ml
+++ b/src/lustre_types.ml
@@ -127,7 +127,12 @@ and expr_annot =
annot_loc: Location.t}
type contract_mode =
- { mode_id: ident; require: eexpr list; ensure: eexpr list; mode_loc: Location.t}
+ {
+ mode_id: ident;
+ require: eexpr list;
+ ensure: eexpr list;
+ mode_loc: Location.t
+ }
type contract_import =
{ import_nodeid: ident;
diff --git a/src/mutation.ml b/src/mutation.ml
index 2aa312d2..769e2379 100644
--- a/src/mutation.ml
+++ b/src/mutation.ml
@@ -30,16 +30,20 @@ let threshold_bool_op = 95
let int_consts = ref []
let rename_app id =
- let node = Corelang.node_from_name id in
- let is_imported =
- match node.top_decl_desc with
- | ImportedNode _ -> true
- | _ -> false
- in
- if !Options.no_mutation_suffix || is_imported then
+ if List.mem id Basic_library.internal_funs ||
+ !Options.no_mutation_suffix then
id
else
- id ^ "_mutant"
+ let node = Corelang.node_from_name id in
+ let is_imported =
+ match node.top_decl_desc with
+ | ImportedNode _ -> true
+ | _ -> false
+ in
+ if is_imported then
+ id
+ else
+ id ^ "_mutant"
(************************************************************************************)
(* Gathering constants in the code *)
@@ -455,7 +459,7 @@ let fold_mutate_op op =
target := Some (Op(op_orig, n-1, op_new));
op
)
- | _ -> if List.mem op Basic_library.internal_funs then op else rename_app op
+ | _ -> op
let fold_mutate_var expr =
@@ -491,19 +495,19 @@ let fold_mutate_pre orig_expr e =
)
| _ -> Expr_pre e
-let fold_mutate_const_value c =
-match c with
-| Const_int i -> (
- match !target with
- | Some (IncrIntCst 0) -> (set_mutation_loc (); Const_int (i+1))
- | Some (DecrIntCst 0) -> (set_mutation_loc (); Const_int (i-1))
- | Some (SwitchIntCst (0, id)) ->
- (set_mutation_loc (); Const_int id)
- | Some (IncrIntCst n) -> (target := Some (IncrIntCst (n-1)); c)
- | Some (DecrIntCst n) -> (target := Some (DecrIntCst (n-1)); c)
- | Some (SwitchIntCst (n, id)) -> (target := Some (SwitchIntCst (n-1, id)); c)
- | _ -> c)
-| _ -> c
+let fold_mutate_const_value c =
+ match c with
+ | Const_int i -> (
+ match !target with
+ | Some (IncrIntCst 0) -> (set_mutation_loc (); Const_int (i+1))
+ | Some (DecrIntCst 0) -> (set_mutation_loc (); Const_int (i-1))
+ | Some (SwitchIntCst (0, id)) ->
+ (set_mutation_loc (); Const_int id)
+ | Some (IncrIntCst n) -> (target := Some (IncrIntCst (n-1)); c)
+ | Some (DecrIntCst n) -> (target := Some (DecrIntCst (n-1)); c)
+ | Some (SwitchIntCst (n, id)) -> (target := Some (SwitchIntCst (n-1, id)); c)
+ | _ -> c)
+ | _ -> c
(*
match c with
@@ -561,29 +565,16 @@ let fold_mutate_stmt stmt =
| Eq eq -> Eq (fold_mutate_eq eq)
| Aut aut -> assert false
-let mutate_contract c =
- { c with
- (* TODO: translate other fields. Do not mutate them, just rename
- the calls with the _mutant suffix *)
- imports = List.map (fun ci -> { ci with import_nodeid = rename_app ci.import_nodeid }) c.imports;
- }
-
-let mutate_spec spec =
- match spec with
- | Contract c -> Contract (mutate_contract c)
- | NodeSpec id -> NodeSpec (rename_app id)
-
+
let fold_mutate_node nd =
current_node := Some nd.node_id;
- { nd with
- node_stmts =
- List.fold_right (fun stmt res -> (fold_mutate_stmt stmt)::res) nd.node_stmts [];
- node_spec = (
- match nd.node_spec with
- | None -> None
- | Some spec -> Some (mutate_spec spec));
- node_id = rename_app nd.node_id
- }
+ let nd =
+ { nd with
+ node_stmts =
+ List.fold_right (fun stmt res -> (fold_mutate_stmt stmt)::res) nd.node_stmts [];
+ }
+ in
+ rename_node rename_app (fun x -> x) nd
let fold_mutate_top_decl td =
match td.top_decl_desc with
--
GitLab