Commit 2ee15c1e authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Add untracked files in lus2lic (they were tracked in the lus2lic reop though)

parent e9f29457
(** Time-stamp: <modified the 18/03/2015 (at 16:40) by Erwan Jahier> *)
(* exported *)
type rhs = Soc.var_expr list
type lhs = Soc.var_expr list
type t = Lic.clock * rhs * lhs * Soc.atomic_operation * Lxm.t
(* exported *)
let to_string_msg: (t -> string) =
fun (c, i, o, p, lxm) ->
(* Version surchargée de Soc.string_of_operation pour afficher les "=" *)
let string_of_operation = function
| Soc.Assign -> ""
| op -> SocUtils.string_of_operation op
in
let string_of_params p = String.concat ", " (List.map SocUtils.string_of_filter p) in
if o = [] then
Format.sprintf "%s(%s)" (string_of_operation p) (string_of_params i)
else
Format.sprintf "%s = %s(%s) %s"
(string_of_params o)
(string_of_operation p) (string_of_params i) (Lic.string_of_clock c)
let to_string: (t -> string) =
fun (c, i, o, p,_) ->
(* Version surchargée de SocUtils.string_of_operation : l'objectif est d'afficher,
en cas de cycle combinatoire, un message d'erreur qui parle le plus possible
à l'utilisateur qui a programmé en V6... Pour cela le mieux (je pense) est
simplement de rendre la variable sur laquelle porte le cycle
*)
let string_of_operation = function
| Soc.Assign -> ""
| Soc.Method((n, sk),sname) -> n
| Soc.Procedure(name,_,_) -> name
in
let string_of_params p = String.concat ", " (List.map SocUtils.string_of_filter p) in
if o = [] then
Format.sprintf "%s(%s)"
(string_of_operation p)
(string_of_params i)
else
Format.sprintf "%s = %s(%s)"
(string_of_params o)
(string_of_operation p)
(string_of_params i)
(** Time-stamp: <modified the 15/01/2015 (at 10:45) by Erwan Jahier> *)
(** An action is an intermediary data type that is used to translate expressions
into [Soc.gao]. It is basically a clocked Soc.atomic_operation with arguments.
The idea is that each expression is translated into one or several actions.
And those clocks are then translated into guards, so that each action is
translated into a gao.
A more natural Module to define that type in would have been Soc, but that
module is meant to be shared with other front-ends (e.g., lucid-synchrone),
and I prefer that module not to depend on
- such a cutting (expr -> action -> gao)
- The [Eff.clock] name (could have been a module parameter though).
*)
type rhs = Soc.var_expr list
type lhs = Soc.var_expr list
type t = Lic.clock * rhs * lhs * Soc.atomic_operation * Lxm.t
val to_string: t -> string
(* This one is meant to be used for error msgs *)
val to_string_msg: t -> string
(* Time-stamp: <modified the 26/02/2015 (at 11:18) by Erwan Jahier> *)
open Lxm
open Lic
open Lv6MainArgs
(* *)
exception Not_handled
let rec is_not_atomic = function
| CallByPosLic({it=CONST_REF _} ,_)
| CallByPosLic({it=VAR_REF _}, _ ) -> false
| CallByPosLic({it=TUPLE} ,[ve]) -> is_not_atomic ve.ve_core
| _ -> true
let rec (string_of_val_exp_eff : Lic.val_exp -> string) =
fun ve ->
string_of_val_exp_eff_core ve.ve_core
and string_of_val_exp_eff_core ve_core =
match ve_core with
| CallByPosLic (by_pos_op_eff, vel) ->
(* ICI : on pourrait afficher en commentaire l'éventuel type_matches ? *)
(string_of_by_pos_op_eff by_pos_op_eff vel)
| Merge _
| CallByNameLic _ -> raise Not_handled
and (string_of_by_pos_op_eff: Lic.by_pos_op srcflagged -> Lic.val_exp list -> string) =
fun posop vel ->
let tuple vel = (String.concat ", " (List.map string_of_val_exp_eff vel)) in
let tuple_par vel = "(" ^ (tuple vel) ^ ")" in
let str =
match posop.it,vel with
| CONST c,_ -> LicDump.string_of_const_eff c
| CALL ({it=("Lustre","not"),[]}), [ve1]
| PREDEF_CALL ({it=("Lustre","not"),[]}), [ve1] ->
((AstPredef.op2string AstPredef.NOT_n) ^ " " ^
(if LicDump.is_a_tuple ve1 then (tuple_par [ve1]) else string_of_val_exp_eff ve1))
| CALL ({it=("Lustre","diese"),[]}), _
| CALL ({it=("Lustre","nor"),[]}), _ -> raise Not_handled
| PREDEF_CALL ({it=("Lustre","nor"),[]}), [ve1] -> raise Not_handled
| CALL ({it=("Lustre","if"),[]}), [ve1; ve2; ve3]
| PREDEF_CALL ({it=("Lustre","if"),[]}), [ve1; ve2; ve3] ->
let ve2str = string_of_val_exp_eff ve2 in
let ve2str = if LicDump.is_a_tuple ve2 then "("^ve2str^")" else ve2str in
let ve3str = string_of_val_exp_eff ve3 in
let ve3str = if LicDump.is_a_tuple ve3 then "("^ve3str^")" else ve3str in
" if " ^ (string_of_val_exp_eff ve1) ^
" then " ^ ve2str ^ " else " ^ ve3str
| CALL(op), vel
| PREDEF_CALL(op), vel -> (
if AstPredef.is_a_predef_op (snd(fst op.it)) then
let op_str = snd (fst op.it) in
let op_short_str = AstPredef.op2string (AstPredef.string_to_op op_str) in
if AstPredef.is_infix (AstPredef.string_to_op op_str) then (
match vel with
| [ve1; ve2] ->
(string_of_val_exp_eff ve1) ^ " " ^ op_short_str ^
" " ^ (string_of_val_exp_eff ve2)
| _ -> assert false
)
else
(op_short_str ^
(match op_str with
| "not" | "true" | "false" -> tuple vel
| _ -> tuple_par vel
)
)
else
let nk = op.it in
((string_of_node_key nk) ^ (tuple_par vel))
)
| CONST_REF idl, _ -> LicDump.dump_long idl
| VAR_REF id, _ -> id
| PRE, [ve] ->
if is_not_atomic ve.ve_core then raise Not_handled else
"pre " ^ (string_of_val_exp_eff ve)
| ARROW, [ve1; ve2] ->
(if LicDump.is_a_tuple ve1 then tuple_par [ve1] else string_of_val_exp_eff ve1) ^
" fby loop { " ^
(if LicDump.is_a_tuple ve1 then tuple_par [ve2] else string_of_val_exp_eff ve2) ^
" } "
| FBY, [ve1; ve2] ->
if is_not_atomic ve1.ve_core then raise Not_handled else
(if LicDump.is_a_tuple ve1 then tuple_par [ve1] else string_of_val_exp_eff ve1)
^ " fby loop pre " ^
(if LicDump.is_a_tuple ve1 then tuple_par [ve2] else string_of_val_exp_eff ve2)
| TUPLE,_ -> (tuple vel)
| ARRAY_ACCES(i), [ve1] ->
(string_of_val_exp_eff ve1) ^ "_" ^ (string_of_int i)
| STRUCT_ACCESS(id), [ve1] ->
(string_of_val_exp_eff ve1) ^ "_" ^ (Lv6Id.to_string id)
| STRUCT_ACCESS _, _
| PRE, _
| WHEN _, _
| CURRENT _ ,_
| CONCAT, _
| HAT (_), _
| ARRAY, _
| ARRAY_SLICE(_), _
| ARROW, _
| FBY, _
| ARRAY_ACCES(_), _ -> raise Not_handled
in
let do_not_parenthesize = function
| VAR_REF _,_
| CONST_REF _,_
| PREDEF_CALL({it=("Lustre","true"),[]}),_
| PREDEF_CALL({it=("Lustre","false"),[]}),_
| ARRAY_ACCES _,_
| STRUCT_ACCESS _,_ -> true
| _,_ -> false
in
if
(* already parenthesized *)
( Str.string_match (Str.regexp "^(") str 0 &&
Str.string_match (Str.regexp ")$") str 0 )
||
(* ident or predef constants *)
(do_not_parenthesize (posop.it,vel))
||
global_opt.one_op_per_equation
then
str
else
("(" ^ str ^ ")")
let (f: Lic.val_exp -> string) =
fun ve ->
try " loop {"^string_of_val_exp_eff ve^"}"
with Not_handled -> ""
(* Time-stamp: <modified the 03/03/2015 (at 14:27) by Erwan Jahier> *)
(* maps node_key to a string that won't clash *)
let node_key_tbl = Hashtbl.create 0
(* maps node name (string) to a counter *)
let node_name_tbl = Hashtbl.create 0
(* exported *)
let (node_key: Lic.node_key -> string -> string) =
fun nk name ->
let (long, sargs) = nk in
try Hashtbl.find node_key_tbl nk
(* Note that we ignore the "name" in argument in this case *)
with Not_found ->
(* let's build an ident that won't clash *)
(* all new name should not begins with a "_" ; hence we prefix by "n_" *)
let name = if name = "" then "n_" ^ (Lv6Id.no_pack_string_of_long long) else name in
if not (Hashtbl.mem node_name_tbl name) then
(
(* that name won't clash, but let's tabulate it *)
Hashtbl.add node_name_tbl name 2;
Hashtbl.add node_key_tbl nk name;
name
)
else
(* That name have already been given, there is a possible clash! *)
let cpt = Hashtbl.find node_name_tbl name in
let fresh_name =
Hashtbl.replace node_name_tbl name (cpt+1);
name ^ "_" ^ (string_of_int cpt)
in
Hashtbl.add node_key_tbl nk fresh_name;
fresh_name
(********************************************************************************)
(* Dealing with fresh local (to the node) variable idents *)
let local_var_tbl = Hashtbl.create 0
(********************************************************************************)
(* The idea is to prefix fresh var name by "_", except if at least
one user ident begins by "_". In that case, we try to prefix them
by "_0", and then "_1", and so on so forth. We take the first
possible one.
nb : this won't work if the user have defined all idents from "_1" to
"_1073741823" (on 32-bits machine), but I bet that this compiler
would die before anyway...
nb : We stored in Lv6parserUtils.name_table the set of idents that begins by "_".
*)
let fresh_var_prefix = ref "_"
let char_is_int = function
|'0'|'1'|'2'|'3'|'4'|'5'|'6'|'7'|'8'|'9' -> true
| _ -> false
(* Returns None if str.[1] is not an int, and Some i otherwhise,
where i is the biggest possible int in str after the "_" (e.g.,
"_23toto" returns "Some 23" *)
let (get_int : string -> int option) =
fun str ->
let _ = assert (str<>"" && str.[0]='_') in
let s = String.length str in
if s>1 && char_is_int str.[1] then
let j = ref 2 in
while !j<s && char_is_int str.[!j] do incr j done;
Some (int_of_string (String.sub str 1 (!j-1)))
else
None
let _ = (* A few unit tests *)
assert (get_int "_" = None);
assert (get_int "_toto" = None);
assert (get_int "_1" = Some 1);
assert (get_int "_1234" = Some 1234);
assert (get_int "_1234toto" = Some 1234)
module IntSet =
Set.Make(struct
type t = int
let compare = compare
end)
(* Make sure that update_fresh_var_prefix has been called *)
let fresh_var_prefix_updated = ref false
(* exported *)
let (update_fresh_var_prefix : unit -> unit) =
fun _ ->
let used_ints = (* the set of ints apprearing after a "_" in program idents *)
Hashtbl.fold
(fun name _ acc ->
match get_int name with
None -> IntSet.add (-1) acc
| Some i -> IntSet.add i acc
)
Lv6parserUtils.name_table
IntSet.empty
in
let used_ints = IntSet.elements used_ints in
let rec find_int l =
match l with
| [] -> -1
| [i] -> if i > 0 then 0 else i+1
| i::j::tail -> if j=i+1 then find_int (j::tail) else i+1
in
let index = find_int used_ints in
if index = (-1) then
()
(* no var begins by "_", so "_" is a good prefix.*)
else (
let new_prefix = ("_" ^ (string_of_int index)) in
fresh_var_prefix := new_prefix ;
Verbose.exe ~level:1 (
fun () ->
prerr_string ("I use " ^ new_prefix ^ " as prefix for fresh var names.\n");
flush stderr
)
);
fresh_var_prefix_updated := true
(********************************************************************************)
(* exported *)
let (local_var : string -> string) =
fun prefix ->
try
let cpt = Hashtbl.find local_var_tbl prefix in
assert (!fresh_var_prefix_updated);
Hashtbl.replace local_var_tbl prefix (cpt+1);
!fresh_var_prefix ^ prefix ^"_"^ (string_of_int cpt)
with
Not_found ->
Hashtbl.add local_var_tbl prefix 2;
!fresh_var_prefix ^ prefix ^ "_1"
(********************************************************************************)
(* exported *)
open Lic
let (var_info : string -> Lic.type_ -> Lic.id_clock -> Lic.var_info) =
fun str type_eff clock_eff ->
let id = Lv6Id.of_string (local_var str) in
let var =
{
var_name_eff = id;
var_nature_eff = AstCore.VarLocal;
var_number_eff = -1; (* this field is used only for i/o.
Should i rather put something sensible there ? *)
var_type_eff = type_eff;
var_clock_eff = clock_eff;
}
in
var
(********************************************************************************)
let (array_type : Lic.type_ -> string -> string) =
fun t name ->
"A_" ^ name
(* Time-stamp: <modified the 03/03/2015 (at 14:29) by Erwan Jahier> *)
(** All new identifier names ougth to be created via this module. *)
(** To be called just after the parsing (to make sure that fresh
var names won't clash with user idents. )
Indeed, during the parsing, we collect the set of forbidden id that
we (somehow) transmit to the fresh id generator below.
*)
val update_fresh_var_prefix : unit -> unit
(** [node_key nk] returns a fresh node ident.
The idea is the following: the caller propose a name to map the
node key. But since that name may clash, we sometimes need to work
a little bit more. This is the purpose of that function.
nb : for a node key, it will always return the same string
(which means that [name] migth be ignored).
*)
val node_key: Lic.node_key -> string -> string
(** Dealing with fresh local (to the node) variable idents *)
(** Returns a fresh local var name *)
val local_var : string -> string (* mv new_var? *)
(** Returns a fresh local var_info *)
val var_info : string -> Lic.type_ -> Lic.id_clock -> Lic.var_info
(** *)
val array_type : Lic.type_ -> string -> string
(* Time-stamp: <modified the 14/08/2014 (at 17:07) by Erwan Jahier> *)
(* generate ocaml glue code that makes it possible to call lus2lic
from ocaml with the current set of arguments (with Lus2licRun.make).
*)
open Lv6MainArgs
let (f: string array -> Lv6MainArgs.t -> unit) =
fun argv opt ->
let outfile = if opt.outfile <> "" then opt.outfile else
let file = List.hd opt.infiles in
try (Filename.chop_extension (Filename.basename file))^ ".ml"
with _ ->
print_string ("*** '"^file^"': bad file name.\n"); exit 2
in
let cma_file = (Filename.chop_extension outfile) ^".cma" in
let remove_me = ["-exec"; "-ocaml";"-o";opt.outfile] in
let args =
Array.fold_right (fun x acc -> if List.mem x remove_me then acc else x::acc) argv []
in
let args_str = "\"" ^ (String.concat "\";\"" args) ^"\"" in
let oc = open_out (outfile) in
Lv6util.dump_entete oc;
Printf.fprintf oc "
let plugin =
let args = Array.of_list [%s] in
Lus2licRun.make args
let dyn_file = (Dynlink.adapt_filename \"%s\")
let _ =
OcamlRM.reg_plugin dyn_file plugin
" args_str cma_file
(** Time-stamp: <modified the 21/01/2015 (at 17:35) by Erwan Jahier> *)
open Lxm
open Lic
open AstPredef
let dbg = (Verbose.get_flag "check-mem")
(********************************************************************************)
(* exported *)
let (is_memoryless_val_exp : LicPrg.t -> Lic.val_exp -> bool) =
fun licprg ve ->
let rec (aux_val_exp : Lic.val_exp -> bool) =
fun ve -> aux_val_exp_core ve.ve_core
and aux_val_exp_core ve_core =
match ve_core with
| CallByPosLic(op, vel) -> (
(List.for_all aux_val_exp vel) && aux_pos_op op.it
)
| CallByNameLic(_,cl) -> (
let vel = (snd (List.split cl)) in
List.for_all aux_val_exp vel
)
| Merge(ve,cl) -> (
let vel = ve::(snd (List.split cl)) in
List.for_all aux_val_exp vel
)
and (aux_pos_op: Lic.by_pos_op -> bool) =
function
| CALL({it=nk}) | PREDEF_CALL({it=nk}) -> (
match LicPrg.find_node licprg nk with
| None -> true (* SNO *)
| Some node_exp -> not node_exp.has_mem_eff
)
| CURRENT _ | PRE | ARROW | FBY
-> false
| HAT (_) | ARRAY| ARRAY_SLICE(_) | ARRAY_ACCES(_) | STRUCT_ACCESS(_)
| WHEN _ | TUPLE | CONCAT | CONST _ | CONST_REF _ | VAR_REF _
-> true
in
aux_val_exp ve
let (check_memory : LicPrg.t -> bool -> val_exp -> Lxm.t -> bool -> bool) =
fun licprg should_have_mem ve lxm warning ->
match should_have_mem, not (is_memoryless_val_exp licprg ve) with
| false, false
| true, true -> false (* disable the warning *)
| false, true ->
let msg = "Error: this call uses memory from a function." in
raise (Lv6errors.Compile_error(lxm,msg))
| true, false -> warning
(********************************************************************************)
(* exported *)
let (is_safe_val_exp : LicPrg.t -> Lic.val_exp -> bool) =
fun licprg ve ->
let rec (aux_val_exp : Lic.val_exp -> bool) =
fun ve -> aux_val_exp_core ve.ve_core
and aux_val_exp_core ve_core =
match ve_core with
| CallByPosLic(op, vel) -> (
(List.for_all aux_val_exp vel) && aux_pos_op op.it
)
| CallByNameLic(_,cl) -> (
let vel = (snd (List.split cl)) in
List.for_all aux_val_exp vel
)
| Merge(ve,cl) -> (
let vel = ve::(snd (List.split cl)) in
List.for_all aux_val_exp vel
)
and (aux_pos_op: Lic.by_pos_op -> bool) =
function
| CALL({it=nk}) | PREDEF_CALL({it=nk}) -> (
match LicPrg.find_node licprg nk with
| None -> true (* SNO *)
| Some node_exp -> node_exp.is_safe_eff
)
| CURRENT _ | PRE | ARROW | FBY
| HAT (_) | ARRAY| ARRAY_SLICE(_) | ARRAY_ACCES(_) | STRUCT_ACCESS(_)
| WHEN _ | TUPLE | CONCAT | CONST _ | CONST_REF _ | VAR_REF _
-> true
in
aux_val_exp ve
let (check_safety : LicPrg.t -> bool -> val_exp -> Lxm.t -> bool -> bool) =
fun licprg should_be_safe ve lxm warning ->
match should_be_safe, is_safe_val_exp licprg ve with
| false, false
| true, true -> false (* disable the warning *)
| true, false ->
let msg = "Error: calling an unsafe node from a safe one." in
raise (Lv6errors.Compile_error(lxm,msg))
| false, true -> warning
(********************************************************************************)
let (check_node : LicPrg.t -> Lic.node_exp -> unit) =
fun licprg node ->
match node.def_eff with
| ExternLic | MetaOpLic | AbstractLic _ -> ()
| BodyLic{ eqs_eff = eql ; asserts_eff = vel } ->
let warning = true in
let warning = List.fold_left
(fun warn eq -> check_memory licprg node.has_mem_eff (snd eq.it) eq.src warn)
warning eql
in
let warning = List.fold_left
(fun warn eq -> check_memory licprg node.has_mem_eff eq.it eq.src warn)
warning vel
in
if warning then (
let id = Lic.string_of_node_key node.node_key_eff in
let msg = Printf.sprintf
"%s is declared as a node, but it uses no memory (i.e., it is a function)."
id
in
Lv6errors.warning node.lxm msg;
);
let warning = true in
let warning = List.fold_left
(fun warn eq -> check_safety licprg node.is_safe_eff (snd eq.it) eq.src warn)
warning eql
in
let warning = List.fold_left
(fun warn eq -> check_safety licprg node.is_safe_eff eq.it eq.src warn)
warning vel
in
if warning then (
let id = Lic.string_of_node_key node.node_key_eff in
let msg = Printf.sprintf "%s is declared as unsafe, but is safe." id in
Lv6errors.warning node.lxm msg
)
(* exported *)
let (doit : LicPrg.t -> unit) =