jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Tabs, trailing ws and long lines shall receive no mercy!

Browse source
This commit is contained in:
Adrien Guatto 2010-06-26 16:53:25 +02:00
parent 7323c83f79
commit b4ddefa65c
52 changed files with 2792 additions and 2732 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
compiler/global/ident.ml
View file

@ -18,7 +18,7 @@ type ident = {
let compare id1 id2 = compare id1.num id2.num
let sourcename id = id.source
let name id =
let name id =
if id.is_generated then
id.source ^ "_" ^ (string_of_int id.num)
else
@ -28,12 +28,12 @@ let set_sourcename id v =
{ id with source = v }
let num = ref 0
let fresh s =
num := !num + 1;
let fresh s =
num := !num + 1;
{ num = !num; source = s; is_generated = true }
let ident_of_name s =
num := !num + 1;
let ident_of_name s =
num := !num + 1;
{ num = !num; source = s; is_generated = false }
let fprint_t ff id = Format.fprintf ff "%s" (name id)
@ -54,18 +54,18 @@ struct
(* Environments union *)
let union env1 env2 =
fold (fun name elt env -> add name elt env) env2 env1
(* Environments difference : env1 - env2 *)
let diff env1 env2 =
fold (fun name _ env -> remove name env) env2 env1
(* Environments partition *)
let partition p env =
fold
(fun key elt (env1,env2) ->
if p(key)
then ((add key elt env1),env2)
else (env1,(add key elt env2)))
if p(key)
then ((add key elt env1),env2)
else (env1,(add key elt env2)))
env
(empty, empty)
end

2
compiler/global/ident.mli
View file

@ -24,7 +24,7 @@ val ident_of_name : string -> ident
module Env :
sig
include (Map.S with type key = ident)
val append : 'a t -> 'a t -> 'a t
val union : 'a t -> 'a t -> 'a t
val diff : 'a t -> 'b t -> 'a t

55
compiler/global/location.ml
View file

@ -10,7 +10,6 @@ type location =
* int (* Position of the next character following the last one *)
let input_name = ref "" (* Input file name. *)
let input_chan = ref stdin (* The channel opened on the input. *)
@ -32,12 +31,12 @@ let current_loc () =
let output_lines oc char1 char2 charline1 line1 line2 =
let n1 = char1 - charline1
and n2 = char2 - charline1 in
if line2 > line1 then
Printf.fprintf oc
", line %d-%d, characters %d-%d:\n" line1 line2 n1 n2
else
Printf.fprintf oc ", line %d, characters %d-%d:\n" line1 n1 n2;
()
if line2 > line1 then
Printf.fprintf oc
", line %d-%d, characters %d-%d:\n" line1 line2 n1 n2
else
Printf.fprintf oc ", line %d, characters %d-%d:\n" line1 n1 n2;
()
let output_loc oc input seek line_flag (Loc(pos1, pos2)) =
@ -49,30 +48,30 @@ let output_loc oc input seek line_flag (Loc(pos1, pos2)) =
with End_of_file -> () in
let copy_line () =
let c = ref ' ' in
begin try
while c := input(); !c != '\n' do output_char oc !c done
with End_of_file ->
output_string oc "<EOF>"
end;
output_char oc '\n' in
begin try
while c := input(); !c != '\n' do output_char oc !c done
with End_of_file ->
output_string oc "<EOF>"
end;
output_char oc '\n' in
let pr_line first len ch =
let c = ref ' '
and f = ref first
and l = ref len in
try
while c := input (); !c != '\n' do
if !f > 0 then begin
f := !f - 1;
output_char oc (if !c == '\t' then !c else ' ')
end
else if !l > 0 then begin
l := !l - 1;
output_char oc (if !c == '\t' then !c else ch)
end
else ()
done
with End_of_file ->
if !f = 0 && !l > 0 then pr_chars 5 ch in
try
while c := input (); !c != '\n' do
if !f > 0 then begin
f := !f - 1;
output_char oc (if !c == '\t' then !c else ' ')
end
else if !l > 0 then begin
l := !l - 1;
output_char oc (if !c == '\t' then !c else ch)
end
else ()
done
with End_of_file ->
if !f = 0 && !l > 0 then pr_chars 5 ch in
let pos = ref 0
and line1 = ref 1
and line1_pos = ref 0
@ -148,7 +147,7 @@ let output_location oc loc =
oc (fun () -> input_char !input_chan) (seek_in !input_chan) true
loc;
seek_in !input_chan p
let output_input_name oc =
Printf.fprintf oc "File \"%s\", line 1:\n" !input_name

78
compiler/global/modules.ml
View file

@ -51,65 +51,65 @@ let findfile filename =
raise(Cannot_find_file filename)
else
let rec find = function
[] ->
raise(Cannot_find_file filename)
| a::rest ->
let b = Filename.concat a filename in
[] ->
raise(Cannot_find_file filename)
| a::rest ->
let b = Filename.concat a filename in
if Sys.file_exists b then b else find rest
in find !load_path
let load_module modname =
let name = String.uncapitalize modname in
try
let filename = findfile (name ^ ".epci") in
let ic = open_in_bin filename in
try
let filename = findfile (name ^ ".epci") in
let ic = open_in_bin filename in
try
let m:env = input_value ic in
if m.format_version <> interface_format_version then (
Printf.eprintf "The file %s was compiled with \
let m:env = input_value ic in
if m.format_version <> interface_format_version then (
Printf.eprintf "The file %s was compiled with \
an older version of the compiler.\n \
Please recompile %s.ept first.\n" filename name;
raise Error
);
close_in ic;
m
with
| End_of_file | Failure _ ->
close_in ic;
Printf.eprintf "Corrupted compiled interface file %s.\n\
Please recompile %s.ept first.\n" filename name;
raise Error
raise Error
);
close_in ic;
m
with
| Cannot_find_file(filename) ->
Printf.eprintf "Cannot find the compiled interface file %s.\n"
filename;
raise Error
| End_of_file | Failure _ ->
close_in ic;
Printf.eprintf "Corrupted compiled interface file %s.\n\
Please recompile %s.ept first.\n" filename name;
raise Error
with
| Cannot_find_file(filename) ->
Printf.eprintf "Cannot find the compiled interface file %s.\n"
filename;
raise Error
let find_module modname =
try
NamesEnv.find modname modules.modules
with
Not_found ->
let m = load_module modname in
modules.modules <- NamesEnv.add modname m modules.modules;
m
let m = load_module modname in
modules.modules <- NamesEnv.add modname m modules.modules;
m
type 'a info = { qualid : qualident; info : 'a }
let find where qualname =
let rec findrec ident = function
| [] -> raise Not_found
| m :: l ->
try { qualid = { qual = m.name; id = ident };
info = where ident m }
with Not_found -> findrec ident l in
let rec findrec ident = function
| [] -> raise Not_found
| m :: l ->
try { qualid = { qual = m.name; id = ident };
info = where ident m }
with Not_found -> findrec ident l in
match qualname with
| Modname({ qual = m; id = ident } as q) ->
let current = if current.name = m then current else find_module m in
{ qualid = q; info = where ident current }
| Name(ident) -> findrec ident (current :: modules.opened)
match qualname with
| Modname({ qual = m; id = ident } as q) ->
let current = if current.name = m then current else find_module m in
{ qualid = q; info = where ident current }
| Name(ident) -> findrec ident (current :: modules.opened)
(* exported functions *)
let open_module modname =
@ -153,5 +153,5 @@ let currentname longname =
match longname with
| Name(n) -> longname
| Modname{ qual = q; id = id} ->
if current.name = q then Name(id) else longname
if current.name = q then Name(id) else longname

31
compiler/global/names.ml
View file

@ -1,12 +1,12 @@
(** Define qualified names "Module.name" (longname)
[shortname] longname -> name
[fullname] longname -> Module.name *)
[shortname] longname -> name
[fullname] longname -> Module.name *)
type name = string
type longname =
| Name of name
| Modname of qualident
| Name of name
| Modname of qualident
and qualident = { qual: string; id: string }
@ -42,8 +42,8 @@ let mk_longname s =
with Not_found -> Name s
(** Are infix
[or], [quo], [mod], [land], [lor], [lxor], [lsl], [lsr], [asr]
and every names not beginning with 'a' .. 'z' | 'A' .. 'Z' | '_' | '`'*)
[or], [quo], [mod], [land], [lor], [lxor], [lsl], [lsr], [asr]
and every names not beginning with 'a' .. 'z' | 'A' .. 'Z' | '_' | '`'*)
let is_infix s =
let module StrSet = Set.Make(String) in
let infix_set =
@ -52,19 +52,22 @@ let is_infix s =
StrSet.empty in
if StrSet.mem s infix_set then true
else (match String.get s 0 with
| 'a' .. 'z' | 'A' .. 'Z' | '_' | '`' -> false
| _ -> true)
| 'a' .. 'z' | 'A' .. 'Z' | '_' | '`' -> false
| _ -> true)
let print_name ff n =
let n = if is_infix n
then "( " ^ (n ^ " )") (* do not remove the space around n, since for example "(*" would create bugs *)
else n
then "( " ^ (n ^ " )") (* do not remove the space around n, since for example
"(*" would create bugs *)
else n
in Format.fprintf ff "%s" n
let print_longname ff n =
match n with
| Name m -> print_name ff m
| Modname { qual = "Pervasives"; id = m } -> print_name ff m
| Modname { qual = m1; id = m2 } -> (Format.fprintf ff "%s." m1; print_name ff m2)
| Name m -> print_name ff m
| Modname { qual = "Pervasives"; id = m } -> print_name ff m
| Modname { qual = m1; id = m2 } ->
Format.fprintf ff "%s." m1;
print_name ff m2

12
compiler/global/signature.ml
View file

@ -22,10 +22,10 @@ type param = { p_name : name }
(** Node signature *)
type node =
{ node_inputs : arg list;
node_outputs : arg list;
node_params : param list; (** Static parameters *)
node_params_constraints : size_constr list }
{ node_inputs : arg list;
node_outputs : arg list;
node_params : param list; (** Static parameters *)
node_params_constraints : size_constr list }
type field = { f_name : name; f_type : ty }
type structure = field list
@ -40,9 +40,9 @@ let types_of_arg_list l = List.map (fun ad -> ad.a_type) l
let mk_arg name ty =
{ a_type = ty; a_name = name }
let mk_param name =
let mk_param name =
{ p_name = name }
let print_param ff p = Names.print_name ff p.p_name

140
compiler/global/static.ml
View file

@ -6,9 +6,9 @@
x[n - 1], x[1 + 3],...
*)
open Names
open Format
type op = | SPlus | SMinus | STimes | SDiv
type size_exp =
@ -22,125 +22,125 @@ type size_constr =
(* unsatisfiable constraint *)
exception Instanciation_failed
exception Not_static
(** Returns the op from an operator full name. *)
let op_from_app_name n =
match n with
| Modname { qual = "Pervasives"; id = "+" } | Name "+" -> SPlus
| Modname { qual = "Pervasives"; id = "-" } | Name "-" -> SMinus
| Modname { qual = "Pervasives"; id = "*" } | Name "*" -> STimes
| Modname { qual = "Pervasives"; id = "/" } | Name "/" -> SDiv
| _ -> raise Not_static
| Modname { qual = "Pervasives"; id = "+" } | Name "+" -> SPlus
| Modname { qual = "Pervasives"; id = "-" } | Name "-" -> SMinus
| Modname { qual = "Pervasives"; id = "*" } | Name "*" -> STimes
| Modname { qual = "Pervasives"; id = "/" } | Name "/" -> SDiv
| _ -> raise Not_static
(** [simplify env e] returns e simplified with the
variables values taken from env (mapping vars to integers).
Variables are replaced with their values and every operator
that can be computed is replaced with the value of the result. *)
let rec simplify env =
function
| SConst n -> SConst n
| SVar id -> (try simplify env (NamesEnv.find id env) with | _ -> SVar id)
| SOp (op, e1, e2) ->
let e1 = simplify env e1 in
let e2 = simplify env e2
in
| SConst n -> SConst n
| SVar id -> (try simplify env (NamesEnv.find id env) with | _ -> SVar id)
| SOp (op, e1, e2) ->
let e1 = simplify env e1 in
let e2 = simplify env e2
in
(match (e1, e2) with
| (SConst n1, SConst n2) ->
let n =
(match op with
| SPlus -> n1 + n2
| SMinus -> n1 - n2
| STimes -> n1 * n2
| SDiv ->
if n2 = 0 then raise Instanciation_failed else n1 / n2)
in SConst n
| (_, _) -> SOp (op, e1, e2))
| (SConst n1, SConst n2) ->
let n =
(match op with
| SPlus -> n1 + n2
| SMinus -> n1 - n2
| STimes -> n1 * n2
| SDiv ->
if n2 = 0 then raise Instanciation_failed else n1 / n2)
in SConst n
| (_, _) -> SOp (op, e1, e2))
(** [int_of_size_exp env e] returns the value of the expression
[e] in the environment [env], mapping vars to integers. Raises
Instanciation_failed if it cannot be computed (if a var has no value).*)
let int_of_size_exp env e =
match simplify env e with | SConst n -> n | _ -> raise Instanciation_failed
(** [is_true env constr] returns whether the constraint is satisfied
in the environment (or None if this can be decided)
and a simplified constraint. *)
let is_true env =
function
| Equal (e1, e2) when e1 = e2 ->
((Some true), (Equal (simplify env e1, simplify env e2)))
| Equal (e1, e2) ->
let e1 = simplify env e1 in
let e2 = simplify env e2
in
| Equal (e1, e2) when e1 = e2 ->
((Some true), (Equal (simplify env e1, simplify env e2)))
| Equal (e1, e2) ->
let e1 = simplify env e1 in
let e2 = simplify env e2
in
(match (e1, e2) with
| (SConst n1, SConst n2) -> ((Some (n1 = n2)), (Equal (e1, e2)))
| (_, _) -> (None, (Equal (e1, e2))))
| LEqual (e1, e2) ->
let e1 = simplify env e1 in
let e2 = simplify env e2
in
| (SConst n1, SConst n2) -> ((Some (n1 = n2)), (Equal (e1, e2)))
| (_, _) -> (None, (Equal (e1, e2))))
| LEqual (e1, e2) ->
let e1 = simplify env e1 in
let e2 = simplify env e2
in
(match (e1, e2) with
| (SConst n1, SConst n2) -> ((Some (n1 <= n2)), (LEqual (e1, e2)))
| (_, _) -> (None, (LEqual (e1, e2))))
| False -> (None, False)
| (SConst n1, SConst n2) -> ((Some (n1 <= n2)), (LEqual (e1, e2)))
| (_, _) -> (None, (LEqual (e1, e2))))
| False -> (None, False)
exception Solve_failed of size_constr
(** [solve env constr_list solves a list of constraints. It
removes equations that can be decided and simplify others.
If one equation cannot be satisfied, it raises Solve_failed. ]*)
let rec solve const_env =
function
| [] -> []
| c :: l ->
let l = solve const_env l in
let (res, c) = is_true const_env c
in
| [] -> []
| c :: l ->
let l = solve const_env l in
let (res, c) = is_true const_env c
in
(match res with
| None -> c :: l
| Some v -> if not v then raise (Solve_failed c) else l)
| None -> c :: l
| Some v -> if not v then raise (Solve_failed c) else l)
(** Substitutes variables in the size exp with their value
in the map (mapping vars to size exps). *)
let rec size_exp_subst m =
function
| SVar n -> (try List.assoc n m with | Not_found -> SVar n)
| SOp (op, e1, e2) -> SOp (op, size_exp_subst m e1, size_exp_subst m e2)
| s -> s
| SVar n -> (try List.assoc n m with | Not_found -> SVar n)
| SOp (op, e1, e2) -> SOp (op, size_exp_subst m e1, size_exp_subst m e2)
| s -> s
(** Substitutes variables in the constraint list with their value
in the map (mapping vars to size exps). *)
let instanciate_constr m constr =
let replace_one m =
function
| Equal (e1, e2) -> Equal (size_exp_subst m e1, size_exp_subst m e2)
| LEqual (e1, e2) -> LEqual (size_exp_subst m e1, size_exp_subst m e2)
| False -> False
| Equal (e1, e2) -> Equal (size_exp_subst m e1, size_exp_subst m e2)
| LEqual (e1, e2) -> LEqual (size_exp_subst m e1, size_exp_subst m e2)
| False -> False
in List.map (replace_one m) constr
let op_to_string =
function | SPlus -> "+" | SMinus -> "-" | STimes -> "*" | SDiv -> "/"
let rec print_size_exp ff =
function
| SConst i -> fprintf ff "%d" i
| SVar id -> fprintf ff "%s" id
| SOp (op, e1, e2) ->
fprintf ff "@[(%a %s %a)@]"
print_size_exp e1 (op_to_string op) print_size_exp e2
| SConst i -> fprintf ff "%d" i
| SVar id -> fprintf ff "%s" id
| SOp (op, e1, e2) ->
fprintf ff "@[(%a %s %a)@]"
print_size_exp e1 (op_to_string op) print_size_exp e2
let print_size_constr ff = function
| Equal (e1, e2) ->
fprintf ff "@[%a = %a@]" print_size_exp e1 print_size_exp e2
| LEqual (e1, e2) ->
fprintf ff "@[%a <= %a@]" print_size_exp e1 print_size_exp e2
| False -> fprintf ff "False"
let psize_constr oc c =
let ff = formatter_of_out_channel oc
in (print_size_constr ff c; fprintf ff "@?")

4
compiler/global/types.ml
View file

@ -16,8 +16,6 @@ let invalid_type = Tprod []
let const_array_of ty n = Tarray (ty, SConst n)
open Pp_tools
open Format
@ -26,4 +24,4 @@ let rec print_type ff = function
fprintf ff "@[<hov2>%a@]" (print_list_r print_type "(" " *" ")") ty_list
| Tid id -> print_longname ff id
| Tarray (ty, n) ->
fprintf ff "@[<hov2>%a^%a@]" print_type ty print_size_exp n
fprintf ff "@[<hov2>%a^%a@]" print_type ty print_size_exp n

132
compiler/heptagon/analysis/causal.ml
View file

@ -43,17 +43,17 @@ type sc =
(* normalized constraints *)
type ac =
| Awrite of ident
| Aread of ident
| Alastread of ident
| Aseq of ac * ac
| Aand of ac * ac
| Atuple of ac list
| Awrite of ident
| Aread of ident
| Alastread of ident
| Aseq of ac * ac
| Aand of ac * ac
| Atuple of ac list
and nc =
| Aor of nc * nc
| Aac of ac
| Aempty
| Aor of nc * nc
| Aac of ac
| Aempty
let output_ac ff ac =
let rec print priority ff ac =
@ -61,22 +61,22 @@ let output_ac ff ac =
begin match ac with
| Aseq(ac1, ac2) ->
(if priority > 1
then fprintf ff "(%a@ < %a)"
else fprintf ff "%a@ < %a")
then fprintf ff "(%a@ < %a)"
else fprintf ff "%a@ < %a")
(print 1) ac1 (print 1) ac2
| Aand(ac1, ac2) ->
(if priority > 0
then fprintf ff "(%a || %a)"
else fprintf ff "%a || %a")
then fprintf ff "(%a || %a)"
else fprintf ff "%a || %a")
(print 0) ac1 (print 0) ac2
| Atuple(acs) ->
print_list_r (print 1) "(" "," ")" ff acs
print_list_r (print 1) "(" "," ")" ff acs
| Awrite(m) -> fprintf ff "%s" (name m)
| Aread(m) -> fprintf ff "^%s" (name m)
| Alastread(m) -> fprintf ff "last %s" (name m)
end;
fprintf ff "@]" in
fprintf ff "@[%a@]@?" (print 0) ac
fprintf ff "@[%a@]@?" (print 0) ac
type error = Ecausality_cycle of ac
@ -86,9 +86,9 @@ exception Error of error
let error kind = raise (Error(kind))
let message loc kind =
let output_ac oc ac =
let output_ac oc ac =
let ff = formatter_of_out_channel oc in output_ac ff ac in
begin match kind with
begin match kind with
| Ecausality_cycle(ac) ->
Printf.eprintf
"%aCausality error: the following constraint is not causal.\n%a\n."
@ -117,7 +117,7 @@ let rec cand nc1 nc2 =
| nc1, Aor(nc2, nc22) -> Aor(cand nc1 nc2, cand nc1 nc22)
| Aac(ac1), Aac(ac2) -> Aac(Aand(ac1, ac2))
let rec ctuple l =
let rec ctuple l =
let conv = function
| Cwrite(n) -> Awrite(n)
| Cread(n) -> Aread(n)
@ -128,10 +128,10 @@ let rec ctuple l =
| Cor _ -> Format.printf "Unexpected or\n"; assert false
| _ -> assert false
in
match l with
| [] -> []
| Cempty::l -> ctuple l
| v::l -> (conv v)::(ctuple l)
match l with
| [] -> []
| Cempty::l -> ctuple l
| v::l -> (conv v)::(ctuple l)
let rec norm = function
| Cor(c1, c2) -> cor (norm c1) (norm c2)
@ -152,9 +152,9 @@ let build ac =
| Awrite(n) ->
nametograph n g n_to_graph
| Atuple l ->
List.fold_left (associate_node g) n_to_graph l
| _ ->
n_to_graph
List.fold_left (associate_node g) n_to_graph l
| _ ->
n_to_graph
in
(* first build the association [n -> node] *)
@ -163,13 +163,13 @@ let build ac =
match ac with
| Aand(ac1, ac2) ->
let n_to_graph = initialize ac1 n_to_graph in
initialize ac2 n_to_graph
initialize ac2 n_to_graph
| Aseq(ac1, ac2) ->
let n_to_graph = initialize ac1 n_to_graph in
initialize ac2 n_to_graph
initialize ac2 n_to_graph
| _ ->
let g = make ac in
associate_node g n_to_graph ac
associate_node g n_to_graph ac
in
let make_graph ac n_to_graph =
@ -177,32 +177,32 @@ let build ac =
try
let g = Env.find n n_to_graph in add_depends node g
with
| Not_found -> () in
| Not_found -> () in
let rec add_dependence g = function
| Aread(n) -> attach g n
| _ -> ()
| Aread(n) -> attach g n
| _ -> ()
in
let rec node_for_ac ac =
let rec node_for_tuple = function
| [] -> raise Not_found
| v::l ->
(try
node_for_ac v
with
Not_found -> node_for_tuple l
)
in
match ac with
| Awrite n -> Env.find n n_to_graph
| Atuple l ->
begin try
node_for_tuple l
with Not_found
_ -> make ac
end
| _ -> make ac
| [] -> raise Not_found
| v::l ->
(try
node_for_ac v
with
Not_found -> node_for_tuple l
)
in
match ac with
| Awrite n -> Env.find n n_to_graph
| Atuple l ->
begin try
node_for_tuple l
with Not_found
_ -> make ac
end
| _ -> make ac
in
let rec make_graph ac =
@ -210,28 +210,28 @@ let build ac =
| Aand(ac1, ac2) ->
let top1, bot1 = make_graph ac1 in
let top2, bot2 = make_graph ac2 in
top1 @ top2, bot1 @ bot2
top1 @ top2, bot1 @ bot2
| Aseq(ac1, ac2) ->
let top1, bot1 = make_graph ac1 in
let top2, bot2 = make_graph ac2 in
(* add extra dependences *)
List.iter
(fun top -> List.iter (fun bot -> add_depends top bot) bot1)
top2;
top1 @ top2, bot1 @ bot2
| Awrite(n) -> let g = Env.find n n_to_graph in [g], [g]
| Aread(n) -> let g = make ac in attach g n; [g], [g]
| Atuple(l) ->
let g = node_for_ac ac in
List.iter (add_dependence g) l;
[g], [g]
(* add extra dependences *)
List.iter
(fun top -> List.iter (fun bot -> add_depends top bot) bot1)
top2;
top1 @ top2, bot1 @ bot2
| Awrite(n) -> let g = Env.find n n_to_graph in [g], [g]
| Aread(n) -> let g = make ac in attach g n; [g], [g]
| Atuple(l) ->
let g = node_for_ac ac in
List.iter (add_dependence g) l;
[g], [g]
| _ -> [], [] in
let top_list, bot_list = make_graph ac in
graph top_list bot_list in
graph top_list bot_list in
let n_to_graph = initialize ac Env.empty in
let g = make_graph ac n_to_graph in
g
g
(* the main entry. *)
let check loc c =
@ -247,7 +247,7 @@ let check loc c =
| Aor(nc1, nc2) -> check nc1; check nc2 in
let nc = norm c in
try
check nc
with
| Error(kind) -> message loc kind
try
check nc
with
| Error(kind) -> message loc kind

149
compiler/heptagon/analysis/causality.ml
View file

@ -12,7 +12,7 @@
(* $Id: causality.ml 615 2009-11-20 17:43:14Z pouzet $ *)
open Misc
open Names
open Names
open Ident
open Heptagon
open Location
@ -24,35 +24,35 @@ let is_empty c = (c = cempty)
let cand c1 c2 =
match c1, c2 with
| Cempty, _ -> c2 | _, Cempty -> c1
| c1, c2 -> Cand(c1, c2)
| Cempty, _ -> c2 | _, Cempty -> c1
| c1, c2 -> Cand(c1, c2)
let rec candlist l =
match l with
| [] -> Cempty
| c1 :: l -> cand c1 (candlist l)
| [] -> Cempty
| c1 :: l -> cand c1 (candlist l)
let ctuplelist l =
Ctuple l
let cor c1 c2 =
match c1, c2 with
| Cempty, Cempty -> Cempty
| _ -> Cor(c1, c2)
| Cempty, Cempty -> Cempty
| _ -> Cor(c1, c2)
let rec corlist l =
match l with
| [] -> Cempty
| [c1] -> c1
| c1 :: l -> cor c1 (corlist l)
| [] -> Cempty
| [c1] -> c1
| c1 :: l -> cor c1 (corlist l)
let cseq c1 c2 =
match c1, c2 with
| Cempty, _ -> c2
| _, Cempty -> c1
| c1, c2 -> Cseq(c1, c2)
| Cempty, _ -> c2
| _, Cempty -> c1
| c1, c2 -> Cseq(c1, c2)
let rec cseqlist l =
match l with
| [] -> Cempty
| c1 :: l -> cseq c1 (cseqlist l)
| [] -> Cempty
| c1 :: l -> cseq c1 (cseqlist l)
let read x = Cread(x)
let lastread x = Clastread(x)
@ -71,27 +71,28 @@ let rec pre = function
let clear env c =
let rec clearec c =
match c with
| Cor(c1, c2) ->
let c1 = clearec c1 in
let c2 = clearec c2 in
cor c1 c2
| Cand(c1, c2) ->
let c1 = clearec c1 in
let c2 = clearec c2 in
cand c1 c2
| Cseq(c1, c2) ->
let c1 = clearec c1 in
let c2 = clearec c2 in
cseq c1 c2
| Ctuple l -> Ctuple (List.map clearec l)
| Cwrite(id) | Cread(id) | Clastread(id) ->
if IdentSet.mem id env then Cempty else c
| Cempty -> c in
| Cor(c1, c2) ->
let c1 = clearec c1 in
let c2 = clearec c2 in
cor c1 c2
| Cand(c1, c2) ->
let c1 = clearec c1 in
let c2 = clearec c2 in
cand c1 c2
| Cseq(c1, c2) ->
let c1 = clearec c1 in
let c2 = clearec c2 in
cseq c1 c2
| Ctuple l -> Ctuple (List.map clearec l)
| Cwrite(id) | Cread(id) | Clastread(id) ->
if IdentSet.mem id env then Cempty else c
| Cempty -> c in
clearec c
let build dec =
List.fold_left (fun acc { v_name = n } -> IdentSet.add n acc) IdentSet.empty dec
let build dec =
let add acc { v_name = n; } = IdentSet.add n acc in
List.fold_left add IdentSet.empty dec
(** Main typing function *)
let rec typing e =
match e.e_desc with
@ -100,51 +101,51 @@ let rec typing e =
| Evar(x) -> read x
| Elast(x) -> lastread x
| Etuple(e_list) ->
candlist (List.map typing e_list)
candlist (List.map typing e_list)
| Eapp({a_op = op}, e_list) -> apply op e_list
| Efield(e1, _) -> typing e1
| Estruct(l) ->
let l = List.map (fun (_, e) -> typing e) l in
candlist l
let l = List.map (fun (_, e) -> typing e) l in
candlist l
| Earray(e_list) ->
candlist (List.map typing e_list)
candlist (List.map typing e_list)
(** Typing an application *)
and apply op e_list =
match op, e_list with
| Epre(_), [e] -> pre (typing e)
| Efby, [e1;e2] ->
let t1 = typing e1 in
let t2 = pre (typing e2) in
candlist [t1; t2]
let t1 = typing e1 in
let t2 = pre (typing e2) in
candlist [t1; t2]
| Earrow, [e1;e2] ->
let t1 = typing e1 in
let t2 = typing e2 in
candlist [t1; t2]
let t1 = typing e1 in
let t2 = typing e2 in
candlist [t1; t2]
| Eifthenelse, [e1; e2; e3] ->
let t1 = typing e1 in
let i2 = typing e2 in
let i3 = typing e3 in
cseq t1 (cor i2 i3)
let t1 = typing e1 in
let i2 = typing e2 in
let i3 = typing e3 in
cseq t1 (cor i2 i3)
| Ecall _, e_list ->
ctuplelist (List.map typing e_list)
ctuplelist (List.map typing e_list)
| Efield_update _, [e1;e2] ->
let t1 = typing e1 in
let t2 = typing e2 in
cseq t2 t1
let t1 = typing e1 in
let t2 = typing e2 in
cseq t2 t1
| Earray_op op, e_list ->
apply_array_op op e_list
and apply_array_op op e_list =
match op, e_list with
| (Eiterator (_, _, _) | Econcat | Eselect_slice
| Eselect_dyn | Eselect _ | Erepeat), e_list ->
match op, e_list with
| (Eiterator (_, _, _) | Econcat | Eselect_slice
| Eselect_dyn | Eselect _ | Erepeat), e_list ->
ctuplelist (List.map typing e_list)
| Eupdate _, [e1;e2] ->
let t1 = typing e1 in
let t2 = typing e2 in
cseq t2 t1
let t1 = typing e1 in
let t2 = typing e2 in
cseq t2 t1
let rec typing_pat = function
| Evarpat(x) -> cwrite(x)
| Etuplepat(pat_list) ->
@ -157,13 +158,13 @@ and typing_eq eq =
match eq.eq_desc with
| Eautomaton(handlers) -> typing_automaton handlers
| Eswitch(e, handlers) ->
cseq (typing e) (typing_switch handlers)
| Epresent(handlers, b) ->
typing_present handlers b
cseq (typing e) (typing_switch handlers)
| Epresent(handlers, b) ->
typing_present handlers b
| Ereset(eq_list, e) ->
cseq (typing e) (typing_eqs eq_list)
cseq (typing e) (typing_eqs eq_list)
| Eeq(pat, e) ->
cseq (typing e) (typing_pat pat)
cseq (typing e) (typing_pat pat)
and typing_switch handlers =
let handler { w_block = b } = typing_block b in
@ -176,7 +177,7 @@ and typing_present handlers b =
and typing_automaton state_handlers =
(* typing the body of the automaton *)
let handler
let handler
{ s_state = _; s_block = b; s_until = suntil; s_unless = sunless } =
let escape { e_cond = e } = typing e in
@ -196,17 +197,17 @@ and typing_block { b_local = dec; b_equs = eq_list; b_loc = loc } =
let typing_contract loc contract =
match contract with
| None -> cempty
| Some { c_local = l_list; c_eq = eq_list; c_assume = e_a;
c_enforce = e_g; c_controllables = c_list } ->
let teq = typing_eqs eq_list in
let t_contract = cseq (typing e_a) (cseq teq (typing e_g)) in
Causal.check loc t_contract;
let t_contract = clear (build l_list) t_contract in
t_contract
| Some { c_local = l_list; c_eq = eq_list; c_assume = e_a;
c_enforce = e_g; c_controllables = c_list } ->
let teq = typing_eqs eq_list in
let t_contract = cseq (typing e_a) (cseq teq (typing e_g)) in
Causal.check loc t_contract;
let t_contract = clear (build l_list) t_contract in
t_contract
let typing_node { n_name = f; n_input = i_list; n_output = o_list;
n_contract = contract;
n_local = l_list; n_equs = eq_list; n_loc = loc } =
n_contract = contract;
n_local = l_list; n_equs = eq_list; n_loc = loc } =
let _ = typing_contract loc contract in
let teq = typing_eqs eq_list in
Causal.check loc teq

166
compiler/heptagon/analysis/initialization.ml
View file

@ -21,19 +21,19 @@ open Location
open Format
type typ =
| Iproduct of typ list
| Ileaf of init
| Iproduct of typ list
| Ileaf of init
and init =
{ mutable i_desc: init_desc;
mutable i_index: int }
and init_desc =
| Izero
| Ione
| Ivar
| Imax of init * init
| Ilink of init
| Izero
| Ione
| Ivar
| Imax of init * init
| Ilink of init
type kind = | Last of init | Var
@ -112,17 +112,17 @@ and iless left_i right_i =
else
match left_i.i_desc, right_i.i_desc with
| (Izero, _) | (_, Ione) -> ()
| _, Izero -> initialized left_i
| Imax(i1, i2), _ ->
iless i1 right_i; iless i2 right_i
| _, Ivar ->
let left_i = occur_check right_i.i_index left_i in
right_i.i_desc <- Ilink(left_i)
| _, Imax(i1, i2) ->
let i1 = occur_check left_i.i_index i1 in
let i2 = occur_check left_i.i_index i2 in
right_i.i_desc <- Ilink(imax left_i (imax i1 i2))
| _ -> raise Unify
| _, Izero -> initialized left_i
| Imax(i1, i2), _ ->
iless i1 right_i; iless i2 right_i
| _, Ivar ->
let left_i = occur_check right_i.i_index left_i in
right_i.i_desc <- Ilink(left_i)
| _, Imax(i1, i2) ->
let i1 = occur_check left_i.i_index i1 in
let i2 = occur_check left_i.i_index i2 in
right_i.i_desc <- Ilink(imax left_i (imax i1 i2))
| _ -> raise Unify
(* an inequation [a < t[a]] becomes [a = t[0]] *)
and occur_check index i =
@ -130,18 +130,18 @@ and occur_check index i =
| Izero | Ione -> i
| Ivar -> if i.i_index = index then izero else i
| Imax(i1, i2) ->
max (occur_check index i1) (occur_check index i2)
max (occur_check index i1) (occur_check index i2)
| Ilink(i) -> occur_check index i
module Printer = struct
open Format
let rec print_list_r print po sep pf ff = function
| [] -> ()
| x :: l ->
fprintf ff "@[%s%a" po print x;
List.iter (fprintf ff "%s@]@ @[%a" sep print) l;
fprintf ff "%s@]" pf
| [] -> ()
| x :: l ->
fprintf ff "@[%s%a" po print x;
List.iter (fprintf ff "%s@]@ @[%a" sep print) l;
fprintf ff "%s@]" pf
let rec fprint_init ff i = match i.i_desc with
| Izero -> fprintf ff "0"
@ -173,13 +173,13 @@ module Error = struct
let message loc kind =
begin match kind with
| Eclash(left_ty, right_ty) ->
Printf.eprintf "%aInitialization error: this expression has type \
| Eclash(left_ty, right_ty) ->
Printf.eprintf "%aInitialization error: this expression has type \
%a, \n\
but is expected to have type %a\n"
output_location loc
Printer.output_typ left_ty
Printer.output_typ right_ty
output_location loc
Printer.output_typ left_ty
Printer.output_typ right_ty
end;
raise Misc.Error
end
@ -195,49 +195,49 @@ let rec typing h e =
| Econst _ | Econstvar _ -> leaf izero
| Evar(x) | Elast(x) -> let { i_typ = i } = Env.find x h in leaf i
| Etuple(e_list) ->
product (List.map (typing h) e_list)
product (List.map (typing h) e_list)
| Eapp({a_op = op}, e_list) ->
let i = apply h op e_list in
skeleton i e.e_ty
let i = apply h op e_list in
skeleton i e.e_ty
| Efield(e1, _) ->
let i = itype (typing h e1) in
skeleton i e.e_ty
let i = itype (typing h e1) in
skeleton i e.e_ty
| Estruct(l) ->
let i =
List.fold_left
(fun acc (_, e) -> max acc (itype (typing h e))) izero l in
skeleton i e.e_ty
let i =
List.fold_left
(fun acc (_, e) -> max acc (itype (typing h e))) izero l in
skeleton i e.e_ty
| Earray(e_list) ->
let i =
List.fold_left
(fun acc e -> max acc (itype (typing h e))) izero e_list in
skeleton i e.e_ty
let i =
List.fold_left
(fun acc e -> max acc (itype (typing h e))) izero e_list in
skeleton i e.e_ty
(** Typing an application *)
and apply h op e_list =
match op, e_list with
| Epre(None), [e] ->
initialized_exp h e;
ione
initialized_exp h e;
ione
| Epre(Some _), [e] ->
initialized_exp h e;
izero
initialized_exp h e;
izero
| Efby, [e1;e2] ->
initialized_exp h e2;
itype (typing h e1)
initialized_exp h e2;
itype (typing h e1)
| Earrow, [e1;e2] ->
let ty1 = typing h e1 in
let _ = typing h e2 in
itype ty1
let ty1 = typing h e1 in
let _ = typing h e2 in
itype ty1
| Eifthenelse, [e1; e2; e3] ->
let i1 = itype (typing h e1) in
let i2 = itype (typing h e2) in
let i3 = itype (typing h e3) in
max i1 (max i2 i3)
| Ecall ({ op_kind = Eop }, _), e_list ->
let i1 = itype (typing h e1) in
let i2 = itype (typing h e2) in
let i3 = itype (typing h e3) in
max i1 (max i2 i3)
| Ecall ({ op_kind = Eop }, _), e_list ->
List.fold_left (fun acc e -> itype (typing h e)) izero e_list
| (Ecall _ | Earray_op _| Efield_update _) , e_list ->
List.iter (fun e -> initialized_exp h e) e_list; izero
List.iter (fun e -> initialized_exp h e) e_list; izero
and expect h e expected_ty =
let actual_ty = typing h e in
@ -257,15 +257,15 @@ and typing_eq h eq =
match eq.eq_desc with
| Eautomaton(handlers) -> typing_automaton h handlers
| Eswitch(e, handlers) ->
initialized_exp h e;
typing_switch h handlers
initialized_exp h e;
typing_switch h handlers
| Epresent(handlers, b) ->
typing_present h handlers b
typing_present h handlers b
| Ereset(eq_list, e) ->
initialized_exp h e; typing_eqs h eq_list
initialized_exp h e; typing_eqs h eq_list
| Eeq(pat, e) ->
let ty_pat = typing_pat h pat in
expect h e ty_pat
let ty_pat = typing_pat h pat in
expect h e ty_pat
and typing_switch h handlers =
let handler { w_block = b } = ignore (typing_block h b) in
@ -286,12 +286,12 @@ and typing_automaton h state_handlers =
let initialized h { s_block = { b_defnames = l } } =
Env.fold
(fun elt _ h ->
let { i_kind = k; i_typ = i } = Env.find elt h in
match k with
| Last _ ->
let h = Env.remove elt h in
Env.add elt { i_kind = Last(izero); i_typ = izero } h
| _ -> h)
let { i_kind = k; i_typ = i } = Env.find elt h in
match k with
| Last _ ->
let h = Env.remove elt h in
Env.add elt { i_kind = Last(izero); i_typ = izero } h
| _ -> h)
l h in
(* typing the body of the automaton *)
@ -306,9 +306,9 @@ and typing_automaton h state_handlers =
List.iter (escape h) sunless in
match state_handlers with
(* we do a special treatment for state variables which *)
(* are defined in the initial state if it cannot be immediately *)
(* exited *)
(* we do a special treatment for state variables which *)
(* are defined in the initial state if it cannot be immediately *)
(* exited *)
| initial :: other_handlers when weak initial ->
let h = initialized h initial in
handler h initial;
@ -337,19 +337,19 @@ let typing_contract h contract =
match contract with
| None -> h
| Some { c_local = l_list; c_eq = eq_list; c_assume = e_a;
c_enforce = e_g; c_controllables = c_list } ->
let h = sbuild h c_list in
let h' = build h l_list in
typing_eqs h' eq_list;
(* assumption *)
expect h' e_a (skeleton izero e_a.e_ty);
(* property *)
expect h' e_g (skeleton izero e_g.e_ty);
h
c_enforce = e_g; c_controllables = c_list } ->
let h = sbuild h c_list in
let h' = build h l_list in
typing_eqs h' eq_list;
(* assumption *)
expect h' e_a (skeleton izero e_a.e_ty);
(* property *)
expect h' e_g (skeleton izero e_g.e_ty);
h
let typing_node { n_name = f; n_input = i_list; n_output = o_list;
n_contract = contract;
n_local = l_list; n_equs = eq_list } =
n_contract = contract;
n_local = l_list; n_equs = eq_list } =
let h = sbuild Env.empty i_list in
let h = sbuild h o_list in
let h = typing_contract h contract in

118
compiler/heptagon/analysis/interface.ml
View file

@ -18,84 +18,84 @@ open Pp_tools
open Types
module Type =
struct
let sigtype { sig_name = name; sig_inputs = i_list;
sig_outputs = o_list; sig_params = params } =
let check_arg a = { a with a_type = check_type a.a_type } in
name, { node_inputs = List.map check_arg i_list;
node_outputs = List.map check_arg o_list;
node_params = params;
node_params_constraints = []; }
let read { interf_desc = desc; interf_loc = loc } =
try
match desc with
| Iopen(n) -> open_module n
| Itypedef(tydesc) -> deftype NamesEnv.empty tydesc
| Isignature(s) ->
let name, s = sigtype s in
add_value name s
with
TypingError(error) -> message loc error
let main l =
List.iter read l
end
struct
let sigtype { sig_name = name; sig_inputs = i_list;
sig_outputs = o_list; sig_params = params } =
let check_arg a = { a with a_type = check_type a.a_type } in
name, { node_inputs = List.map check_arg i_list;
node_outputs = List.map check_arg o_list;
node_params = params;
node_params_constraints = []; }
let read { interf_desc = desc; interf_loc = loc } =
try
match desc with
| Iopen(n) -> open_module n
| Itypedef(tydesc) -> deftype NamesEnv.empty tydesc
| Isignature(s) ->
let name, s = sigtype s in
add_value name s
with
TypingError(error) -> message loc error
let main l =
List.iter read l
end
module Printer =
struct
open Format
open Hept_printer
let deftype ff name tdesc =
match tdesc with
| Tabstract -> fprintf ff "@[type %s@.@]" name
| Tenum(tag_name_list) ->
fprintf ff "@[<hov 2>type %s = " name;
print_list_r print_name "" " |" "" ff tag_name_list;
fprintf ff "@.@]"
fprintf ff "@[<hov 2>type %s = " name;
print_list_r print_name "" " |" "" ff tag_name_list;
fprintf ff "@.@]"
| Tstruct(f_ty_list) ->
fprintf ff "@[<hov 2>type %s = " name;
fprintf ff "@[<hov 1>";
print_list_r
(fun ff { f_name = field; f_type = ty } -> print_name ff field;
fprintf ff "@[<hov 2>type %s = " name;
fprintf ff "@[<hov 1>";
print_list_r
(fun ff { f_name = field; f_type = ty } -> print_name ff field;
fprintf ff ": ";
print_type ff ty) "{" ";" "}" ff f_ty_list;
fprintf ff "@]@.@]"
print_type ff ty) "{" ";" "}" ff f_ty_list;
fprintf ff "@]@.@]"
let signature ff name { node_inputs = inputs;
node_outputs = outputs;
node_params = params;
node_params_constraints = constr } =
node_outputs = outputs;
node_params = params;
node_params_constraints = constr } =
let print ff arg =
match arg.a_name with
| None -> print_type ff arg.a_type
| Some(name) ->
print_name ff name; fprintf ff ":"; print_type ff arg.a_type
| None -> print_type ff arg.a_type
| Some(name) ->
print_name ff name; fprintf ff ":"; print_type ff arg.a_type
in
let print_node_params ff = function
| [] -> ()
| l -> print_list_r print_name "<<" "," ">>" ff l
in
fprintf ff "@[<v 2>val ";
print_name ff name;
print_node_params ff (List.map (fun p -> p.p_name) params);
fprintf ff "@[";
print_list_r print "(" ";" ")" ff inputs;
fprintf ff "@] returns @[";
print_list_r print "(" ";" ")" ff outputs;
fprintf ff "@]";
(match constr with
| [] -> ()
| constr ->
fprintf ff "\n with: @[";
print_list_r Static.print_size_constr "" "," "" ff constr;
fprintf ff "@]"
);
fprintf ff "@.@]"
in
fprintf ff "@[<v 2>val ";
print_name ff name;
print_node_params ff (List.map (fun p -> p.p_name) params);
fprintf ff "@[";
print_list_r print "(" ";" ")" ff inputs;
fprintf ff "@] returns @[";
print_list_r print "(" ";" ")" ff outputs;
fprintf ff "@]";
(match constr with
| [] -> ()
| constr ->
fprintf ff "\n with: @[";
print_list_r Static.print_size_constr "" "," "" ff constr;
fprintf ff "@]"
);
fprintf ff "@.@]"
let print oc =
let ff = formatter_of_out_channel oc in
NamesEnv.iter (fun key typdesc -> deftype ff key typdesc) current.types;

1046
compiler/heptagon/analysis/typing.ml
View file

File diff suppressed because it is too large Load diff

134
compiler/heptagon/hept_printer.ml
View file

@ -20,8 +20,8 @@ open Pp_tools
open Types
open Signature
let iterator_to_string i =
match i with
let iterator_to_string i =
match i with
| Imap -> "map"
| Ifold -> "fold"
| Imapfold -> "mapfold"
@ -98,79 +98,79 @@ and print_op ff op e_list =
fprintf ff "@]"
| Ecall({ op_name = f; op_params = params }, reset), e_list ->
print_longname ff f;
print_call_params ff params;
print_call_params ff params;
print_exps ff e_list;
(match reset with
| None -> ()
| Some r -> fprintf ff " every %a" print_exp r
)
| Efield_update f, [e1;e2] ->
fprintf ff "(@[";
print_exp ff e1;
fprintf ff " with .";
print_longname ff f;
fprintf ff " = ";
print_exp ff e2;
fprintf ff ")@]"
(match reset with
| None -> ()
| Some r -> fprintf ff " every %a" print_exp r
)
| Efield_update f, [e1;e2] ->
fprintf ff "(@[";
print_exp ff e1;
fprintf ff " with .";
print_longname ff f;
fprintf ff " = ";
print_exp ff e2;
fprintf ff ")@]"
| Earray_op op, e_list ->
print_array_op ff op e_list
and print_array_op ff op e_list =
and print_array_op ff op e_list =
match op, e_list with
| Erepeat, [e1; e2] ->
print_exp ff e1;
fprintf ff "^";
print_exp ff e2
| Eselect idx_list, [e] ->
print_exp ff e;
print_list_r print_size_exp "[" "][" "]" ff idx_list
print_exp ff e1;
fprintf ff "^";
print_exp ff e2
| Eselect idx_list, [e] ->
print_exp ff e;
print_list_r print_size_exp "[" "][" "]" ff idx_list
| Eselect_dyn, e::defe::idx_list ->
fprintf ff "@[(";
print_exp ff e;
print_list_r print_exp "[" "][" "] default " ff idx_list;
print_exp ff defe;
fprintf ff ")@]"
fprintf ff "@[(";
print_exp ff e;
print_list_r print_exp "[" "][" "] default " ff idx_list;
print_exp ff defe;
fprintf ff ")@]"
| Eupdate idx_list, [e1;e2] ->
fprintf ff "(@[";
print_exp ff e1;
fprintf ff " with ";
print_list_r print_size_exp "[" "][" "]" ff idx_list;
fprintf ff " = ";
print_exp ff e2;
fprintf ff ")@]"
fprintf ff "(@[";
print_exp ff e1;
fprintf ff " with ";
print_list_r print_size_exp "[" "][" "]" ff idx_list;
fprintf ff " = ";
print_exp ff e2;
fprintf ff ")@]"
| Eselect_slice, [e; idx1; idx2] ->
print_exp ff e;
fprintf ff "[";
print_exp ff idx1;
fprintf ff "..";
print_exp ff idx2;
fprintf ff "]"
| Eiterator (it, { op_name = op; op_params = params } , reset), e::e_list ->
fprintf ff "(";
print_iterator ff it;
fprintf ff " ";
(match params with
| [] -> print_longname ff op
| l ->
fprintf ff "(";
print_longname ff op;
print_call_params ff params;
fprintf ff ")"
);
fprintf ff " <<";
print_exp ff e;
fprintf ff ">>) ";
print_exps ff e_list;
(match reset with
| None -> ()
| Some r -> fprintf ff " every %a" print_exp r
)
| Econcat, [e1;e2] ->
fprintf ff "@[";
print_exp ff e1;
fprintf ff " @@ ";
print_exp ff e2;
fprintf ff "@]"
print_exp ff e;
fprintf ff "[";
print_exp ff idx1;
fprintf ff "..";
print_exp ff idx2;
fprintf ff "]"
| Eiterator (it, { op_name = op; op_params = params } , reset), e::e_list ->
fprintf ff "(";
print_iterator ff it;
fprintf ff " ";
(match params with
| [] -> print_longname ff op
| l ->
fprintf ff "(";
print_longname ff op;
print_call_params ff params;
fprintf ff ")"
);
fprintf ff " <<";
print_exp ff e;
fprintf ff ">>) ";
print_exps ff e_list;
(match reset with
| None -> ()
| Some r -> fprintf ff " every %a" print_exp r
)
| Econcat, [e1;e2] ->
fprintf ff "@[";
print_exp ff e1;
fprintf ff " @@ ";
print_exp ff e2;
fprintf ff "@]"
let rec print_eq ff eq =
match eq.eq_desc with
@ -350,7 +350,7 @@ let print_open_module ff name =
let ptype oc ty =
let ff = formatter_of_out_channel oc in
print_type ff ty; fprintf ff "@?"
print_type ff ty; fprintf ff "@?"
let print oc { p_opened = po; p_types = pt; p_nodes = pn; p_consts = pc } =
let ff = formatter_of_out_channel oc in

178
compiler/heptagon/heptagon.ml
View file

@ -10,20 +10,20 @@
open Location
open Misc
open Names
open Ident
open Ident
open Static
open Signature
open Types
type iterator_type =
type iterator_type =
| Imap
| Ifold
| Imapfold
type exp =
{ e_desc : desc; e_ty : ty; e_loc : location }
{ e_desc : desc; e_ty : ty; e_loc : location }
and desc =
and desc =
| Econst of const
| Evar of ident
| Econstvar of name
@ -34,20 +34,20 @@ type exp =
| Estruct of (longname * exp) list
| Earray of exp list
and app =
{ a_op : op; }
and app =
{ a_op : op; }
and op =
and op =
| Epre of const option
| Efby
| Earrow
| Eifthenelse
| Earray_op of array_op
| Efield_update of longname
| Ecall of op_desc * exp option (** [op_desc] is the function called
[exp option] is the optional reset condition *)
| Ecall of op_desc * exp option (** [op_desc] is the function called [exp
option] is the optional reset condition *)
and array_op =
and array_op =
| Erepeat
| Eselect of size_exp list
| Eselect_dyn
@ -56,112 +56,114 @@ type exp =
| Econcat
| Eiterator of iterator_type * op_desc * exp option (** [op_desc] node to map
[exp option] reset *)
and op_desc = { op_name : longname; op_params: size_exp list; op_kind: op_kind }
and op_kind = | Eop | Enode
and const =
and op_desc = { op_name : longname; op_params: size_exp list; op_kind: op_kind }
and op_kind = | Eop | Enode
and const =
| Cint of int
| Cfloat of float
| Cconstr of longname
| Carray of size_exp * const
and pat =
and pat =
| Etuplepat of pat list | Evarpat of ident
type eq =
{ eq_desc : eqdesc; eq_statefull : bool; eq_loc : location }
{ eq_desc : eqdesc; eq_statefull : bool; eq_loc : location }
and eqdesc =
and eqdesc =
| Eautomaton of state_handler list
| Eswitch of exp * switch_handler list
| Epresent of present_handler list * block
| Ereset of eq list * exp
| Eeq of pat * exp
and block =
{ b_local : var_dec list; b_equs : eq list; mutable b_defnames : ty Env.t;
mutable b_statefull : bool; b_loc : location
}
and block = {
b_local : var_dec list; b_equs : eq list; mutable b_defnames : ty Env.t;
mutable b_statefull : bool; b_loc : location
}
and state_handler =
{ s_state : name; s_block : block; s_until : escape list;
s_unless : escape list
}
and state_handler = {
s_state : name; s_block : block; s_until : escape list;
s_unless : escape list
}
and escape =
{ e_cond : exp; e_reset : bool; e_next_state : name
}
and escape = {
e_cond : exp; e_reset : bool; e_next_state : name
}
and switch_handler =
{ w_name : longname; w_block : block
}
and switch_handler = {
w_name : longname; w_block : block
}
and present_handler =
{ p_cond : exp; p_block : block
}
and present_handler = {
p_cond : exp; p_block : block
}
and var_dec =
{ v_name : ident; mutable v_type : ty; v_last : last; v_loc : location }
and var_dec = {
v_name : ident; mutable v_type : ty; v_last : last; v_loc : location
}
and last =
and last =
| Var | Last of const option
type type_dec =
{ t_name : name; t_desc : type_desc; t_loc : location }
type type_dec = {
t_name : name; t_desc : type_desc; t_loc : location
}
and type_desc =
and type_desc =
| Type_abs | Type_enum of name list | Type_struct of structure
type contract =
{ c_assume : exp; c_enforce : exp; c_controllables : var_dec list;
c_local : var_dec list; c_eq : eq list
}
type contract = {
c_assume : exp; c_enforce : exp; c_controllables : var_dec list;
c_local : var_dec list; c_eq : eq list
}
type node_dec =
{ n_name : name; n_statefull : bool; n_input : var_dec list;
n_output : var_dec list; n_local : var_dec list;
n_contract : contract option; n_equs : eq list; n_loc : location;
n_params : param list;
n_params_constraints : size_constr list
}
type node_dec = {
n_name : name; n_statefull : bool; n_input : var_dec list;
n_output : var_dec list; n_local : var_dec list;
n_contract : contract option; n_equs : eq list; n_loc : location;
n_params : param list;
n_params_constraints : size_constr list
}
type const_dec =
{ c_name : name; c_type : ty; c_value : size_exp; c_loc : location }
type const_dec = {
c_name : name; c_type : ty; c_value : size_exp; c_loc : location }
type program =
{ p_pragmas : (name * string) list; p_opened : name list;
p_types : type_dec list; p_nodes : node_dec list;
p_consts : const_dec list
}
type program = {
p_pragmas : (name * string) list; p_opened : name list;
p_types : type_dec list; p_nodes : node_dec list;
p_consts : const_dec list
}
type signature =
{ sig_name : name; sig_inputs : arg list;
sig_outputs : arg list; sig_params : param list
}
type signature = {
sig_name : name; sig_inputs : arg list;
sig_outputs : arg list; sig_params : param list
}
type interface =
interface_decl list
interface_decl list
and interface_decl =
{ interf_desc : interface_desc; interf_loc : location
}
and interface_decl = {
interf_desc : interface_desc; interf_loc : location
}
and interface_desc =
and interface_desc =
| Iopen of name | Itypedef of type_dec | Isignature of signature
(* Helper functions to create AST. *)
let mk_exp desc ty =
{ e_desc = desc; e_ty = ty; e_loc = no_location; }
let mk_op op = { a_op = op; }
let mk_op_desc ln params kind =
{ op_name = ln; op_params = params; op_kind = kind }
let mk_type_dec name desc =
let mk_type_dec name desc =
{ t_name = name; t_desc = desc; t_loc = no_location; }
let mk_equation ?(statefull = true) desc =
{ eq_desc = desc; eq_statefull = statefull; eq_loc = no_location; }
@ -175,40 +177,40 @@ let mk_block ?(statefull = true) defnames eqs =
let dfalse = mk_exp (Econst (Cconstr Initial.pfalse)) (Tid Initial.pbool)
let dtrue = mk_exp (Econst (Cconstr Initial.ptrue)) (Tid Initial.pbool)
let mk_ifthenelse e1 e2 e3 =
{ e3 with e_desc = Eapp(mk_op Eifthenelse, [e1; e2; e3]) }
let mk_simple_equation pat e =
mk_equation ~statefull:false (Eeq(pat, e))
let mk_switch_equation ?(statefull = true) e l =
let mk_switch_equation ?(statefull = true) e l =
mk_equation ~statefull:statefull (Eswitch (e, l))
(** @return a size exp operator from a Heptagon operator. *)
let op_from_app app =
match app.a_op with
| Ecall ( { op_name = op; op_kind = Eop }, _) -> op_from_app_name op
| _ -> raise Not_static
| Ecall ( { op_name = op; op_kind = Eop }, _) -> op_from_app_name op
| _ -> raise Not_static
(** Translates a Heptagon exp into a static size exp. *)
let rec size_exp_of_exp e =
match e.e_desc with
| Econstvar n -> SVar n
| Econst (Cint i) -> SConst i
| Eapp (app, [ e1; e2 ]) ->
let op = op_from_app app
in SOp (op, size_exp_of_exp e1, size_exp_of_exp e2)
| _ -> raise Not_static
| Econstvar n -> SVar n
| Econst (Cint i) -> SConst i
| Eapp (app, [ e1; e2 ]) ->
let op = op_from_app app
in SOp (op, size_exp_of_exp e1, size_exp_of_exp e2)
| _ -> raise Not_static
(** @return the set of variables defined in [pat]. *)
let vars_pat pat =
let rec _vars_pat locals acc = function
| Evarpat x ->
if (IdentSet.mem x locals) or (IdentSet.mem x acc)
then acc
else IdentSet.add x acc
| Etuplepat pat_list -> List.fold_left (_vars_pat locals) acc pat_list
| Evarpat x ->
if (IdentSet.mem x locals) or (IdentSet.mem x acc)
then acc
else IdentSet.add x acc
| Etuplepat pat_list -> List.fold_left (_vars_pat locals) acc pat_list
in _vars_pat IdentSet.empty IdentSet.empty pat

46
compiler/heptagon/main/hept_compiler.ml
View file

@ -12,36 +12,36 @@ open Compiler_utils
let compile_impl pp p =
(* Typing *)
let p = do_pass Typing.program "Typing" p pp true in
if !print_types then Interface.Printer.print stdout;
(* Causality check *)
let p = do_silent_pass Causality.program "Causality check" p true in
(* Initialization check *)
let p =
do_silent_pass Initialization.program "Initialization check" p !init in
(* Completion of partial definitions *)
let p = do_pass Completion.program "Completion" p pp true in
if !print_types then Interface.Printer.print stdout;
(* Automata *)
let p = do_pass Automata.program "Automata" p pp true in
(* Causality check *)
let p = do_silent_pass Causality.program "Causality check" p true in
(* Present *)
let p = do_pass Present.program "Present" p pp true in
(* Initialization check *)
let p =
do_silent_pass Initialization.program "Initialization check" p !init in
(* Shared variables (last) *)
let p = do_pass Last.program "Last" p pp true in
(* Completion of partial definitions *)
let p = do_pass Completion.program "Completion" p pp true in
(* Reset *)
let p = do_pass Reset.program "Reset" p pp true in
(* Automata *)
let p = do_pass Automata.program "Automata" p pp true in
(* Every *)
let p = do_pass Every.program "Every" p pp true in
(* Present *)
let p = do_pass Present.program "Present" p pp true in
(* Return the transformed AST *)
p
(* Shared variables (last) *)
let p = do_pass Last.program "Last" p pp true in
(* Reset *)
let p = do_pass Reset.program "Reset" p pp true in
(* Every *)
let p = do_pass Every.program "Every" p pp true in
(* Return the transformed AST *)
p
let compile_interface l =

56
compiler/heptagon/main/heptcheck.ml
View file

@ -21,40 +21,40 @@ let parse_implementation lexbuf =
let parse_interface lexbuf =
parse Parser.interface Lexer.token lexbuf
let compile_impl modname filename =
let compile_impl modname filename =
(* input and output files *)
let source_name = filename ^ ".ept" in
let ic = open_in source_name in
let close_all_files () =
close_in ic
close_in ic
in
try
init_compiler modname source_name ic;
(* Parsing of the file *)
let lexbuf = Lexing.from_channel ic in
let p = parse_implementation lexbuf in
try
init_compiler modname source_name ic;
(* Convert the parse tree to Heptagon AST *)
let p = Scoping.translate_program p in
if !verbose
then begin
comment "Parsing";
pp p
end;
(* Parsing of the file *)
let lexbuf = Lexing.from_channel ic in
let p = parse_implementation lexbuf in
(* Call the compiler*)
let p = Hept_compiler.compile_impl pp p in
(* Convert the parse tree to Heptagon AST *)
let p = Scoping.translate_program p in
if !verbose
then begin
comment "Parsing";
pp p
end;
if !verbose
then begin
comment "Checking"
end;
close_all_files ()
(* Call the compiler*)
let p = Hept_compiler.compile_impl pp p in
with x -> close_all_files (); raise x
if !verbose
then begin
comment "Checking"
end;
close_all_files ()
with x -> close_all_files (); raise x
let compile_interface modname filename =
(* input and output files *)
@ -77,10 +77,10 @@ let compile_interface modname filename =
(* Convert the parse tree to Heptagon AST *)
let l = Scoping.translate_interface l in
(* Call the compiler*)
(* Call the compiler*)
let l = Hept_compiler.compile_interface l in
Modules.write itc;
Modules.write itc;
close_all_files ()
with
@ -91,12 +91,12 @@ let compile file =
then
let filename = Filename.chop_suffix file ".ept" in
let modname = String.capitalize(Filename.basename filename) in
compile_impl modname filename
compile_impl modname filename
else if Filename.check_suffix file ".epi"
then
let filename = Filename.chop_suffix file ".epi" in
let modname = String.capitalize(Filename.basename filename) in
compile_interface modname filename
compile_interface modname filename
else
raise (Arg.Bad ("Unknow file type: " ^ file))
@ -111,7 +111,7 @@ let main () =
"-where", Arg.Unit locate_stdlib, doc_locate_stdlib;
"-stdlib", Arg.String set_stdlib, doc_stdlib;
"-nopervasives", Arg.Unit set_no_pervasives, doc_no_pervasives;
"-noinit", Arg.Clear init, doc_noinit;
"-noinit", Arg.Clear init, doc_noinit;
"-fti", Arg.Set full_type_info, doc_full_type_info;
]
compile

8
compiler/heptagon/parsing/parsetree.ml
View file

@ -12,7 +12,7 @@ open Names
open Location
open Signature
type iterator_type =
type iterator_type =
| Imap
| Ifold
| Imapfold
@ -41,7 +41,7 @@ and app =
and op =
| Epre of const option
| Efby | Earrow | Eifthenelse
| Efby | Earrow | Eifthenelse
| Earray_op of array_op
| Efield_update of longname
| Ecall of op_desc
@ -177,7 +177,7 @@ let mk_app op =
{ a_op = op; }
let mk_op_desc ln params kind =
{ op_name = ln; op_params = params; op_kind = kind }
{ op_name = ln; op_params = params; op_kind = kind }
let mk_call desc exps =
Eapp (mk_app (Ecall desc), exps)
@ -205,7 +205,7 @@ let mk_var_dec name ty last =
v_last = last; v_loc = Location.current_loc () }
let mk_block locals eqs =
{ b_local = locals; b_equs = eqs;
{ b_local = locals; b_equs = eqs;
b_loc = Location.current_loc () }
let mk_const_dec id ty e =

202
compiler/heptagon/parsing/scoping.ml
View file

@ -22,23 +22,23 @@ struct
begin match kind with
| Evar name ->
eprintf "%aThe value identifier %s is unbound.\n"
output_location loc
name
output_location loc
name
| Econst_var name ->
eprintf "%aThe const identifier %s is unbound.\n"
output_location loc
name
output_location loc
name
| Evariable_already_defined name ->
eprintf "%aThe variable %s is already defined.\n"
output_location loc
name
output_location loc
name
| Econst_variable_already_defined name ->
eprintf "%aThe const variable %s is already defined.\n"
output_location loc
name
output_location loc
name
| Estatic_exp_expected ->
eprintf "%aA static expression was expected.\n"
output_location loc
output_location loc
end;
raise Misc.Error
end
@ -46,7 +46,7 @@ end
module Rename =
struct
include
(Map.Make (struct type t = string let compare = String.compare end))
(Map.Make (struct type t = string let compare = String.compare end))
let append env0 env =
fold (fun key v env -> add key v env) env0 env
@ -54,9 +54,9 @@ struct
try
find n env
with
Not_found -> Error.message loc (Error.Evar(n))
Not_found -> Error.message loc (Error.Evar(n))
end
(*Functions to build the renaming map*)
let add_var loc x env =
if Rename.mem x env then
@ -72,26 +72,26 @@ let add_const_var loc x env =
let rec build_pat loc env = function
| Evarpat x -> add_var loc x env
| Etuplepat l ->
| Etuplepat l ->
List.fold_left (build_pat loc) env l
let build_vd_list env l =
let build_vd env vd =
add_var vd.v_loc vd.v_name env
in
List.fold_left build_vd env l
List.fold_left build_vd env l
let build_cd_list env l =
let build_cd env cd =
add_const_var cd.c_loc cd.c_name env
in
List.fold_left build_cd env l
List.fold_left build_cd env l
let build_id_list loc env l =
let build_id env id =
add_const_var loc id env
in
List.fold_left build_id env l
in
List.fold_left build_id env l
(* Translate the AST into Heptagon. *)
let translate_iterator_type = function
@ -115,26 +115,28 @@ let op_from_app loc app =
let check_const_vars = ref true
let rec translate_size_exp const_env e =
match e.e_desc with
| Evar n ->
if !check_const_vars & not (NamesEnv.mem n const_env) then
Error.message e.e_loc (Error.Econst_var n)
else
SVar n
| Econst (Cint i) -> SConst i
| Eapp(app, [e1;e2]) ->
let op = op_from_app e.e_loc app in
SOp(op, translate_size_exp const_env e1, translate_size_exp const_env e2)
| _ -> Error.message e.e_loc Error.Estatic_exp_expected
match e.e_desc with
| Evar n ->
if !check_const_vars & not (NamesEnv.mem n const_env) then
Error.message e.e_loc (Error.Econst_var n)
else
SVar n
| Econst (Cint i) -> SConst i
| Eapp(app, [e1;e2]) ->
let op = op_from_app e.e_loc app in
SOp(op,
translate_size_exp const_env e1,
translate_size_exp const_env e2)
| _ -> Error.message e.e_loc Error.Estatic_exp_expected
let rec translate_type const_env = function
| Tprod ty_list -> Types.Tprod(List.map (translate_type const_env) ty_list)
| Tid ln -> Types.Tid ln
| Tarray (ty, e) ->
| Tarray (ty, e) ->
let ty = translate_type const_env ty in
Types.Tarray (ty, translate_size_exp const_env e)
Types.Tarray (ty, translate_size_exp const_env e)
and translate_exp const_env env e =
and translate_exp const_env env e =
{ Heptagon.e_desc = translate_desc e.e_loc const_env env e.e_desc;
Heptagon.e_ty = Types.invalid_type;
Heptagon.e_loc = e.e_loc }
@ -150,50 +152,56 @@ and translate_app const_env env app =
| Efield_update f -> Heptagon.Efield_update f
| Earray_op op -> Heptagon.Earray_op (translate_array_op const_env env op)
in
{ Heptagon.a_op = op; }
{ Heptagon.a_op = op; }
and translate_op_desc const_env desc =
{ Heptagon.op_name = desc.op_name;
Heptagon.op_params = List.map (translate_size_exp const_env) desc.op_params;
Heptagon.op_kind = translate_op_kind desc.op_kind }
and translate_array_op const_env env = function
| Eselect e_list -> Heptagon.Eselect (List.map (translate_size_exp const_env) e_list)
| Eupdate e_list -> Heptagon.Eupdate (List.map (translate_size_exp const_env) e_list)
and translate_array_op const_env env = function
| Eselect e_list ->
Heptagon.Eselect (List.map (translate_size_exp const_env) e_list)
| Eupdate e_list ->
Heptagon.Eupdate (List.map (translate_size_exp const_env) e_list)
| Erepeat -> Heptagon.Erepeat
| Eselect_slice -> Heptagon.Eselect_slice
| Econcat -> Heptagon.Econcat
| Eselect_dyn -> Heptagon.Eselect_dyn
| Eiterator (it, desc) ->
Heptagon.Eiterator (translate_iterator_type it,
| Eselect_dyn -> Heptagon.Eselect_dyn
| Eiterator (it, desc) ->
Heptagon.Eiterator (translate_iterator_type it,
translate_op_desc const_env desc, None)
and translate_desc loc const_env env = function
| Econst c -> Heptagon.Econst (translate_const c)
| Evar x ->
if Rename.mem x env then
Heptagon.Evar (Rename.name loc env x)
else if NamesEnv.mem x const_env then (* var not defined, maybe a const var*)
Heptagon.Econstvar x
| Evar x ->
if Rename.mem x env then
Heptagon.Evar (Rename.name loc env x)
else
Error.message loc (Error.Evar x)
if NamesEnv.mem x const_env then (* var not defined, maybe a const var*)
Heptagon.Econstvar x
else
Error.message loc (Error.Evar x)
| Elast x -> Heptagon.Elast (Rename.name loc env x)
| Etuple e_list -> Heptagon.Etuple (List.map (translate_exp const_env env) e_list)
| Etuple e_list ->
Heptagon.Etuple (List.map (translate_exp const_env env) e_list)
| Eapp ({ a_op = (Earray_op Erepeat)} as app, e_list) ->
let e_list = List.map (translate_exp const_env env) e_list in
(match e_list with
| [{ Heptagon.e_desc = Heptagon.Econst c }; e1 ] ->
Heptagon.Econst (Heptagon.Carray (Heptagon.size_exp_of_exp e1, c))
| _ -> Heptagon.Eapp (translate_app const_env env app, e_list)
)
(match e_list with
| [{ Heptagon.e_desc = Heptagon.Econst c }; e1 ] ->
Heptagon.Econst (Heptagon.Carray (Heptagon.size_exp_of_exp e1, c))
| _ -> Heptagon.Eapp (translate_app const_env env app, e_list)
)
| Eapp (app, e_list) ->
let e_list = List.map (translate_exp const_env env) e_list in
Heptagon.Eapp (translate_app const_env env app, e_list)
Heptagon.Eapp (translate_app const_env env app, e_list)
| Efield (e, field) -> Heptagon.Efield (translate_exp const_env env e, field)
| Estruct f_e_list ->
let f_e_list = List.map (fun (f,e) -> f, translate_exp const_env env e) f_e_list in
Heptagon.Estruct f_e_list
| Earray e_list -> Heptagon.Earray (List.map (translate_exp const_env env) e_list)
let f_e_list =
List.map (fun (f,e) -> f, translate_exp const_env env e) f_e_list in
Heptagon.Estruct f_e_list
| Earray e_list ->
Heptagon.Earray (List.map (translate_exp const_env env) e_list)
and translate_pat loc env = function
| Evarpat x -> Heptagon.Evarpat (Rename.name loc env x)
@ -201,40 +209,40 @@ and translate_pat loc env = function
let rec translate_eq const_env env eq =
{ Heptagon.eq_desc = translate_eq_desc eq.eq_loc const_env env eq.eq_desc ;
Heptagon.eq_statefull = false;
Heptagon.eq_statefull = false;
Heptagon.eq_loc = eq.eq_loc }
and translate_eq_desc loc const_env env = function
| Eswitch(e, switch_handlers) ->
let sh = List.map
(translate_switch_handler loc const_env env)
switch_handlers in
Heptagon.Eswitch (translate_exp const_env env e, sh)
| Eeq(p, e) ->
Heptagon.Eeq (translate_pat loc env p, translate_exp const_env env e)
| Epresent (present_handlers, b) ->
Heptagon.Epresent (List.map (translate_present_handler const_env env)
present_handlers,
fst (translate_block const_env env b))
| Eautomaton state_handlers ->
Heptagon.Eautomaton (List.map (translate_state_handler const_env env)
state_handlers)
| Ereset (eq_list, e) ->
Heptagon.Ereset (List.map (translate_eq const_env env) eq_list,
translate_exp const_env env e)
| Eswitch(e, switch_handlers) ->
let sh = List.map
(translate_switch_handler loc const_env env)
switch_handlers in
Heptagon.Eswitch (translate_exp const_env env e, sh)
| Eeq(p, e) ->
Heptagon.Eeq (translate_pat loc env p, translate_exp const_env env e)
| Epresent (present_handlers, b) ->
Heptagon.Epresent (List.map (translate_present_handler const_env env)
present_handlers,
fst (translate_block const_env env b))
| Eautomaton state_handlers ->
Heptagon.Eautomaton (List.map (translate_state_handler const_env env)
state_handlers)
| Ereset (eq_list, e) ->
Heptagon.Ereset (List.map (translate_eq const_env env) eq_list,
translate_exp const_env env e)
and translate_block const_env env b =
let env = build_vd_list env b.b_local in
{ Heptagon.b_local = translate_vd_list const_env env b.b_local;
Heptagon.b_equs = List.map (translate_eq const_env env) b.b_equs;
Heptagon.b_defnames = Env.empty ;
Heptagon.b_statefull = false;
Heptagon.b_defnames = Env.empty ;
Heptagon.b_statefull = false;
Heptagon.b_loc = b.b_loc }, env
and translate_state_handler const_env env sh =
let b, env = translate_block const_env env sh.s_block in
{ Heptagon.s_state = sh.s_state;
Heptagon.s_block = b;
Heptagon.s_block = b;
Heptagon.s_until = List.map (translate_escape const_env env) sh.s_until;
Heptagon.s_unless = List.map (translate_escape const_env env) sh.s_unless; }
@ -251,11 +259,11 @@ and translate_switch_handler loc const_env env sh =
{ Heptagon.w_name = sh.w_name;
Heptagon.w_block = fst (translate_block const_env env sh.w_block) }
and translate_var_dec const_env env vd =
and translate_var_dec const_env env vd =
{ Heptagon.v_name = Rename.name vd.v_loc env vd.v_name;
Heptagon.v_type = translate_type const_env vd.v_type;
Heptagon.v_last = translate_last env vd.v_last;
Heptagon.v_loc = vd.v_loc }
Heptagon.v_loc = vd.v_loc }
and translate_vd_list const_env env =
List.map (translate_var_dec const_env env)
@ -264,11 +272,12 @@ and translate_last env = function
| Var -> Heptagon.Var
| Last (None) -> Heptagon.Last None
| Last (Some c) -> Heptagon.Last (Some (translate_const c))
let translate_contract const_env env ct =
{ Heptagon.c_assume = translate_exp const_env env ct.c_assume;
Heptagon.c_enforce = translate_exp const_env env ct.c_enforce;
Heptagon.c_controllables = translate_vd_list const_env env ct.c_controllables;
Heptagon.c_enforce = translate_exp const_env env ct.c_enforce;
Heptagon.c_controllables =
translate_vd_list const_env env ct.c_controllables;
Heptagon.c_local = translate_vd_list const_env env ct.c_local;
Heptagon.c_eq = List.map (translate_eq const_env env) ct.c_eq }
@ -283,7 +292,7 @@ let translate_node const_env env node =
Heptagon.n_contract = Misc.optional
(translate_contract const_env env) node.n_contract;
Heptagon.n_equs = List.map (translate_eq const_env env) node.n_equs;
Heptagon.n_loc = node.n_loc;
Heptagon.n_loc = node.n_loc;
Heptagon.n_params = List.map Signature.mk_param node.n_params;
Heptagon.n_params_constraints = []; }
@ -292,14 +301,14 @@ let translate_typedec const_env ty =
| Type_abs -> Heptagon.Type_abs
| Type_enum(tag_list) -> Heptagon.Type_enum(tag_list)
| Type_struct(field_ty_list) ->
let translate_field_type (f,ty) =
Signature.mk_field f (translate_type const_env ty)
in
Heptagon.Type_struct (List.map translate_field_type field_ty_list)
let translate_field_type (f,ty) =
Signature.mk_field f (translate_type const_env ty)
in
Heptagon.Type_struct (List.map translate_field_type field_ty_list)
in
{ Heptagon.t_name = ty.t_name;
Heptagon.t_desc = onetype ty.t_desc;
Heptagon.t_loc = ty.t_loc }
{ Heptagon.t_name = ty.t_name;
Heptagon.t_desc = onetype ty.t_desc;
Heptagon.t_loc = ty.t_loc }
let translate_const_dec const_env cd =
{ Heptagon.c_name = cd.c_name;
@ -312,7 +321,8 @@ let translate_program p =
{ Heptagon.p_pragmas = p.p_pragmas;
Heptagon.p_opened = p.p_opened;
Heptagon.p_types = List.map (translate_typedec const_env) p.p_types;
Heptagon.p_nodes = List.map (translate_node const_env Rename.empty) p.p_nodes;
Heptagon.p_nodes =
List.map (translate_node const_env Rename.empty) p.p_nodes;
Heptagon.p_consts = List.map (translate_const_dec const_env) p.p_consts; }
let translate_arg const_env a =
@ -326,15 +336,15 @@ let translate_signature s =
Heptagon.sig_outputs = List.map (translate_arg const_env) s.sig_outputs;
Heptagon.sig_params = List.map Signature.mk_param s.sig_params; }
let translate_interface_desc const_env = function
let translate_interface_desc const_env = function
| Iopen n -> Heptagon.Iopen n
| Itypedef tydec -> Heptagon.Itypedef (translate_typedec const_env tydec)
| Isignature s -> Heptagon.Isignature (translate_signature s)
| Isignature s -> Heptagon.Isignature (translate_signature s)
let translate_interface_decl const_env idecl =
{ Heptagon.interf_desc = translate_interface_desc const_env idecl.interf_desc;
let translate_interface_decl const_env idecl =
{ Heptagon.interf_desc = translate_interface_desc const_env idecl.interf_desc;
Heptagon.interf_loc = idecl.interf_loc }
let translate_interface =
let translate_interface =
List.map (translate_interface_decl NamesEnv.empty)

66
compiler/heptagon/transformations/automata.ml
View file

@ -22,14 +22,14 @@ let mk_var_exp n ty =
let mk_pair e1 e2 =
mk_exp (Etuple [e1;e2]) (Tprod [e1.e_ty; e2.e_ty])
let mk_reset_equation eq_list e =
let mk_reset_equation eq_list e =
mk_equation (Ereset (eq_list, e))
let mk_switch_equation e l =
let mk_switch_equation e l =
mk_equation (Eswitch (e, l))
let mk_exp_fby_false e =
mk_exp (Eapp(mk_op (Epre (Some (Cconstr Initial.pfalse))), [e]))
let mk_exp_fby_false e =
mk_exp (Eapp(mk_op (Epre (Some (Cconstr Initial.pfalse))), [e]))
(Tid Initial.pbool)
let mk_exp_fby_state initial e =
@ -44,7 +44,7 @@ let intro_type states =
let state_type = "st" ^ n in
state_type_dec_list :=
(mk_type_dec state_type (Type_enum (list states))) :: !state_type_dec_list;
Name(state_type)
Name(state_type)
(* an automaton may be a Moore automaton, i.e., with only weak transitions; *)
(* a Mealy one, i.e., with only strong transition or mixed *)
@ -113,37 +113,37 @@ and translate_automaton v eq_list handlers =
let escapes n s rcont =
let escape { e_cond = e; e_reset = r; e_next_state = n } cont =
mk_ifthenelse e (mk_pair (state n) (if r then dtrue else dfalse)) cont
mk_ifthenelse e (mk_pair (state n) (if r then dtrue else dfalse)) cont
in
List.fold_right escape s (mk_pair (state n) rcont)
List.fold_right escape s (mk_pair (state n) rcont)
in
let strong { s_state = n; s_unless = su } =
let defnames = Env.add resetname (Tid Initial.pbool) Env.empty in
let defnames = Env.add statename tstatetype defnames in
let st_eq = mk_simple_equation
let st_eq = mk_simple_equation
(Etuplepat[Evarpat(statename); Evarpat(resetname)])
(escapes n su (boolvar pre_next_resetname)) in
mk_block defnames [mk_reset_equation [st_eq]
(boolvar pre_next_resetname)]
mk_block defnames [mk_reset_equation [st_eq]
(boolvar pre_next_resetname)]
in
let weak { s_state = n; s_block = b; s_until = su } =
let b = translate_block b in
let defnames = Env.add next_resetname (Tid Initial.pbool) b.b_defnames in
let defnames = Env.add next_statename tstatetype defnames in
let ns_eq = mk_simple_equation
let ns_eq = mk_simple_equation
(Etuplepat[Evarpat(next_statename); Evarpat(next_resetname)])
(escapes n su dfalse) in
{ b with b_equs =
[mk_reset_equation (ns_eq::b.b_equs) (boolvar resetname)];
{ b with b_equs =
[mk_reset_equation (ns_eq::b.b_equs) (boolvar resetname)];
(* (or_op (boolvar pre_next_resetname) (boolvar resetname))]; *)
b_defnames = defnames;
}
}
in
let v =
(mk_var_dec next_statename (Tid(statetype))) ::
(mk_var_dec next_statename (Tid(statetype))) ::
(mk_var_dec resetname (Tid Initial.pbool)) ::
(mk_var_dec next_resetname (Tid Initial.pbool)) ::
(mk_var_dec pre_next_resetname (Tid Initial.pbool)) :: v in
@ -153,38 +153,38 @@ and translate_automaton v eq_list handlers =
| true, false ->
let switch_e = mk_exp_fby_state initial (statevar next_statename) in
let switch_handlers = (List.map
(fun ({ s_state = n } as case) ->
{ w_name = name n; w_block = weak case })
handlers) in
(fun ({ s_state = n } as case) ->
{ w_name = name n; w_block = weak case })
handlers) in
let switch_eq = mk_switch_equation switch_e switch_handlers in
let nr_eq = mk_simple_equation (Evarpat pre_next_resetname)
(mk_exp_fby_false (boolvar (next_resetname))) in
let nr_eq = mk_simple_equation (Evarpat pre_next_resetname)
(mk_exp_fby_false (boolvar (next_resetname))) in
let pnr_eq = mk_simple_equation (Evarpat resetname)
(boolvar pre_next_resetname) in
(* a Moore automaton with only weak transitions *)
v, switch_eq :: nr_eq :: pnr_eq :: eq_list
(* a Moore automaton with only weak transitions *)
v, switch_eq :: nr_eq :: pnr_eq :: eq_list
| _ ->
(* the general case; two switch to generate,
statename variable used and defined *)
(* the general case; two switch to generate,
statename variable used and defined *)
let v = (mk_var_dec statename (Tid statetype)) :: v in
let ns_switch_e = mk_exp_fby_state initial (statevar next_statename) in
let ns_switch_handlers = List.map
(fun ({ s_state = n } as case) ->
{ w_name = name n; w_block = strong case })
handlers in
(fun ({ s_state = n } as case) ->
{ w_name = name n; w_block = strong case })
handlers in
let ns_switch_eq = mk_switch_equation ns_switch_e ns_switch_handlers in
let switch_e = statevar statename in
let switch_handlers = List.map
(fun ({ s_state = n } as case) ->
{ w_name = name n; w_block = weak case })
handlers in
(fun ({ s_state = n } as case) ->
{ w_name = name n; w_block = weak case })
handlers in
let switch_eq = mk_switch_equation switch_e switch_handlers in
let pnr_eq = mk_simple_equation (Evarpat pre_next_resetname)
(mk_exp_fby_false (boolvar (next_resetname))) in
v, ns_switch_eq :: switch_eq :: pnr_eq :: eq_list
let pnr_eq = mk_simple_equation (Evarpat pre_next_resetname)
(mk_exp_fby_false (boolvar (next_resetname))) in
v, ns_switch_eq :: switch_eq :: pnr_eq :: eq_list
let translate_contract ({ c_local = v; c_eq = eq_list} as c) =
let v, eq_list = translate_eqs v eq_list in

15
compiler/heptagon/transformations/every.ml
View file

@ -21,7 +21,7 @@ open Heptagon
open Reset
(*
let defnames m n d =
let defnames m n d =
let rec loop acc k = if k < n then loop (S.add m.(k) acc) (k+1) else acc in
loop d 0
*)
@ -77,20 +77,21 @@ and translate v acc_eq_list e =
let v, acc_eq_list,re = translate v acc_eq_list re in
let n, v, acc_eq_list = equation v acc_eq_list re in
let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
v,acc_eq_list,
v,acc_eq_list,
{ e with e_desc =
Eapp({ op with a_op = Ecall(op_desc,
Eapp({ op with a_op = Ecall(op_desc,
Some { re with e_desc = Evar(n) }) },
e_list) }
| Eapp ({ a_op = Earray_op(Eiterator(it, op_desc, Some re)) } as op, e_list)
when not (is_var re) ->
when not (is_var re) ->
let v, acc_eq_list,re = translate v acc_eq_list re in
let n, v, acc_eq_list = equation v acc_eq_list re in
let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
let re = { re with e_desc = Evar n } in
v,acc_eq_list,
let re = { re with e_desc = Evar n } in
v,acc_eq_list,
{ e with e_desc =
Eapp({ op with a_op = Earray_op(Eiterator(it, op_desc, Some re)) },
Eapp({ op with a_op =
Earray_op(Eiterator(it, op_desc, Some re)) },
e_list) }
| Eapp(f, e_list) ->
let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in

10
compiler/heptagon/transformations/last.ml
View file

@ -21,11 +21,11 @@ let last (eq_list, env, v) { v_name = n; v_type = t; v_last = last } =
let lastn = Ident.fresh ("last" ^ (sourcename n)) in
let eq = mk_equation (Eeq (Evarpat lastn,
mk_exp (Eapp (mk_op (Epre default),
[mk_exp (Evar n) t])) t)) in
eq:: eq_list,
[mk_exp (Evar n) t])) t)) in
eq:: eq_list,
Env.add n lastn env,
(mk_var_dec lastn t) :: v
let extend_env env v = List.fold_left last ([], env, []) v
let rec translate_eq env eq =
@ -64,7 +64,7 @@ and translate env e =
{ e with e_desc =
Estruct(List.map (fun (f, e) -> (f, translate env e)) e_f_list) }
| Earray(e_list) ->
{ e with e_desc = Earray(List.map (translate env) e_list) }
{ e with e_desc = Earray(List.map (translate env) e_list) }
let translate_contract env contract =
match contract with
@ -93,7 +93,7 @@ let node ({ n_input = i; n_local = v; n_output = o;
let contract, env = translate_contract env contract in
let eq_lastn_n_list, env, last_v = extend_env env v in
let eq_list = translate_eqs env eq_list in
{ n with
{ n with
n_input = i;
n_output = o;
n_local = v @ last_o @ last_v;

8
compiler/heptagon/transformations/present.ml
View file

@ -47,9 +47,11 @@ and translate_switch_handlers handlers =
and translate_present_handlers handlers cont =
let translate_present_handler { p_cond = e; p_block = b } cont =
let statefull = b.b_statefull or cont.b_statefull in
mk_block ~statefull:statefull b.b_defnames
[mk_switch_equation ~statefull:statefull e [{ w_name = ptrue; w_block = b };
{ w_name = pfalse; w_block = cont }]] in
mk_block ~statefull:statefull b.b_defnames
[mk_switch_equation
~statefull:statefull e
[{ w_name = ptrue; w_block = b };
{ w_name = pfalse; w_block = cont }]] in
let b = List.fold_right translate_present_handler handlers cont in
List.hd (b.b_equs)

66
compiler/heptagon/transformations/reset.ml
View file

@ -38,18 +38,19 @@ open Types
l_m1 = if res then true else true fby m1;...;
l_m3 = if res then true else true fby m3
e1 -> e2 is translated into if (true fby false) then e1 else e2
e1 -> e2 is translated into if (true fby false) then e1 else e2
*)
let mk_bool_var n =
let mk_bool_var n =
mk_exp (Evar n) (Tid Initial.pbool)
let mk_bool_param n =
let mk_bool_param n =
mk_var_dec n (Tid Initial.pbool)
let or_op_call = mk_op ( Ecall(mk_op_desc Initial.por [] Eop, None) )
let pre_true e =
{ e with e_desc = Eapp(mk_op (Epre (Some (Cconstr Initial.ptrue))), [e]) }
let pre_true e = {
e with e_desc = Eapp(mk_op (Epre (Some (Cconstr Initial.ptrue))), [e])
}
let init e = pre_true { dfalse with e_loc = e.e_loc }
(* the boolean condition for a structural reset *)
@ -84,7 +85,7 @@ let ifres res e2 e3 =
match res with
| Rfalse -> mk_ifthenelse (init e3) e2 e3
| _ -> (* a reset occurs *)
mk_ifthenelse (exp_of_res res) e2 e3
mk_ifthenelse (exp_of_res res) e2 e3
(* add an equation *)
let equation v acc_eq_list e =
@ -111,10 +112,12 @@ let add_local_equations i n m lm acc =
(* [mi = false;...; m1 = l_m1;...; mn = l_mn] *)
let rec loop acc k =
if k < n then
if k = i then loop ((mk_simple_equation (Evarpat (m.(k))) dfalse) :: acc) (k+1)
if k = i
then loop ((mk_simple_equation (Evarpat (m.(k))) dfalse) :: acc) (k+1)
else
loop
((mk_simple_equation (Evarpat (m.(k))) (mk_bool_var lm.(k))) :: acc) (k+1)
((mk_simple_equation (Evarpat (m.(k))) (mk_bool_var lm.(k))) :: acc)
(k+1)
else acc
in loop acc 0
@ -123,13 +126,13 @@ let add_global_equations n m lm res acc =
l_mn = if res then true else true fby mn ] *)
let rec loop acc k =
if k < n then
let exp =
let exp =
(match res with
| Rfalse -> pre_true (mk_bool_var m.(k))
| _ -> ifres res dtrue (pre_true (mk_bool_var m.(k)))
) in
loop
((mk_equation (Eeq (Evarpat (lm.(k)), exp))) :: acc) (k+1)
loop
((mk_equation (Eeq (Evarpat (lm.(k)), exp))) :: acc) (k+1)
else acc in
loop acc 0
@ -206,12 +209,12 @@ and translate res e =
match res, e1 with
| Rfalse, { e_desc = Econst(c) } ->
(* no reset *)
{ e with e_desc =
Eapp({ op with a_op = Epre(Some c) }, [e2]) }
{ e with e_desc =
Eapp({ op with a_op = Epre(Some c) }, [e2]) }
| _ ->
ifres res e1
{ e with e_desc =
Eapp({ op with a_op = Epre(default e1) }, [e2]) }
{ e with e_desc =
Eapp({ op with a_op = Epre(default e1) }, [e2]) }
end
| Eapp({ a_op = Earrow }, [e1;e2]) ->
let e1 = translate res e1 in
@ -223,32 +226,33 @@ and translate res e =
let re = translate res re in
let e_list = List.map (translate res) e_list in
let op = { op with a_op = Ecall(op_desc, Some (or_op res re))} in
{ e with e_desc = Eapp(op, e_list) }
(* create a new reset exp if necessary *)
{ e with e_desc = Eapp(op, e_list) }
(* create a new reset exp if necessary *)
| Eapp({ a_op = Ecall(op_desc, None) } as op, e_list) ->
let e_list = List.map (translate res) e_list in
if true_reset res & op_desc.op_kind <> Eop then
let op = { op with a_op = Ecall(op_desc, Some (exp_of_res res)) } in
{ e with e_desc = Eapp(op, e_list) }
{ e with e_desc = Eapp(op, e_list) }
else
{ e with e_desc = Eapp(op, e_list ) }
(* add reset to the current reset exp. *)
| Eapp( { a_op = Earray_op (Eiterator(it, op_desc, Some re)) } as op, e_list) ->
(* add reset to the current reset exp. *)
| Eapp( { a_op = Earray_op (Eiterator(it, op_desc, Some re)) } as op,
e_list) ->
let re = translate res re in
let e_list = List.map (translate res) e_list in
let r = Some (or_op res re) in
let r = Some (or_op res re) in
let op = { op with a_op = Earray_op (Eiterator(it, op_desc, r)) } in
{ e with e_desc = Eapp(op, e_list) }
(* create a new reset exp if necessary *)
| Eapp( { a_op = Earray_op (Eiterator(it, op_desc, None)) } as op, e_list) ->
{ e with e_desc = Eapp(op, e_list) }
(* create a new reset exp if necessary *)
| Eapp({ a_op = Earray_op (Eiterator(it, op_desc, None)) } as op, e_list) ->
let e_list = List.map (translate res) e_list in
if true_reset res then
let r = Some (exp_of_res res) in
let op = { op with a_op = Earray_op (Eiterator(it, op_desc, r)) } in
{ e with e_desc = Eapp(op, e_list) }
else
{ e with e_desc = Eapp(op, e_list) }
if true_reset res then
let r = Some (exp_of_res res) in
let op = { op with a_op = Earray_op (Eiterator(it, op_desc, r)) } in
{ e with e_desc = Eapp(op, e_list) }
else
{ e with e_desc = Eapp(op, e_list) }
| Eapp(op, e_list) ->
{ e with e_desc = Eapp(op, List.map (translate res) e_list) }
| Efield(e', field) ->

127
compiler/main/hept2mls.ml
View file

@ -56,7 +56,8 @@ struct
let add l env =
Ecomp(env,
List.fold_left
(fun acc { Heptagon.v_name = n } -> IdentSet.add n acc) IdentSet.empty l)
(fun acc { Heptagon.v_name = n } ->
IdentSet.add n acc) IdentSet.empty l)
(* sample e according to the clock [base on C1(x1) on ... on Cn(xn)] *)
let con env x e =
@ -150,7 +151,9 @@ let switch x ci_eqs_list =
then ()
else
begin
List.iter (fun (x,e) -> Printf.eprintf "|%s|, " (name x)) firsts;
List.iter
(fun (x,e) -> Printf.eprintf "|%s|, " (name x))
firsts;
assert false
end;
check_eqs nexts in
@ -189,7 +192,7 @@ let translate_op_kind = function
| Heptagon.Enode -> Enode
let translate_op_desc { Heptagon.op_name = n; Heptagon.op_params = p;
Heptagon.op_kind = k } =
Heptagon.op_kind = k } =
{ op_name = n; op_params = p;
op_kind = translate_op_kind k }
@ -200,8 +203,8 @@ let translate_reset = function
let translate_iterator_type = function
| Heptagon.Imap -> Imap
| Heptagon.Ifold -> Ifold
| Heptagon.Imapfold -> Imapfold
| Heptagon.Ifold -> Ifold
| Heptagon.Imapfold -> Imapfold
let rec application env { Heptagon.a_op = op; } e_list =
match op, e_list with
@ -209,7 +212,7 @@ let rec application env { Heptagon.a_op = op; } e_list =
| Heptagon.Epre(Some(c)), [e] -> Efby(Some(const c), e)
| Heptagon.Efby, [{ e_desc = Econst(c) } ; e] -> Efby(Some(c), e)
| Heptagon.Eifthenelse, [e1;e2;e3] -> Eifthenelse(e1, e2, e3)
| Heptagon.Ecall(op_desc, r), e_list ->
| Heptagon.Ecall(op_desc, r), e_list ->
Ecall(translate_op_desc op_desc, e_list, translate_reset r)
| Heptagon.Efield_update f, [e1;e2] -> Efield_update(f, e1, e2)
| Heptagon.Earray_op op, e_list ->
@ -217,53 +220,54 @@ let rec application env { Heptagon.a_op = op; } e_list =
and translate_array_op env op e_list =
match op, e_list with
| Heptagon.Erepeat, [e; idx] ->
Erepeat (size_exp_of_exp idx, e)
| Heptagon.Eselect idx_list, [e] ->
Eselect (idx_list, e)
(*Little hack: we need the to access the type of the array being accessed to
store the bounds (which will be used at code generation time, where the types
are harder to find). *)
| Heptagon.Erepeat, [e; idx] ->
Erepeat (size_exp_of_exp idx, e)
| Heptagon.Eselect idx_list, [e] ->
Eselect (idx_list, e)
(*Little hack: we need the to access the type of the array being
accessed to store the bounds (which will be used at code generation
time, where the types are harder to find). *)
| Heptagon.Eselect_dyn, e::defe::idx_list ->
let bounds = bounds_list e.e_ty in
Eselect_dyn (idx_list, bounds, e, defe)
let bounds = bounds_list e.e_ty in
Eselect_dyn (idx_list, bounds, e, defe)
| Heptagon.Eupdate idx_list, [e1;e2] ->
Eupdate (idx_list, e1, e2)
Eupdate (idx_list, e1, e2)
| Heptagon.Eselect_slice, [e; idx1; idx2] ->
Eselect_slice (size_exp_of_exp idx1, size_exp_of_exp idx2, e)
| Heptagon.Econcat, [e1; e2] ->
Econcat (e1, e2)
| Heptagon.Eiterator(it, op_desc, reset), idx::e_list ->
Eiterator(translate_iterator_type it,
translate_op_desc op_desc,
Eselect_slice (size_exp_of_exp idx1, size_exp_of_exp idx2, e)
| Heptagon.Econcat, [e1; e2] ->
Econcat (e1, e2)
| Heptagon.Eiterator(it, op_desc, reset), idx::e_list ->
Eiterator(translate_iterator_type it,
translate_op_desc op_desc,
size_exp_of_exp idx, e_list,
translate_reset reset)
translate_reset reset)
let rec translate env
{ Heptagon.e_desc = desc; Heptagon.e_ty = ty;
{ Heptagon.e_desc = desc; Heptagon.e_ty = ty;
Heptagon.e_loc = loc } =
match desc with
| Heptagon.Econst(c) ->
Env.const env (mk_exp ~loc:loc ~exp_ty:ty (Econst (const c)))
| Heptagon.Evar x ->
Env.con env x (mk_exp ~loc:loc ~exp_ty:ty (Evar x))
| Heptagon.Econstvar(x) ->
Env.const env (mk_exp ~loc:loc ~exp_ty:ty (Econstvar x))
| Heptagon.Etuple(e_list) ->
mk_exp ~loc:loc ~exp_ty:ty (Etuple (List.map (translate env) e_list))
| Heptagon.Eapp(app, e_list) ->
mk_exp ~loc:loc ~exp_ty:ty (application env app
(List.map (translate env) e_list))
| Heptagon.Efield(e, field) ->
mk_exp ~loc:loc ~exp_ty:ty (Efield (translate env e, field))
| Heptagon.Estruct f_e_list ->
let f_e_list = List.map
(fun (f, e) -> (f, translate env e)) f_e_list in
mk_exp ~loc:loc ~exp_ty:ty (Estruct f_e_list)
| Heptagon.Earray(e_list) ->
mk_exp ~loc:loc ~exp_ty:ty (Earray (List.map (translate env) e_list))
| Heptagon.Elast _ -> Error.message loc Error.Eunsupported_language_construct
match desc with
| Heptagon.Econst(c) ->
Env.const env (mk_exp ~loc:loc ~exp_ty:ty (Econst (const c)))
| Heptagon.Evar x ->
Env.con env x (mk_exp ~loc:loc ~exp_ty:ty (Evar x))
| Heptagon.Econstvar(x) ->
Env.const env (mk_exp ~loc:loc ~exp_ty:ty (Econstvar x))
| Heptagon.Etuple(e_list) ->
mk_exp ~loc:loc ~exp_ty:ty (Etuple (List.map (translate env) e_list))
| Heptagon.Eapp(app, e_list) ->
mk_exp ~loc:loc ~exp_ty:ty (application env app
(List.map (translate env) e_list))
| Heptagon.Efield(e, field) ->
mk_exp ~loc:loc ~exp_ty:ty (Efield (translate env e, field))
| Heptagon.Estruct f_e_list ->
let f_e_list = List.map
(fun (f, e) -> (f, translate env e)) f_e_list in
mk_exp ~loc:loc ~exp_ty:ty (Estruct f_e_list)
| Heptagon.Earray(e_list) ->
mk_exp ~loc:loc ~exp_ty:ty (Earray (List.map (translate env) e_list))
| Heptagon.Elast _ ->
Error.message loc Error.Eunsupported_language_construct
let rec translate_pat = function
| Heptagon.Evarpat(n) -> Evarpat n
| Heptagon.Etuplepat(l) -> Etuplepat (List.map translate_pat l)
@ -272,10 +276,10 @@ let rec rename_pat ni locals s_eqs = function
| Heptagon.Evarpat(n), ty ->
if IdentSet.mem n ni then (
let n_copy = Ident.fresh (sourcename n) in
Evarpat n_copy,
Evarpat n_copy,
(mk_var_dec n_copy ty) :: locals,
add n (mk_exp ~exp_ty:ty (Evar n_copy)) s_eqs
) else
) else
Evarpat n, locals, s_eqs
| Heptagon.Etuplepat(l), Tprod l_ty ->
let l, locals, s_eqs =
@ -290,7 +294,7 @@ let rec rename_pat ni locals s_eqs = function
let all_locals ni p =
IdentSet.is_empty (IdentSet.inter (Heptagon.vars_pat p) ni)
let rec translate_eq env ni (locals, l_eqs, s_eqs)
let rec translate_eq env ni (locals, l_eqs, s_eqs)
{ Heptagon.eq_desc = desc; Heptagon.eq_loc = loc } =
match desc with
| Heptagon.Eswitch(e, switch_handlers) ->
@ -306,9 +310,9 @@ let rec translate_eq env ni (locals, l_eqs, s_eqs)
s_eqs
| Heptagon.Eeq(p, e) (* some are local *) ->
(* transforms [p = e] into [p' = e; p = p'] *)
let p', locals, s_eqs =
rename_pat ni locals s_eqs (p, e.Heptagon.e_ty) in
locals,
let p', locals, s_eqs =
rename_pat ni locals s_eqs (p, e.Heptagon.e_ty) in
locals,
(mk_equation ~loc:loc p' (translate env e)) :: l_eqs,
s_eqs
| Heptagon.Epresent _ | Heptagon.Eautomaton _ | Heptagon.Ereset _ ->
@ -342,7 +346,10 @@ and translate_switch_handlers env ni (locals, l_eqs, s_eqs) e handlers =
[] -> IdentSet.empty
| { Heptagon.w_block = { Heptagon.b_defnames = env } } :: _ ->
(* Create set from env *)
(Ident.Env.fold (fun name _ set -> IdentSet.add name set) env IdentSet.empty) in
(Ident.Env.fold
(fun name _ set -> IdentSet.add name set)
env
IdentSet.empty) in
let ni_handlers = def handlers in
let x, locals, l_eqs = equation locals l_eqs (translate env e) in
@ -379,9 +386,9 @@ let translate_contract env contract =
let node
{ Heptagon.n_name = n; Heptagon.n_input = i; Heptagon.n_output = o;
Heptagon.n_contract = contract;
Heptagon.n_local = l; Heptagon.n_equs = eq_list;
Heptagon.n_local = l; Heptagon.n_equs = eq_list;
Heptagon.n_loc = loc;
Heptagon.n_params = params;
Heptagon.n_params = params;
Heptagon.n_params_constraints = params_constr } =
let env = Env.add o (Env.add i Env.empty) in
let contract, env = translate_contract env contract in
@ -413,13 +420,13 @@ let typedec
let const_dec cd =
{ c_name = cd.Heptagon.c_name;
c_value = cd.Heptagon.c_value;
c_value = cd.Heptagon.c_value;
c_loc = cd.Heptagon.c_loc; }
let program
let program
{ Heptagon.p_pragmas = pragmas;
Heptagon.p_opened = modules;
Heptagon.p_types = pt_list;
Heptagon.p_opened = modules;
Heptagon.p_types = pt_list;
Heptagon.p_nodes = n_list;
Heptagon.p_consts = c_list; } =
{ p_pragmas = pragmas;

62
compiler/main/heptc.ml
View file

@ -52,12 +52,12 @@ let interface modname filename =
(* Convert the parse tree to Heptagon AST *)
let l = Scoping.translate_interface l in
(* Call the compiler*)
(* Call the compiler*)
let l = Hept_compiler.compile_interface l in
Modules.write itc;
close_all_files ()
Modules.write itc;
close_all_files ()
with
| x -> close_all_files (); raise x
@ -99,34 +99,34 @@ let compile modname filename =
pp p
end;
(* Process the Heptagon AST *)
let p = Hept_compiler.compile_impl pp p in
Modules.write itc;
(* Process the Heptagon AST *)
let p = Hept_compiler.compile_impl pp p in
Modules.write itc;
(* Compile Heptagon to MiniLS *)
let p = Hept2mls.program p in
let pp = Mls_printer.print stdout in
if !verbose then comment "Translation into MiniLs";
Mls_printer.print mlsc p;
(* Process the MiniLS AST *)
let p = Mls_compiler.compile pp p in
(* Compile Heptagon to MiniLS *)
let p = Hept2mls.program p in
(* Compile MiniLS to Obc *)
let o = Mls2obc.program p in
(*if !verbose then*) comment "Translation into Obc";
Obc.Printer.print obc o;
let pp = Obc.Printer.print stdout in
if !verbose then pp o;
(* Translation into dataflow and sequential languages *)
Mls2seq.targets filename p o !target_languages;
close_all_files ()
with
let pp = Mls_printer.print stdout in
if !verbose then comment "Translation into MiniLs";
Mls_printer.print mlsc p;
(* Process the MiniLS AST *)
let p = Mls_compiler.compile pp p in
(* Compile MiniLS to Obc *)
let o = Mls2obc.program p in
(*if !verbose then*) comment "Translation into Obc";
Obc.Printer.print obc o;
let pp = Obc.Printer.print stdout in
if !verbose then pp o;
(* Translation into dataflow and sequential languages *)
Mls2seq.targets filename p o !target_languages;
close_all_files ()
with
| x -> close_all_files (); raise x
let compile file =
@ -157,7 +157,7 @@ let main () =
"-nopervasives", Arg.Unit set_no_pervasives, doc_no_pervasives;
"-target", Arg.String add_target_language, doc_target;
"-targetpath", Arg.String set_target_path, doc_target_path;
"-noinit", Arg.Clear init, doc_noinit;
"-noinit", Arg.Clear init, doc_noinit;
"-fti", Arg.Set full_type_info, doc_full_type_info;
]
compile

306
compiler/minils/analysis/clocking.ml
View file

@ -16,68 +16,68 @@ open Signature
open Types
open Location
open Printf
type error = | Etypeclash of ct * ct
exception TypingError of error
exception Unify
let error kind = raise (TypingError kind)
let message e kind =
match kind with | Etypeclash (actual_ct, expected_ct) ->
Printf.eprintf "%aClock Clash: this expression has clock %a, \n\
Printf.eprintf "%aClock Clash: this expression has clock %a, \n\
but is expected to have clock %a.\n"
Mls_printer.print_exp e
Mls_printer.print_clock actual_ct
Mls_printer.print_clock expected_ct;
raise Error
Mls_printer.print_exp e
Mls_printer.print_clock actual_ct
Mls_printer.print_clock expected_ct;
raise Error
let index = ref 0
let gen_index () = (incr index; !index)
let new_var () = Cvar { contents = Cindex (gen_index ()); }
let rec repr ck =
match ck with
| Cbase | Con _ | Cvar { contents = Cindex _ } -> ck
| Cvar (({ contents = Clink ck } as link)) ->
let ck = repr ck in (link.contents <- Clink ck; ck)
| Cbase | Con _ | Cvar { contents = Cindex _ } -> ck
| Cvar (({ contents = Clink ck } as link)) ->
let ck = repr ck in (link.contents <- Clink ck; ck)
let rec occur_check index ck =
let ck = repr ck
in
match ck with
match ck with
| Cbase -> ()
| Cvar { contents = Cindex n } when index <> n -> ()
| Con (ck, _, _) -> occur_check index ck
| _ -> raise Unify
let rec ck_value ck =
match ck with
| Cbase | Con _ | Cvar { contents = Cindex _ } -> ck
| Cvar { contents = Clink ck } -> ck_value ck
| Cbase | Con _ | Cvar { contents = Cindex _ } -> ck
| Cvar { contents = Clink ck } -> ck_value ck
let rec unify t1 t2 =
if t1 == t2
then ()
else
(match (t1, t2) with
| (Ck ck1, Ck ck2) -> unify_ck ck1 ck2
| (Cprod ct_list1, Cprod ct_list2) ->
(try List.iter2 unify ct_list1 ct_list2 with | _ -> raise Unify)
| _ -> raise Unify)
| (Ck ck1, Ck ck2) -> unify_ck ck1 ck2
| (Cprod ct_list1, Cprod ct_list2) ->
(try List.iter2 unify ct_list1 ct_list2 with | _ -> raise Unify)
| _ -> raise Unify)
and unify_ck ck1 ck2 =
let ck1 = repr ck1 in
let ck2 = repr ck2
in
if ck1 == ck2
then ()
else
(match (ck1, ck2) with
if ck1 == ck2
then ()
else
(match (ck1, ck2) with
| (Cbase, Cbase) -> ()
| (Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 }) when
n1 = n2 -> ()
@ -88,167 +88,167 @@ and unify_ck ck1 ck2 =
| (Con (ck1, c1, n1), Con (ck2, c2, n2)) when (c1 = c2) & (n1 = n2) ->
unify_ck ck1 ck2
| _ -> raise Unify)
let rec eq ck1 ck2 =
match ((repr ck1), (repr ck2)) with
| (Cbase, Cbase) -> true
| (Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 }) -> true
| (Con (ck1, _, n1), Con (ck2, _, n2)) when n1 = n2 -> eq ck1 ck2
| _ -> false
| (Cbase, Cbase) -> true
| (Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 }) -> true
| (Con (ck1, _, n1), Con (ck2, _, n2)) when n1 = n2 -> eq ck1 ck2
| _ -> false
let rec unify t1 t2 =
match (t1, t2) with
| (Ck ck1, Ck ck2) -> unify_ck ck1 ck2
| (Cprod t1_list, Cprod t2_list) -> unify_list t1_list t2_list
| _ -> raise Unify
| (Ck ck1, Ck ck2) -> unify_ck ck1 ck2
| (Cprod t1_list, Cprod t2_list) -> unify_list t1_list t2_list
| _ -> raise Unify
and unify_list t1_list t2_list =
try List.iter2 unify t1_list t2_list with | _ -> raise Unify
let rec skeleton ck = function
| Tprod ty_list -> Cprod (List.map (skeleton ck) ty_list)
| Tarray _ | Tid _ -> Ck ck
let ckofct = function | Ck ck -> repr ck | Cprod ct_list -> Cbase
let prod =
function | [] -> assert false | [ ty ] -> ty | ty_list -> Tprod ty_list
let typ_of_name h x = Env.find x h
let rec typing h e =
let ct =
match e.e_desc with
| Econst _ | Econstvar _ -> Ck (new_var ())
| Evar x -> Ck (typ_of_name h x)
| Efby (c, e) -> typing h e
| Etuple e_list -> Cprod (List.map (typing h) e_list)
| Ecall(_, e_list, r) ->
let ck_r = match r with
| None -> new_var()
| Some(reset) -> typ_of_name h reset
in (List.iter (expect h (Ck ck_r)) e_list; skeleton ck_r e.e_ty)
| Ecall(_, e_list, Some(reset)) ->
let ck_r = typ_of_name h reset
in (List.iter (expect h (Ck ck_r)) e_list; skeleton ck_r e.e_ty)
| Ewhen (e, c, n) ->
let ck_n = typ_of_name h n
in (expect h (skeleton ck_n e.e_ty) e;
skeleton (Con (ck_n, c, n)) e.e_ty)
| Eifthenelse (e1, e2, e3) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty
in (expect h (Ck ck) e1; expect h ct e2; expect h ct e3; ct)
| Emerge (n, c_e_list) ->
let ck_c = typ_of_name h n
in (typing_c_e_list h ck_c n c_e_list; skeleton ck_c e.e_ty)
| Efield (e1, n) ->
let ck = new_var () in
let ct = skeleton ck e1.e_ty in (expect h (Ck ck) e1; ct)
| Efield_update (_, e1, e2) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty
in (expect h (Ck ck) e1; expect h ct e2; ct)
| Estruct l ->
let ck = new_var () in
(List.iter
(fun (n, e) -> let ct = skeleton ck e.e_ty in expect h ct e) l;
Ck ck)
| Earray e_list ->
let ck = new_var ()
in (List.iter (expect h (Ck ck)) e_list; skeleton ck e.e_ty)
| Earray_op(op) -> typing_array_op h e op
| Econst _ | Econstvar _ -> Ck (new_var ())
| Evar x -> Ck (typ_of_name h x)
| Efby (c, e) -> typing h e
| Etuple e_list -> Cprod (List.map (typing h) e_list)
| Ecall(_, e_list, r) ->
let ck_r = match r with
| None -> new_var()
| Some(reset) -> typ_of_name h reset
in (List.iter (expect h (Ck ck_r)) e_list; skeleton ck_r e.e_ty)
| Ecall(_, e_list, Some(reset)) ->
let ck_r = typ_of_name h reset
in (List.iter (expect h (Ck ck_r)) e_list; skeleton ck_r e.e_ty)
| Ewhen (e, c, n) ->
let ck_n = typ_of_name h n
in (expect h (skeleton ck_n e.e_ty) e;
skeleton (Con (ck_n, c, n)) e.e_ty)
| Eifthenelse (e1, e2, e3) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty
in (expect h (Ck ck) e1; expect h ct e2; expect h ct e3; ct)
| Emerge (n, c_e_list) ->
let ck_c = typ_of_name h n
in (typing_c_e_list h ck_c n c_e_list; skeleton ck_c e.e_ty)
| Efield (e1, n) ->
let ck = new_var () in
let ct = skeleton ck e1.e_ty in (expect h (Ck ck) e1; ct)
| Efield_update (_, e1, e2) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty
in (expect h (Ck ck) e1; expect h ct e2; ct)
| Estruct l ->
let ck = new_var () in
(List.iter
(fun (n, e) -> let ct = skeleton ck e.e_ty in expect h ct e) l;
Ck ck)
| Earray e_list ->
let ck = new_var ()
in (List.iter (expect h (Ck ck)) e_list; skeleton ck e.e_ty)
| Earray_op(op) -> typing_array_op h e op
in (e.e_ck <- ckofct ct; ct)
and typing_array_op h e = function
| Erepeat (_, e) -> typing h e
| Eselect (_, e) -> typing h e
| Eselect_dyn (e_list, _, e, defe) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty
in (expect h ct e; List.iter (expect h ct) e_list; ct)
| Eupdate (_, e1, e2) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty
in (expect h (Ck ck) e1; expect h ct e2; ct)
| Eselect_slice (_, _, e) -> typing h e
| Econcat (e1, e2) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty
in (expect h (Ck ck) e1; expect h ct e2; ct)
| Eiterator (_, _, _, e_list, r) ->
let ck_r = match r with
| None -> new_var()
| Some(reset) -> typ_of_name h reset
in (List.iter (expect h (Ck ck_r)) e_list; skeleton ck_r e.e_ty)
| Erepeat (_, e) -> typing h e
| Eselect (_, e) -> typing h e
| Eselect_dyn (e_list, _, e, defe) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty
in (expect h ct e; List.iter (expect h ct) e_list; ct)
| Eupdate (_, e1, e2) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty
in (expect h (Ck ck) e1; expect h ct e2; ct)
| Eselect_slice (_, _, e) -> typing h e
| Econcat (e1, e2) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty
in (expect h (Ck ck) e1; expect h ct e2; ct)
| Eiterator (_, _, _, e_list, r) ->
let ck_r = match r with
| None -> new_var()
| Some(reset) -> typ_of_name h reset
in (List.iter (expect h (Ck ck_r)) e_list; skeleton ck_r e.e_ty)
and expect h expected_ty e =
let actual_ty = typing h e
in
try unify actual_ty expected_ty
with | Unify -> message e (Etypeclash (actual_ty, expected_ty))
try unify actual_ty expected_ty
with | Unify -> message e (Etypeclash (actual_ty, expected_ty))
and typing_c_e_list h ck_c n c_e_list =
let rec typrec =
function
| [] -> ()
| (c, e) :: c_e_list ->
(expect h (skeleton (Con (ck_c, c, n)) e.e_ty) e; typrec c_e_list)
| [] -> ()
| (c, e) :: c_e_list ->
(expect h (skeleton (Con (ck_c, c, n)) e.e_ty) e; typrec c_e_list)
in typrec c_e_list
let rec typing_pat h =
function
| Evarpat x -> Ck (typ_of_name h x)
| Etuplepat pat_list -> Cprod (List.map (typing_pat h) pat_list)
| Evarpat x -> Ck (typ_of_name h x)
| Etuplepat pat_list -> Cprod (List.map (typing_pat h) pat_list)
let typing_eqs h eq_list =
List.iter
(fun { eq_lhs = pat; eq_rhs = e } ->
match e.e_desc with (*TODO FIXME*)
| _ ->
let ty_pat = typing_pat h pat
in
| _ ->
let ty_pat = typing_pat h pat
in
(try expect h ty_pat e
with
| Error ->
(* TODO remettre en route quand Printer fonctionne
| Error ->
(* TODO remettre en route quand Printer fonctionne
(* DEBUG *)
Printf.eprintf "Complete expression: %a\n"
Printer.print_exp e;
Printf.eprintf "Clock pattern: %a\n"
Printer.print_clock ty_pat; *)
raise Error))
(* DEBUG *)
Printf.eprintf "Complete expression: %a\n"
Printer.print_exp e;
Printf.eprintf "Clock pattern: %a\n"
Printer.print_clock ty_pat; *)
raise Error))
eq_list
let build h dec =
List.fold_left (fun h { v_name = n } -> Env.add n (new_var ()) h) h dec
let sbuild h dec base =
List.fold_left (fun h { v_name = n } -> Env.add n base h) h dec
let typing_contract h contract base =
match contract with
| None -> h
| Some
{
c_local = l_list;
c_eq = eq_list;
c_assume = e_a;
c_enforce = e_g;
c_controllables = c_list
} ->
let h = sbuild h c_list base in
let h' = build h l_list
in
| None -> h
| Some
{
c_local = l_list;
c_eq = eq_list;
c_assume = e_a;
c_enforce = e_g;
c_controllables = c_list
} ->
let h = sbuild h c_list base in
let h' = build h l_list
in
(* assumption *)
(* property *)
(typing_eqs h' eq_list;
expect h' (Ck base) e_a;
expect h' (Ck base) e_g;
h)
let typing_node (({
n_name = f;
n_input = i_list;
@ -257,26 +257,26 @@ let typing_node (({
n_local = l_list;
n_equs = eq_list
} as node))
=
=
let base = Cbase in
let h = sbuild Env.empty i_list base in
let h = sbuild h o_list base in
let h = typing_contract h contract base in
let h = build h l_list
in
(typing_eqs h eq_list;
(*update clock info in variables descriptions *)
let set_clock vd =
{ (vd) with v_clock = ck_value (Env.find vd.v_name h); }
in
{
(node)
with
n_input = List.map set_clock i_list;
n_output = List.map set_clock o_list;
n_local = List.map set_clock l_list;
})
(typing_eqs h eq_list;
(*update clock info in variables descriptions *)
let set_clock vd =
{ (vd) with v_clock = ck_value (Env.find vd.v_name h); }
in
{
(node)
with
n_input = List.map set_clock i_list;
n_output = List.map set_clock o_list;
n_local = List.map set_clock l_list;
})
let program (({ p_nodes = p_node_list } as p)) =
{ (p) with p_nodes = List.map typing_node p_node_list; }

305
compiler/minils/analysis/init.ml
View file

@ -21,7 +21,7 @@ open Minils
open Location
open Format
open Types
type typ = | Iproduct of typ list | Ileaf of init
and init = { mutable i_desc : init_desc; mutable i_index : int}
@ -29,79 +29,79 @@ and init = { mutable i_desc : init_desc; mutable i_index : int}
and init_desc = | Izero | Ione | Ivar | Imax of init * init | Ilink of init
type typ_env =
{ t_init : init; (* its initialisation type *) t_value : longname option }
{ t_init : init; (* its initialisation type *) t_value : longname option }
(* its initial value *)
(* typing errors *)
exception Unify
let index = ref 0
let gen_index () = (incr index; !index)
let new_var () = { i_desc = Ivar; i_index = gen_index (); }
let izero = { i_desc = Izero; i_index = gen_index (); }
let ione = { i_desc = Ione; i_index = gen_index (); }
let imax i1 i2 = { i_desc = Imax (i1, i2); i_index = gen_index (); }
let product l = Iproduct l
let leaf i = Ileaf i
(* basic operation on initialization values *)
let rec irepr i =
match i.i_desc with
| Ilink i_son ->
let i_son = irepr i_son in (i.i_desc <- Ilink i_son; i_son)
| _ -> i
| Ilink i_son ->
let i_son = irepr i_son in (i.i_desc <- Ilink i_son; i_son)
| _ -> i
(** Simplification rules for max. Nothing fancy here *)
let max i1 i2 =
let i1 = irepr i1 in
let i2 = irepr i2
in
match ((i1.i_desc), (i2.i_desc)) with
match ((i1.i_desc), (i2.i_desc)) with
| (Izero, Izero) -> izero
| (Izero, _) -> i2
| (_, Izero) -> i1
| (_, Ione) | (Ione, _) -> ione
| _ -> imax i1 i2
let rec itype =
function | Iproduct ty_list -> itype_list ty_list | Ileaf i -> i
and itype_list ty_list =
List.fold_left (fun acc ty -> max acc (itype ty)) izero ty_list
(* saturate an initialization type. Every element must be initialized *)
let rec initialized i =
let i = irepr i
in
match i.i_desc with
match i.i_desc with
| Izero -> ()
| Ivar -> i.i_desc <- Ilink izero
| Imax (i1, i2) -> (initialized i1; initialized i2)
| Ilink i -> initialized i
| Ione -> raise Unify
(* build an initialization type from a type *)
let rec skeleton i =
function
| Tprod ty_list -> product (List.map (skeleton i) ty_list)
| Tarray _ | Tid _ -> leaf i
| Tprod ty_list -> product (List.map (skeleton i) ty_list)
| Tarray _ | Tid _ -> leaf i
(* sub-typing *)
let rec less left_ty right_ty =
if left_ty == right_ty
then ()
else
(match (left_ty, right_ty) with
| (Iproduct l1, Iproduct l2) -> List.iter2 less l1 l2
| (Ileaf i1, Ileaf i2) -> iless i1 i2
| _ -> raise Unify)
| (Iproduct l1, Iproduct l2) -> List.iter2 less l1 l2
| (Ileaf i1, Ileaf i2) -> iless i1 i2
| _ -> raise Unify)
and iless left_i right_i =
if left_i == right_i
@ -110,10 +110,10 @@ and iless left_i right_i =
(let left_i = irepr left_i in
let right_i = irepr right_i
in
if left_i == right_i
then ()
else
(match ((left_i.i_desc), (right_i.i_desc)) with
if left_i == right_i
then ()
else
(match ((left_i.i_desc), (right_i.i_desc)) with
| (Izero, _) | (_, Ione) -> ()
| (_, Izero) -> initialized left_i
| (Imax (i1, i2), _) -> (iless i1 right_i; iless i2 right_i)
@ -128,67 +128,67 @@ and iless left_i right_i =
and (* an inequation [a < t[a]] becomes [a = t[0]] *) occur_check index i =
match i.i_desc with
| Izero | Ione -> i
| Ivar -> if i.i_index = index then izero else i
| Imax (i1, i2) -> max (occur_check index i1) (occur_check index i2)
| Ilink i -> occur_check index i
| Izero | Ione -> i
| Ivar -> if i.i_index = index then izero else i
| Imax (i1, i2) -> max (occur_check index i1) (occur_check index i2)
| Ilink i -> occur_check index i
(* computes the initialization type of a merge *)
let merge opt_c c_i_list =
let rec search c c_i_list =
match c_i_list with
| [] -> izero
| (c0, i) :: c_i_list -> if c = c0 then i else search c c_i_list
| [] -> izero
| (c0, i) :: c_i_list -> if c = c0 then i else search c c_i_list
in
match opt_c with
match opt_c with
| None -> List.fold_left (fun acc (_, i) -> max acc i) izero c_i_list
| Some c -> search c c_i_list
module Printer =
struct
open Format
let rec print_list_r print po sep pf ff =
function
struct
open Format
let rec print_list_r print po sep pf ff =
function
| [] -> ()
| x :: l ->
(fprintf ff "@[%s%a" po print x;
List.iter (fprintf ff "%s@]@ @[%a" sep print) l;
fprintf ff "%s@]" pf)
let rec fprint_init ff i =
match i.i_desc with
let rec fprint_init ff i =
match i.i_desc with
| Izero -> fprintf ff "0"
| Ione -> fprintf ff "1"
| Ivar -> fprintf ff "0"
| Imax (i1, i2) ->
fprintf ff "@[%a\\/%a@]" fprint_init i1 fprint_init i2
| Ilink i -> fprint_init ff i
let rec fprint_typ ff =
function
let rec fprint_typ ff =
function
| Ileaf i -> fprint_init ff i
| Iproduct ty_list ->
fprintf ff "@[%a@]" (print_list_r fprint_typ "(" " *" ")") ty_list
let output_typ oc ty =
let ff = formatter_of_out_channel oc
in (fprintf ff "@["; fprint_typ ff ty; fprintf ff "@?@]")
end
let output_typ oc ty =
let ff = formatter_of_out_channel oc
in (fprintf ff "@["; fprint_typ ff ty; fprintf ff "@?@]")
end
module Error =
struct
open Location
type error = | Eclash of typ * typ
exception Error of location * error
let error loc kind = raise (Error (loc, kind))
let message loc kind =
((match kind with
struct
open Location
type error = | Eclash of typ * typ
exception Error of location * error
let error loc kind = raise (Error (loc, kind))
let message loc kind =
((match kind with
| Eclash (left_ty, right_ty) ->
Printf.eprintf
"%aInitialization error: this expression has type \
@ -196,128 +196,129 @@ module Error =
but is expected to have type %a\n"
output_location loc Printer.output_typ left_ty Printer.
output_typ right_ty);
raise Misc.Error)
end
raise Misc.Error)
end
let less_exp e actual_ty expected_ty =
try less actual_ty expected_ty
with
| Unify -> Error.message e.e_loc (Error.Eclash (actual_ty, expected_ty))
| Unify -> Error.message e.e_loc (Error.Eclash (actual_ty, expected_ty))
let rec typing h e =
match e.e_desc with
| Econst c -> leaf izero
| Evar x -> let { t_init = i } = Env.find x h in leaf i
| Efby (None, e) -> (expect h e (skeleton izero e.e_ty); leaf ione)
| Efby ((Some _), e) -> (expect h e (skeleton izero e.e_ty); leaf izero)
| Etuple e_list -> product (List.map (typing h) e_list)
| Econst c -> leaf izero
| Evar x -> let { t_init = i } = Env.find x h in leaf i
| Efby (None, e) -> (expect h e (skeleton izero e.e_ty); leaf ione)
| Efby ((Some _), e) -> (expect h e (skeleton izero e.e_ty); leaf izero)
| Etuple e_list -> product (List.map (typing h) e_list)
(*TODO traitement singulier et empêche reset d'un 'op'*)
| Ecall (op, e_list, None) when op.op_kind = Eop ->
let i = List.fold_left (fun acc e -> itype (typing h e)) izero e_list
in skeleton i e.e_ty
| Ecall (op, e_list, reset) when op.op_kind = Enode ->
List.iter (fun e -> expect h e (skeleton izero e.e_ty)) e_list;
let i = match reset with
| None -> izero
| Some(n) -> let { t_init = i } = Env.find n h in i
in skeleton i e.e_ty
| Ewhen (e, c, n) ->
let { t_init = i1 } = Env.find n h in
let i2 = itype (typing h e) in skeleton (max i1 i2) e.e_ty
(* result of the encoding of e1 -> e2 == if true fby false then e1 else e2 *)
| Eifthenelse(
{ e_desc = Efby(Some (Cconstr tn), { e_desc = Econst (Cconstr fn) }) },
e2, e3) when tn = Initial.ptrue & fn = Initial.pfalse ->
expect h e3 (skeleton ione e3.e_ty);
let i = itype (typing h e2) in skeleton i e.e_ty
| Eifthenelse (e1, e2, e3) ->
let i1 = itype (typing h e1) in
let i2 = itype (typing h e2) in
let i3 = itype (typing h e3) in
let i = max i1 (max i2 i3) in skeleton i e.e_ty
| Emerge (n, c_e_list) ->
let { t_init = i; t_value = opt_c } = Env.find n h in
let i =
merge opt_c
(List.map (fun (c, e) -> (c, (itype (typing h e)))) c_e_list)
in skeleton i e.e_ty
| Efield (e1, n) -> let i = itype (typing h e1) in skeleton i e.e_ty
| Estruct l ->
let i =
List.fold_left (fun acc (_, e) -> max acc (itype (typing h e))) izero
l
in skeleton i e.e_ty
| Efield_update _ | Econstvar _ | Earray _ | Earray_op _ ->
leaf izero (* TODO FIXME array_op dans init *)
(*TODO traitement singulier et empêche reset d'un 'op'*)
| Ecall (op, e_list, None) when op.op_kind = Eop ->
let i = List.fold_left (fun acc e -> itype (typing h e)) izero e_list
in skeleton i e.e_ty
| Ecall (op, e_list, reset) when op.op_kind = Enode ->
List.iter (fun e -> expect h e (skeleton izero e.e_ty)) e_list;
let i = match reset with
| None -> izero
| Some(n) -> let { t_init = i } = Env.find n h in i
in skeleton i e.e_ty
| Ewhen (e, c, n) ->
let { t_init = i1 } = Env.find n h in
let i2 = itype (typing h e) in skeleton (max i1 i2) e.e_ty
(* result of the encoding of e1 -> e2 ==
if true fby false then e1 else e2 *)
| Eifthenelse(
{ e_desc = Efby(Some (Cconstr tn), { e_desc = Econst (Cconstr fn) }) },
e2, e3) when tn = Initial.ptrue & fn = Initial.pfalse ->
expect h e3 (skeleton ione e3.e_ty);
let i = itype (typing h e2) in skeleton i e.e_ty
| Eifthenelse (e1, e2, e3) ->
let i1 = itype (typing h e1) in
let i2 = itype (typing h e2) in
let i3 = itype (typing h e3) in
let i = max i1 (max i2 i3) in skeleton i e.e_ty
| Emerge (n, c_e_list) ->
let { t_init = i; t_value = opt_c } = Env.find n h in
let i =
merge opt_c
(List.map (fun (c, e) -> (c, (itype (typing h e)))) c_e_list)
in skeleton i e.e_ty
| Efield (e1, n) -> let i = itype (typing h e1) in skeleton i e.e_ty
| Estruct l ->
let i =
List.fold_left (fun acc (_, e) -> max acc (itype (typing h e))) izero
l
in skeleton i e.e_ty
| Efield_update _ | Econstvar _ | Earray _ | Earray_op _ ->
leaf izero (* TODO FIXME array_op dans init *)
and expect h e expected_ty =
let actual_ty = typing h e in less_exp e actual_ty expected_ty
let rec typing_pat h =
function
| Evarpat x -> let { t_init = i } = Env.find x h in leaf i
| Etuplepat pat_list -> product (List.map (typing_pat h) pat_list)
| Evarpat x -> let { t_init = i } = Env.find x h in leaf i
| Etuplepat pat_list -> product (List.map (typing_pat h) pat_list)
let typing_eqs h eq_list =
List.iter
(fun { eq_lhs = pat; eq_rhs = e } ->
let ty_pat = typing_pat h pat in expect h e ty_pat)
eq_list
let build h eq_list =
let rec build_pat h =
function
| Evarpat x -> Env.add x { t_init = new_var (); t_value = None; } h
| Etuplepat pat_list -> List.fold_left build_pat h pat_list in
| Evarpat x -> Env.add x { t_init = new_var (); t_value = None; } h
| Etuplepat pat_list -> List.fold_left build_pat h pat_list in
let build_equation h { eq_lhs = pat; eq_rhs = e } =
match (pat, (e.e_desc)) with
| (Evarpat x, Efby ((Some (Cconstr c)), _)) ->
(* we keep the initial value of state variables *)
Env.add x { t_init = new_var (); t_value = Some c; } h
| _ -> build_pat h pat
| (Evarpat x, Efby ((Some (Cconstr c)), _)) ->
(* we keep the initial value of state variables *)
Env.add x { t_init = new_var (); t_value = Some c; } h
| _ -> build_pat h pat
in List.fold_left build_equation h eq_list
let sbuild h dec =
List.fold_left
(fun h { v_name = n } -> Env.add n { t_init = izero; t_value = None; } h)
h dec
let typing_contract h contract =
match contract with
| None -> h
| Some
{
c_local = l_list;
c_eq = eq_list;
c_assume = e_a;
c_enforce = e_g;
c_controllables = c_list
} ->
let h = sbuild h c_list in
let h' = build h eq_list
in
| None -> h
| Some
{
c_local = l_list;
c_eq = eq_list;
c_assume = e_a;
c_enforce = e_g;
c_controllables = c_list
} ->
let h = sbuild h c_list in
let h' = build h eq_list
in
(* assumption *)
(* property *)
(typing_eqs h' eq_list;
expect h' e_a (skeleton izero e_a.e_ty);
expect h' e_g (skeleton izero e_g.e_ty);
h)
let typing_node {
n_name = f;
n_input = i_list;
n_output = o_list;
n_contract = contract;
n_local = l_list;
n_equs = eq_list
} =
n_name = f;
n_input = i_list;
n_output = o_list;
n_contract = contract;
n_local = l_list;
n_equs = eq_list
} =
let h = sbuild Env.empty i_list in
let h = sbuild h o_list in
let h = typing_contract h contract in
let h = build h eq_list in typing_eqs h eq_list
let program (({ p_nodes = p_node_list } as p)) =
(List.iter typing_node p_node_list; p)

2
compiler/minils/main/mls2seq.ml
View file

@ -19,7 +19,7 @@ let dataflow_target filename p target_languages =
if !verbose then
comment "Translation into dynamic system (Z/3Z equations)";
Sigali.Printer.print dir p;
one_target others
one_target others
| ("vhdl_df" | "vhdl") :: others ->
let dirname = build_path (filename ^ "_vhdl") in
let dir = clean_dir dirname in

8
compiler/minils/main/mls_compiler.ml
View file

@ -19,12 +19,12 @@ let compile pp p =
(* Normalization to maximize opportunities *)
let p = do_pass Normalize.program "Normalization" p pp true in
(* Scheduling *)
let p = do_pass Schedule.program "Scheduling" p pp true in
(* Parametrized functions instantiation *)
let p = do_pass Callgraph.program
let p = do_pass Callgraph.program
"Parametrized functions instantiation" p pp true in
p
p

64
compiler/minils/main/mlsc.ml
View file

@ -38,20 +38,20 @@ let compile_impl modname filename =
let source_name = filename ^ ".mls"
and mls_norm_name = filename ^ "_norm.mls"
and obc_name = filename ^ ".obc" in
let ic = open_in source_name
and mlsnc = open_out mls_norm_name
and obc = open_out obc_name in
let close_all_files () =
close_in ic;
close_out obc;
close_out mlsnc
in
try
init_compiler modname source_name ic;
(* Parsing of the file *)
let lexbuf = Lexing.from_channel ic in
let p = parse_implementation lexbuf in
@ -60,28 +60,28 @@ let compile_impl modname filename =
comment "Parsing";
pp p
end;
(* Call the compiler*)
let p = Mls_compiler.compile pp p in
if !verbose
then begin
comment "Checking"
end;
(* Producing Object-based code *)
let o = Mls2obc.program p in
if !verbose then comment "Translation into Object-based code";
Obc.Printer.print obc o;
let pp = Obc.Printer.print stdout in
if !verbose then pp o;
(* Translation into dataflow and sequential languages *)
targets filename p o !target_languages;
(* Producing Object-based code *)
let o = Mls2obc.program p in
if !verbose then comment "Translation into Object-based code";
Obc.Printer.print obc o;
let pp = Obc.Printer.print stdout in
if !verbose then pp o;
(* Translation into dataflow and sequential languages *)
targets filename p o !target_languages;
close_all_files ()
with x -> close_all_files (); raise x
let compile file =
@ -98,22 +98,22 @@ let main () =
try
Arg.parse
[
"-v", Arg.Set verbose, doc_verbose;
"-version", Arg.Unit show_version, doc_version;
"-i", Arg.Set print_types, doc_print_types;
"-I", Arg.String add_include, doc_include;
"-where", Arg.Unit locate_stdlib, doc_locate_stdlib;
"-stdlib", Arg.String set_stdlib, doc_stdlib;
"-s", Arg.String set_simulation_node, doc_sim;
"-nopervasives", Arg.Unit set_no_pervasives, doc_no_pervasives;
"-target", Arg.String add_target_language, doc_target;
"-targetpath", Arg.String set_target_path, doc_target_path;
"-noinit", Arg.Clear init, doc_noinit;
"-fti", Arg.Set full_type_info, doc_full_type_info;
"-v", Arg.Set verbose, doc_verbose;
"-version", Arg.Unit show_version, doc_version;
"-i", Arg.Set print_types, doc_print_types;
"-I", Arg.String add_include, doc_include;
"-where", Arg.Unit locate_stdlib, doc_locate_stdlib;
"-stdlib", Arg.String set_stdlib, doc_stdlib;
"-s", Arg.String set_simulation_node, doc_sim;
"-nopervasives", Arg.Unit set_no_pervasives, doc_no_pervasives;
"-target", Arg.String add_target_language, doc_target;
"-targetpath", Arg.String set_target_path, doc_target_path;
"-noinit", Arg.Clear init, doc_noinit;
"-fti", Arg.Set full_type_info, doc_full_type_info;
]
compile
errmsg;
with
| Misc.Error -> exit 2;;
| Misc.Error -> exit 2;;
main ()

143
compiler/minils/minils.ml
View file

@ -18,7 +18,7 @@ open Signature
open Static
open Types
type iterator_type =
type iterator_type =
| Imap
| Ifold
| Imapfold
@ -45,9 +45,11 @@ and edesc =
| Econstvar of name
| Efby of const option * exp
| Etuple of exp list
| Ecall of op_desc * exp list * ident option (** [op_desc] is the function called
[exp list] is the passed arguments
[ident option] is the optional reset condition *)
| Ecall of op_desc * exp list * ident option (** [op_desc] is the function
called [exp list] is the
passed arguments [ident
option] is the optional reset
condition *)
| Ewhen of exp * longname * ident
| Emerge of ident * (longname * exp) list
@ -61,16 +63,17 @@ and edesc =
and array_op =
| Erepeat of size_exp * exp
| Eselect of size_exp list * exp (*indices, array*)
| Eselect_dyn of exp list * size_exp list * exp * exp (*indices, bounds, array, default*)
| Eselect_dyn of exp list * size_exp list * exp * exp (* indices, bounds,
array, default*)
| Eupdate of size_exp list * exp * exp (*indices, array, value*)
| Eselect_slice of size_exp * size_exp * exp (*lower bound, upper bound, array*)
| Eselect_slice of size_exp * size_exp * exp (*lower bound, upper bound,
array*)
| Econcat of exp * exp
| Eiterator of iterator_type * op_desc * size_exp * exp list * ident option (**
[op_desc] is the function iterated,
[size_exp] is the size of the iteration,
[exp list] is the passed arguments,
[ident option] is the optional reset condition *)
| Eiterator of iterator_type * op_desc * size_exp * exp list * ident option
(** [op_desc] is the function iterated, [size_exp] is the size of the
iteration, [exp list] is the passed arguments, [ident option] is the
optional reset condition *)
and op_desc = { op_name: longname; op_params: size_exp list; op_kind: op_kind }
and op_kind = | Eop | Enode
@ -91,7 +94,7 @@ and const =
| Cint of int
| Cfloat of float
| Cconstr of longname
| Carray of size_exp * const
| Carray of size_exp * const
and pat =
| Etuplepat of pat list
@ -123,7 +126,7 @@ type node_dec =
n_local : var_dec list;
n_equs : eq list;
n_loc : location;
n_params : param list;
n_params : param list;
n_params_constraints : size_constr list;
n_params_instances : (int list) list; }(*TODO commenter ou passer en env*)
@ -153,36 +156,36 @@ let mk_var_dec ?(clock = Cbase) name ty =
let mk_equation ?(loc = no_location) pat exp =
{ eq_lhs = pat; eq_rhs = exp; eq_loc = loc }
let mk_node
?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = [])
?(loc = no_location) ?(param = []) ?(constraints = []) ?(pinst = []) name =
{ n_name = name;
n_input = input;
n_output = output;
n_contract = contract;
n_local = local;
n_equs = eq;
n_loc = loc;
n_params = param;
n_params_constraints = constraints;
n_params_instances = pinst; }
?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = [])
?(loc = no_location) ?(param = []) ?(constraints = []) ?(pinst = []) name =
{ n_name = name;
n_input = input;
n_output = output;
n_contract = contract;
n_local = local;
n_equs = eq;
n_loc = loc;
n_params = param;
n_params_constraints = constraints;
n_params_instances = pinst; }
let mk_type_dec ?(type_desc = Type_abs) ?(loc = no_location) name =
{ t_name = name; t_desc = type_desc; t_loc = loc }
let rec size_exp_of_exp e =
match e.e_desc with
| Econstvar n -> SVar n
| Econst (Cint i) -> SConst i
| Ecall(op, [e1;e2], _) ->
let sop = op_from_app_name op.op_name in
SOp(sop, size_exp_of_exp e1, size_exp_of_exp e2)
| _ -> raise Not_static
match e.e_desc with
| Econstvar n -> SVar n
| Econst (Cint i) -> SConst i
| Ecall(op, [e1;e2], _) ->
let sop = op_from_app_name op.op_name in
SOp(sop, size_exp_of_exp e1, size_exp_of_exp e2)
| _ -> raise Not_static
(** @return the list of bounds of an array type*)
let rec bounds_list ty =
let rec bounds_list ty =
match ty with
| Tarray(ty, n) -> n::(bounds_list ty)
| _ -> []
@ -191,10 +194,10 @@ let rec bounds_list ty =
in a list of [var_dec]. *)
let rec vd_find n = function
| [] -> Format.printf "Not found var %s\n" (name n); raise Not_found
| vd::l ->
| vd::l ->
if vd.v_name = n then vd else vd_find n l
(** @return whether an object of name [n] belongs to
(** @return whether an object of name [n] belongs to
a list of [var_dec]. *)
let rec vd_mem n = function
| [] -> false
@ -203,15 +206,15 @@ let rec vd_mem n = function
(** @return whether [ty] corresponds to a record type. *)
let is_record_type ty = match ty with
| Tid n ->
(try
ignore (Modules.find_struct n); true
with
Not_found -> false)
(try
ignore (Modules.find_struct n); true
with
Not_found -> false)
| _ -> false
module Vars =
struct
let add x acc =
let add x acc =
if List.mem x acc then acc else x :: acc
let rec vars_pat acc = function
@ -229,48 +232,48 @@ struct
| Evar n -> add n acc
| Emerge(x, c_e_list) ->
let acc = add x acc in
List.fold_left (fun acc (_, e) -> read is_left acc e) acc c_e_list
List.fold_left (fun acc (_, e) -> read is_left acc e) acc c_e_list
| Eifthenelse(e1, e2, e3) ->
read is_left (read is_left (read is_left acc e1) e2) e3
| Ewhen(e, c, x) ->
let acc = add x acc in
read is_left acc e
read is_left acc e
| Etuple(e_list) -> List.fold_left (read is_left) acc e_list
| Ecall(_, e_list, None) ->
| Ecall(_, e_list, None) ->
List.fold_left (read is_left) acc e_list
| Ecall(_, e_list, Some x) ->
let acc = add x acc in
List.fold_left (read is_left) acc e_list
List.fold_left (read is_left) acc e_list
| Efby(_, e) ->
if is_left then vars_ck acc e.e_ck else read is_left acc e
| Efield(e, _) -> read is_left acc e
| Estruct(f_e_list) ->
List.fold_left (fun acc (_, e) -> read is_left acc e) acc f_e_list
| Econst _ | Econstvar _ -> acc
| Efield_update (_, e1, e2) ->
read is_left (read is_left acc e1) e2
(*Array operators*)
| Earray e_list -> List.fold_left (read is_left) acc e_list
| Earray_op op -> read_array_op is_left acc op
| Econst _ | Econstvar _ -> acc
| Efield_update (_, e1, e2) ->
read is_left (read is_left acc e1) e2
(*Array operators*)
| Earray e_list -> List.fold_left (read is_left) acc e_list
| Earray_op op -> read_array_op is_left acc op
in
vars_ck acc e.e_ck
vars_ck acc e.e_ck
and read_array_op is_left acc = function
and read_array_op is_left acc = function
| Erepeat (_,e) -> read is_left acc e
| Eselect (_,e) -> read is_left acc e
| Eselect_dyn (e_list, _, e1, e2) ->
let acc = List.fold_left (read is_left) acc e_list in
read is_left (read is_left acc e1) e2
| Eupdate (_, e1, e2) ->
read is_left (read is_left acc e1) e2
| Eselect_slice (_ , _, e) -> read is_left acc e
| Econcat (e1, e2) ->
read is_left (read is_left acc e1) e2
| Eiterator (_, _, _, e_list, None) ->
List.fold_left (read is_left) acc e_list
| Eiterator (_, _, _, e_list, Some x) ->
| Eselect (_,e) -> read is_left acc e
| Eselect_dyn (e_list, _, e1, e2) ->
let acc = List.fold_left (read is_left) acc e_list in
read is_left (read is_left acc e1) e2
| Eupdate (_, e1, e2) ->
read is_left (read is_left acc e1) e2
| Eselect_slice (_ , _, e) -> read is_left acc e
| Econcat (e1, e2) ->
read is_left (read is_left acc e1) e2
| Eiterator (_, _, _, e_list, None) ->
List.fold_left (read is_left) acc e_list
| Eiterator (_, _, _, e_list, Some x) ->
let acc = add x acc in
List.fold_left (read is_left) acc e_list
List.fold_left (read is_left) acc e_list
let rec remove x = function
| [] -> []
@ -299,11 +302,11 @@ struct
match ck with
| Cbase | Cvar { contents = Cindex _ } -> l
| Con(ck, c, n) -> headrec ck (n :: l)
| Cvar { contents = Clink ck } -> headrec ck l
| Cvar { contents = Clink ck } -> headrec ck l
in
headrec ck []
headrec ck []
(** Returns a list of memory vars (x in x = v fby e)
(** Returns a list of memory vars (x in x = v fby e)
appearing in an equation. *)
let memory_vars ({ eq_lhs = _; eq_rhs = e } as eq) =
match e.e_desc with

62
compiler/minils/mls_printer.ml
View file

@ -8,15 +8,15 @@ open Signature
open Pp_tools
(** Every print_ function is boxed, that is it doesn't export break points,
Exceptions are print_list* print_type_desc *)
Exceptions are print_list* print_type_desc *)
(** Every print_ function is without heading white space,
except for print_type_desc *)
except for print_type_desc *)
(** Every print_ function is without heading carry return *)
let iterator_to_string i =
match i with
let iterator_to_string i =
match i with
| Imap -> "map"
| Ifold -> "fold"
| Imapfold -> "mapfold"
@ -40,13 +40,13 @@ let rec print_clock ff = function
let print_vd ff { v_name = n; v_type = ty; v_clock = ck } =
if !Misc.full_type_info then
fprintf ff "%a : %a :: %a" print_ident n print_type ty print_ck ck
fprintf ff "%a : %a :: %a" print_ident n print_type ty print_ck ck
else fprintf ff "%a : %a" print_ident n print_type ty
let print_local_vars ff = function
| [] -> ()
| l -> fprintf ff "@[<4>%a@]@\n" (print_list_r print_vd "var "";"";") l
let rec print_c ff = function
| Cint i -> fprintf ff "%d" i
| Cfloat f -> fprintf ff "%f" f
@ -58,7 +58,7 @@ let rec print_params ff l =
and print_node_params ff l =
fprintf ff "@[<2>%a@]" (print_list_r print_param "<<"","">>") l
and print_exp_tuple ff l =
fprintf ff "@[<2>%a@]" (print_list_r print_exp "("","")") l
@ -70,17 +70,17 @@ and print_index ff idx =
and print_dyn_index ff idx =
fprintf ff "@[<2>%a@]" (print_list print_exp "[""][""]") idx
and print_op ff op =
fprintf ff "%a%a" print_longname op.op_name print_params op.op_params
and print_exp ff e =
if !Misc.full_type_info then
if !Misc.full_type_info then
fprintf ff "%a : %a" print_exp_desc e.e_desc print_type e.e_ty
else fprintf ff "%a" print_exp_desc e.e_desc
and print_every ff reset =
print_opt (fun ff id -> fprintf ff " every %a" print_ident id) ff reset
print_opt (fun ff id -> fprintf ff " every %a" print_ident id) ff reset
and print_exp_desc ff = function
| Evar x -> print_ident ff x
@ -100,7 +100,7 @@ and print_exp_desc ff = function
| Emerge (x, tag_e_list) ->
fprintf ff "@[<2>merge %a@ %a@]"
print_ident x print_tag_e_list tag_e_list
| Etuple e_list ->
| Etuple e_list ->
print_exp_tuple ff e_list
| Efield (e, field) ->
fprintf ff "%a.%a" print_exp e print_longname field
@ -128,23 +128,23 @@ and print_array_op ff = function
print_exp e print_size_exp idx1 print_size_exp idx2
| Econcat (e1, e2) -> fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2
| Eiterator (it, f, n, e_list, r) ->
fprintf ff "@[<2>(%s (%a)<<%a>>)@,%a@]%a"
(iterator_to_string it)
print_op f
print_size_exp n
print_exp_tuple e_list
print_every r
fprintf ff "@[<2>(%s (%a)<<%a>>)@,%a@]%a"
(iterator_to_string it)
print_op f
print_size_exp n
print_exp_tuple e_list
print_every r
and print_tag_e_list ff tag_e_list =
fprintf ff "@[%a@]"
(print_list
(print_couple print_longname print_exp "("" -> "")") """""") tag_e_list
(print_couple print_longname print_exp "("" -> "")") """""") tag_e_list
let print_eq ff { eq_lhs = p; eq_rhs = e } =
if !Misc.full_type_info
then fprintf ff "@[<2>%a :: %a =@ %a@]"
print_pat p print_ck e.e_ck print_exp e
print_pat p print_ck e.e_ck print_exp e
else fprintf ff "@[<2>%a =@ %a@]" print_pat p print_exp e
@ -156,9 +156,9 @@ let print_open_module ff name = fprintf ff "open %a@." print_name name
let rec print_type_def ff { t_name = name; t_desc = tdesc } =
fprintf ff "@[<2>type %s%a@]@." name print_type_desc tdesc
(** Small exception to the rule,
adding a heading space itself when needed and exporting a break*)
adding a heading space itself when needed and exporting a break*)
and print_type_desc ff = function
| Type_abs -> () (* that's the reason of the exception *)
| Type_enum tag_name_list ->
@ -169,7 +169,7 @@ and print_type_desc ff = function
and print_field ff field =
fprintf ff "@[%a: %a@]" print_name field.f_name print_type field.f_type
let print_const_dec ff c =
fprintf ff "const %a = %a" print_name c.c_name
print_size_exp c.c_value
@ -178,13 +178,13 @@ let print_contract ff
{ c_local = l; c_eq = eqs;
c_assume = e_a; c_enforce = e_g; c_controllables = cl } =
fprintf ff "@[<v2>contract@\n%a%a@ assume %a;@ enforce %a@ with %a@]"
print_local_vars l
print_eqs eqs
print_exp e_a
print_exp e_g
print_vd_tuple cl
print_local_vars l
print_eqs eqs
print_exp e_a
print_exp e_g
print_vd_tuple cl
let print_node ff
{ n_name = n; n_input = ni; n_output = no;
n_contract = contract; n_local = nl; n_equs = ne; n_params = params } =

44
compiler/minils/sequential/c.ml
View file

@ -36,7 +36,7 @@ type cty =
| Cty_int (** C machine-dependent integer type. *)
| Cty_float (** C machine-dependent single-precision floating-point type. *)
| Cty_char (** C character type. *)
| Cty_id of string (** Previously defined C type, such as an enum or struct. *)
| Cty_id of string (** Previously defined C type, such as an enum or struct.*)
| Cty_ptr of cty (** C points-to-other-type type. *)
| Cty_arr of int * cty (** A static array of the specified size. *)
| Cty_void (** Well, [void] is not really a C type. *)
@ -64,7 +64,7 @@ and cexpr =
| Cconst of cconst (** Constants. *)
| Clhs of clhs (** Left-hand-side expressions are obviously expressions! *)
| Caddrof of clhs (** Take the address of a left-hand-side expression. *)
| Cstructlit of string * cexpr list (** Structure literal "{ f1, f2, ... }". *)
| Cstructlit of string * cexpr list (** Structure literal "{ f1, f2, ... }".*)
| Carraylit of cexpr list (** Array literal [e1, e2, ...]. *)
and cconst =
| Ccint of int (** Integer constant. *)
@ -84,7 +84,7 @@ and cstm =
| Cskip (** A dummy instruction that does nothing and will not be printed. *)
| Caffect of clhs * cexpr (** Affect the result of an expression to a lhs. *)
| Cif of cexpr * cstm list * cstm list (** Alternative *)
| Cswitch of cexpr * (string * cstm list) list (** Case/switch over an enum. *)
| Cswitch of cexpr * (string * cstm list) list (** Case/switch over an enum.*)
| Cwhile of cexpr * cstm list (** While loop. *)
| Cfor of string * int * int * cstm list (** For loop. int <= string < int *)
| Creturn of cexpr (** Ends a procedure/function by returning an expression.*)
@ -110,7 +110,7 @@ type cfundef = {
(** C top-level definitions. *)
type cdef =
| Cfundef of cfundef (** Function definition, see [cfundef]. *)
| Cvardef of string * cty (** A variable definition, with its name and type. *)
| Cvardef of string * cty (** A variable definition, with its name and type.*)
(** [cdecl_of_cfundef cfd] returns a declaration for the function def. [cfd]. *)
let cdecl_of_cfundef cfd = match cfd with
@ -129,9 +129,9 @@ and cfile_desc =
(** {3 Pretty-printing of the C ast.} *)
(** [pp_list1 f sep fmt l] pretty-prints into the Format.formatter [fmt] elements
of the list [l] via the function [f], separated by [sep] strings and
breakable spaces. *)
(** [pp_list1 f sep fmt l] pretty-prints into the Format.formatter [fmt]
elements of the list [l] via the function [f], separated by [sep] strings
and breakable spaces. *)
let rec pp_list1 f sep fmt l = match l with
| [] -> fprintf fmt ""
| [x] -> fprintf fmt "%a" f x
@ -156,17 +156,17 @@ let rec pp_cty fmt cty = match cty with
and the string of indices. *)
let rec pp_array_decl cty =
match cty with
| Cty_arr(n, cty') ->
let ty, s = pp_array_decl cty' in
ty, sprintf "%s[%d]" s n
| Cty_arr(n, cty') ->
let ty, s = pp_array_decl cty' in
ty, sprintf "%s[%d]" s n
| _ -> cty, ""
(* pp_vardecl, featuring an ugly hack coping with C's inconsistent concrete
syntax! *)
let rec pp_vardecl fmt (s, cty) = match cty with
| Cty_arr (n, cty') ->
| Cty_arr (n, cty') ->
let ty, indices = pp_array_decl cty in
fprintf fmt "%a %s%s" pp_cty ty s indices
fprintf fmt "%a %s%s" pp_cty ty s indices
| _ -> fprintf fmt "%a %s" pp_cty cty s
and pp_paramdecl fmt (s, cty) = match cty with
| Cty_arr (n, cty') -> fprintf fmt "%a* %s" pp_cty cty' s
@ -196,7 +196,7 @@ and pp_cstm fmt stm = match stm with
pp_cexpr c pp_cstm_list t pp_cstm_list e
| Cfor(x, lower, upper, e) ->
fprintf fmt "@[<v>@[<v 2>for (int %s = %d; %s < %d; ++%s) {%a@]@ }@]"
x lower x upper x pp_cstm_list e
x lower x upper x pp_cstm_list e
| Cwhile (e, b) ->
fprintf fmt "@[<v>@[<v 2>while (%a) {%a@]@ }@]" pp_cexpr e pp_cstm_list b
| Csblock cb -> pp_cblock fmt cb
@ -216,7 +216,7 @@ and pp_cexpr fmt ce = match ce with
| Caddrof lhs -> fprintf fmt "&%a" pp_clhs lhs
| Cstructlit (s, el) ->
fprintf fmt "(%s){@[%a@]}" s (pp_list1 pp_cexpr ",") el
| Carraylit el ->
| Carraylit el ->
fprintf fmt "[@[%a@]]" (pp_list1 pp_cexpr ",") el
and pp_clhs fmt lhs = match lhs with
| Cvar s -> fprintf fmt "%s" s
@ -224,9 +224,9 @@ and pp_clhs fmt lhs = match lhs with
| Cfield (Cderef lhs, f) -> fprintf fmt "%a->%s" pp_clhs lhs f
| Cfield (lhs, f) -> fprintf fmt "%a.%s" pp_clhs lhs f
| Carray (lhs, e) ->
fprintf fmt "%a[%a]"
pp_clhs lhs
pp_cexpr e
fprintf fmt "%a[%a]"
pp_clhs lhs
pp_cexpr e
let pp_cdecl fmt cdecl = match cdecl with
| Cdecl_enum (s, sl) ->
@ -313,17 +313,17 @@ let lhs_of_exp e =
| Clhs e -> e
| _ -> assert false
(** Returns the type of a pointer to a type, except for
(** Returns the type of a pointer to a type, except for
types which are already pointers. *)
let pointer_to ty =
let pointer_to ty =
match ty with
| Cty_arr _ | Cty_ptr _ -> ty
| _ -> Cty_ptr ty
| Cty_arr _ | Cty_ptr _ -> ty
| _ -> Cty_ptr ty
(** Returns whether a type is a pointer. *)
let is_pointer_type = function
| Cty_arr _ | Cty_ptr _ -> true
| _ -> false
| _ -> false
(** [array_base_ctype ty idx_list] returns the base type of an array
type. If idx_list = [i1; ..; ip] and a is a variable of type ty,

13
compiler/minils/sequential/c.mli
View file

@ -21,7 +21,7 @@ type cty =
| Cty_int (** C machine-dependent integer type. *)
| Cty_float (** C machine-dependent single-precision floating-point type. *)
| Cty_char (** C character type. *)
| Cty_id of string (** Previously defined C type, such as an enum or struct. *)
| Cty_id of string (** Previously defined C type, such as an enum or struct.*)
| Cty_ptr of cty (** C points-to-other-type type. *)
| Cty_arr of int * cty (** A static array of the specified size. *)
| Cty_void (** Well, [void] is not really a C type. *)
@ -45,7 +45,8 @@ and cexpr =
| Cconst of cconst (** Constants. *)
| Clhs of clhs (** Left-hand-side expressions are obviously expressions! *)
| Caddrof of clhs (** Take the address of a left-hand-side expression. *)
| Cstructlit of string * cexpr list (** Structure literal " \{f1, f2, ... \}". *)
| Cstructlit of string * cexpr list (** Structure literal
" \{f1, f2, ... \}". *)
| Carraylit of cexpr list (** Array literal [e1, e2, ...]. *)
and cconst =
| Ccint of int (** Integer constant. *)
@ -65,7 +66,7 @@ and cstm =
| Cskip (** A dummy instruction that does nothing and will not be printed. *)
| Caffect of clhs * cexpr (** Affect the result of an expression to a lhs. *)
| Cif of cexpr * cstm list * cstm list (** Alternative *)
| Cswitch of cexpr * (string * cstm list) list (** Case/switch over an enum. *)
| Cswitch of cexpr * (string * cstm list) list (** Case/switch over an enum.*)
| Cwhile of cexpr * cstm list (** While loop. *)
| Cfor of string * int * int * cstm list (** For loop. int <= string < int *)
| Creturn of cexpr (** Ends a procedure/function by returning an expression.*)
@ -91,7 +92,7 @@ type cfundef = {
(** C top-level definitions. *)
type cdef =
| Cfundef of cfundef (** Function definition, see [cfundef]. *)
| Cvardef of string * cty (** A variable definition, with its name and type. *)
| Cvardef of string * cty (** A variable definition, with its name and type.*)
val cdecl_of_cfundef : cdef -> cdecl
@ -102,7 +103,7 @@ type cfile_desc =
list *)
| Csource of cdef list
type cfile = string * cfile_desc (** File name * file content *)
type cfile = string * cfile_desc (** File name * file content *)
(** [output dir cprog] pretty-prints the C program [cprog] to new files in the
directory [dir]. *)
@ -115,7 +116,7 @@ val cname_of_name : string -> string
(** Converts an expression to a lhs. *)
val lhs_of_exp : cexpr -> clhs
(** Returns the type of a pointer to a type, except for
(** Returns the type of a pointer to a type, except for
types which are already pointers. *)
val pointer_to : cty -> cty

159
compiler/minils/sequential/cgen.ml
View file

@ -38,19 +38,20 @@ struct
output_location loc
name
| Eno_unnamed_output ->
eprintf "%aCode generation : Unnamed outputs are not supported. \n"
eprintf "%aCode generation : Unnamed outputs are not supported.\n"
output_location loc
| Ederef_not_pointer ->
eprintf "%aCode generation : Trying to deference a non pointer type. \n"
eprintf
"%aCode generation : Trying to deference a non pointer type.\n"
output_location loc
end;
raise Misc.Error
end
let rec struct_name ty =
let rec struct_name ty =
match ty with
| Cty_id n -> n
| _ -> assert false
| Cty_id n -> n
| _ -> assert false
let cname_of_name' name = match name with
| Name n -> Name (cname_of_name n)
@ -110,8 +111,8 @@ let is_scalar_type ty =
match ty with
| Types.Tid name_int when name_int = Initial.pint -> true
| Types.Tid name_float when name_float = Initial.pfloat -> true
| Types.Tid name_bool when name_bool = Initial.pbool -> true
| _ -> false
| Types.Tid name_bool when name_bool = Initial.pbool -> true
| _ -> false
(******************************)
@ -145,12 +146,12 @@ let rec ctype_of_otype oty =
let ctype_of_heptty ty =
let ty = Mls2obc.translate_type NamesEnv.empty ty in
ctype_of_otype ty
ctype_of_otype ty
let cvarlist_of_ovarlist vl =
let cvar_of_ovar vd =
let ty = ctype_of_otype vd.v_type in
name vd.v_name, ty
name vd.v_name, ty
in
List.map cvar_of_ovar vl
@ -209,41 +210,41 @@ let rec assoc_type_lhs lhs var_env =
| Carray (lhs, _) ->
let ty = assoc_type_lhs lhs var_env in
array_base_ctype ty [1]
| Cderef lhs ->
(match assoc_type_lhs lhs var_env with
| Cty_ptr ty -> ty
| _ -> Error.message no_location Error.Ederef_not_pointer
)
| Cderef lhs ->
(match assoc_type_lhs lhs var_env with
| Cty_ptr ty -> ty
| _ -> Error.message no_location Error.Ederef_not_pointer
)
| Cfield(Cderef (Cvar "self"), x) -> assoc_type x var_env
| Cfield(x, f) ->
let ty = assoc_type_lhs x var_env in
let n = struct_name ty in
let { info = fields } = find_struct (longname n) in
ctype_of_heptty (field_assoc (Name f) fields)
ctype_of_heptty (field_assoc (Name f) fields)
(** Creates the statement a = [e_1, e_2, ..], which gives a list
a[i] = e_i.*)
let rec create_affect_lit dest l ty =
let rec create_affect_lit dest l ty =
let rec _create_affect_lit dest i = function
| [] -> []
| v::l ->
let stm = create_affect_stm (Carray (dest, Cconst (Ccint i))) v ty in
stm@(_create_affect_lit dest (i+1) l)
| v::l ->
let stm = create_affect_stm (Carray (dest, Cconst (Ccint i))) v ty in
stm@(_create_affect_lit dest (i+1) l)
in
_create_affect_lit dest 0 l
_create_affect_lit dest 0 l
(** Creates the expression dest <- src (copying arrays if necessary). *)
and create_affect_stm dest src ty =
match ty with
| Cty_arr (n, bty) ->
(match src with
| Carraylit l -> create_affect_lit dest l bty
| Clhs src ->
(match src with
| Carraylit l -> create_affect_lit dest l bty
| Clhs src ->
let x = gen_symbol () in
[Cfor(x, 0, n,
create_affect_stm (Carray (dest, Clhs (Cvar x)))
(Clhs (Carray (src, Clhs (Cvar x)))) bty)]
)
[Cfor(x, 0, n,
create_affect_stm (Carray (dest, Clhs (Cvar x)))
(Clhs (Carray (src, Clhs (Cvar x)))) bty)]
)
| _ -> [Caffect (dest, src)]
(** Returns the expression to use e as an argument of
@ -267,12 +268,12 @@ let rec cexpr_of_exp var_env exp =
(** Constants, the easiest translation. *)
| Const lit ->
(match lit with
| Cint i -> Cconst (Ccint i)
| Cfloat f -> Cconst (Ccfloat f)
| Cconstr c -> Cconst (Ctag (shortname c))
| Obc.Carray(n,c) ->
let cc = cexpr_of_exp var_env (Const c) in
Carraylit (repeat_list cc n)
| Cint i -> Cconst (Ccint i)
| Cfloat f -> Cconst (Ccfloat f)
| Cconstr c -> Cconst (Ctag (shortname c))
| Obc.Carray(n,c) ->
let cc = cexpr_of_exp var_env (Const c) in
Carraylit (repeat_list cc n)
)
(** Operators *)
| Op(op, exps) ->
@ -281,7 +282,7 @@ let rec cexpr_of_exp var_env exp =
| Struct_lit (tyn, fl) ->
let cexps = List.map (fun (_,e) -> cexpr_of_exp var_env e) fl in
let ctyn = shortname tyn in
Cstructlit (ctyn, cexps)
Cstructlit (ctyn, cexps)
| Array_lit e_list ->
Carraylit (cexprs_of_exps var_env e_list)
@ -311,25 +312,25 @@ and cop_of_op_aux var_env op_name cexps =
and cop_of_op var_env op_name exps =
let cexps = cexprs_of_exps var_env exps in
cop_of_op_aux var_env op_name cexps
cop_of_op_aux var_env op_name cexps
and clhs_of_lhs var_env = function
(** Each Obc variable corresponds to a real local C variable. *)
(** Each Obc variable corresponds to a real local C variable. *)
| Var v ->
let n = name v in
if List.mem_assoc n var_env then
let ty = assoc_type n var_env in
(match ty with
| Cty_ptr _ -> Cderef (Cvar n)
| _ -> Cvar n
)
else
Cvar n
if List.mem_assoc n var_env then
let ty = assoc_type n var_env in
(match ty with
| Cty_ptr _ -> Cderef (Cvar n)
| _ -> Cvar n
)
else
Cvar n
(** Dereference our [self] struct holding the node's memory. *)
| Mem v -> Cfield (Cderef (Cvar "self"), name v)
(** Field access. /!\ Indexed Obj expression should be a valid lhs! *)
(** Field access. /!\ Indexed Obj expression should be a valid lhs! *)
| Field (l, fn) -> Cfield(clhs_of_lhs var_env l, shortname fn)
| Array (l, idx) ->
| Array (l, idx) ->
Carray(clhs_of_lhs var_env l, cexpr_of_exp var_env idx)
and clhss_of_lhss var_env lhss =
@ -337,7 +338,7 @@ and clhss_of_lhss var_env lhss =
and clhs_of_exp var_env exp = match exp with
| Lhs l -> clhs_of_lhs var_env l
(** We were passed an expression that is not translatable to a valid C lhs?! *)
(** We were passed an expression that is not translatable to a valid C lhs?!*)
| _ -> invalid_arg "clhs_of_exp: argument not a Var, Mem or Field"
let rec assoc_obj instance obj_env =
@ -350,8 +351,8 @@ let rec assoc_obj instance obj_env =
let assoc_cn instance obj_env =
match instance with
| Context obj
| Array_context (obj, _) -> (assoc_obj obj obj_env).cls
| Context obj
| Array_context (obj, _) -> (assoc_obj obj obj_env).cls
let is_op = function
| Modname { qual = "Pervasives"; id = _ } -> true
@ -368,18 +369,18 @@ let step_fun_call sig_info args mem =
[args] is the list of expressions to use as arguments.
[mem] is the lhs where is stored the node's context.*)
let generate_function_call var_env obj_env outvl objn args =
let mem =
let mem =
(match objn with
| Context o -> Cfield (Cderef (Cvar "self"), o)
| Array_context (o, l) ->
let l = clhs_of_lhs var_env l in
Carray (Cfield (Cderef (Cvar "self"), o), Clhs l)
| Context o -> Cfield (Cderef (Cvar "self"), o)
| Array_context (o, l) ->
let l = clhs_of_lhs var_env l in
Carray (Cfield (Cderef (Cvar "self"), o), Clhs l)
) in
(** Class name for the object to step. *)
(** Class name for the object to step. *)
let classln = assoc_cn objn obj_env in
let classn = shortname classln in
let mod_classn, sig_info = node_info classln in
let fun_call =
if is_op classln then
cop_of_op_aux var_env classln args
@ -388,7 +389,7 @@ let generate_function_call var_env obj_env outvl objn args =
holding structure. *)
let args = step_fun_call sig_info.info args mem in
(** Our C expression for the function call. *)
Cfun_call (classn ^ "_step", args)
Cfun_call (classn ^ "_step", args)
in
(** Act according to the length of our list. Step functions with
@ -436,7 +437,7 @@ let rec cstm_of_act var_env obj_env act =
let cte = cstm_of_act var_env obj_env te in
let cfe = cstm_of_act var_env obj_env fe in
[Cif (cc, cte, cfe)]
(** Translation of case into a C switch statement is simple enough: we
just recursively translate obj expressions and statements to
corresponding C constructs, and cautiously "shortnamize"
@ -447,17 +448,17 @@ let rec cstm_of_act var_env obj_env act =
List.map
(fun (c,act) -> shortname c, cstm_of_act var_env obj_env act) cl in
[Cswitch (cexpr_of_exp var_env e, ccl)]
(** For composition of statements, just recursively apply our
translation function on sub-statements. *)
| For (x, i1, i2, act) ->
[Cfor(name x, i1, i2, cstm_of_act var_env obj_env act)]
[Cfor(name x, i1, i2, cstm_of_act var_env obj_env act)]
| Comp (s1, s2) ->
let cstm1 = cstm_of_act var_env obj_env s1 in
let cstm2 = cstm_of_act var_env obj_env s2 in
cstm1@cstm2
(** Reinitialization of an object variable, extracting the reset
function's name from our environment [obj_env]. *)
| Reinit on ->
@ -472,28 +473,28 @@ let rec cstm_of_act var_env obj_env act =
let elt = [Caddrof( Carray(field, Clhs (Cvar x)) )] in
[Cfor(x, 0, obj.size,
[Csexpr (Cfun_call (classn ^ "_reset", elt ))] )]
(** Special case for x = 0^n^n...*)
| Assgn (vn, Const c) ->
let vn = clhs_of_lhs var_env vn in
create_affect_const var_env vn c
(** Purely syntactic translation from an Obc local variable to a C
local one, with recursive translation of the rhs expression. *)
| Assgn (vn, e) ->
let vn = clhs_of_lhs var_env vn in
let ty = assoc_type_lhs vn var_env in
let ce = cexpr_of_exp var_env e in
create_affect_stm vn ce ty
create_affect_stm vn ce ty
(** Step functions applications can return multiple values, so we use a
local structure to hold the results, before allocating to our
variables. *)
| Step_ap (outvl, objn, el) ->
let args = cexprs_of_exps var_env el in
let outvl = clhss_of_lhss var_env outvl in
generate_function_call var_env obj_env outvl objn args
let args = cexprs_of_exps var_env el in
let outvl = clhss_of_lhss var_env outvl in
generate_function_call var_env obj_env outvl objn args
(** Well, Nothing translates to no instruction. *)
| Nothing -> []
@ -522,7 +523,7 @@ let main_def_of_class_def cd =
let iter_var = Ident.name (Ident.fresh "i") in
let lhs = Carray (lhs, Clhs (Cvar iter_var)) in
let (reads, bufs) = read_lhs_of_ty lhs ty in
([Cfor (iter_var, 0, n, reads)], bufs)
([Cfor (iter_var, 0, n, reads)], bufs)
| _ ->
let rec mk_prompt lhs = match lhs with
| Cvar vn -> (vn, [])
@ -610,8 +611,8 @@ let main_def_of_class_def cd =
@ [Caddrof (Cvar "mem")] in
Cfun_call (cd.cl_id ^ "_step", args) in
concat scanf_calls
(* Our function returns something only when the node has exactly one
non-array output. *)
(* Our function returns something only when the node has exactly one
non-array output. *)
@ ([match cd.step.out with
| [{ v_type = Tarray _; }] -> Csexpr funcall
| [_] -> Caffect (Cvar "res", funcall)
@ -636,7 +637,7 @@ let main_def_of_class_def cd =
(** Builds the argument list of step function*)
let step_fun_args n sf =
let args = cvarlist_of_ovarlist sf.inp in
args @ [("self", Cty_ptr (Cty_id (n ^ "_mem")))]
args @ [("self", Cty_ptr (Cty_id (n ^ "_mem")))]
(** [fun_def_of_step_fun name obj_env mods sf] returns a C function definition
[name ^ "_out"] corresponding to the Obc step function [sf]. The object name
@ -855,7 +856,8 @@ let cfile_list_of_oprog name oprog =
List.iter add_opened_module deps;
let cfile_name = String.uncapitalize cd.cl_id in
let mem_cdecl,use_ctrlr,(cdecls, cdefs) = cdefs_and_cdecls_of_class_def cd in
let mem_cdecl,use_ctrlr,(cdecls, cdefs) =
cdefs_and_cdecls_of_class_def cd in
let cfile_mem = cfile_name ^ "_mem" in
add_opened_module cfile_mem;
@ -898,8 +900,9 @@ let global_file_header name prog =
let ty_decls = List.concat ty_decls in
let mem_step_fun_decls = List.map mem_decl_of_class_def prog.o_defs in
let reset_fun_decls =
List.map
(fun cd -> cdecl_of_cfundef (reset_fun_def_of_class_def cd)) prog.o_defs in
let cdecl_of_reset_fun cd =
cdecl_of_cfundef (reset_fun_def_of_class_def cd) in
List.map cdecl_of_reset_fun prog.o_defs in
let step_fun_decls = List.map step_fun_decl prog.o_defs in
(name ^ ".h", Cheader (get_opened_modules (),
@ -912,5 +915,5 @@ let global_file_header name prog =
let translate name prog =
let modname = (Filename.basename name) in
global_name := String.capitalize modname;
(global_file_header modname prog) :: (cfile_list_of_oprog modname prog)
global_name := String.capitalize modname;
(global_file_header modname prog) :: (cfile_list_of_oprog modname prog)

30
compiler/minils/sequential/control.ml
View file

@ -17,7 +17,7 @@ open Misc
let var_from_name map x =
begin try
Env.find x map
Env.find x map
with
_ -> assert false
end
@ -37,25 +37,25 @@ let rec control map ck s =
let rec simplify act =
match act with
| Obc.Assgn (lhs, e) ->
(match e with
| Obc.Lhs l when l = lhs -> Obc.Nothing
| _ -> act
)
| Obc.Case(lhs, h) ->
(match simplify_handlers h with
| [] -> Obc.Nothing
| h -> Obc.Case(lhs, h)
)
| _ -> act
| Obc.Assgn (lhs, e) ->
(match e with
| Obc.Lhs l when l = lhs -> Obc.Nothing
| _ -> act
)
| Obc.Case(lhs, h) ->
(match simplify_handlers h with
| [] -> Obc.Nothing
| h -> Obc.Case(lhs, h)
)
| _ -> act
and simplify_handlers = function
| [] -> []
| (n,a)::h ->
| (n,a)::h ->
let h = simplify_handlers h in
(match simplify a with
| Obc.Nothing -> h
| a -> (n,a)::h
| Obc.Nothing -> h
| a -> (n,a)::h
)
let rec join s1 s2 =

47
compiler/minils/sequential/csubst.ml
View file

@ -2,35 +2,36 @@ open C
open Ident
open Names
let rec subst_stm map stm =
match stm with
let rec subst_stm map stm =
match stm with
| Csexpr e -> Csexpr (subst_exp map e)
| Cskip -> Cskip
| Creturn e -> Creturn (subst_exp map e)
| Csblock cblock ->
Csblock (subst_block map cblock)
Csblock (subst_block map cblock)
| Caffect (lhs, e) ->
Caffect(subst_lhs map lhs, subst_exp map e)
Caffect(subst_lhs map lhs, subst_exp map e)
| Cif (e, truel, falsel) ->
Cif (subst_exp map e, subst_stm_list map truel,
subst_stm_list map falsel)
Cif (subst_exp map e, subst_stm_list map truel,
subst_stm_list map falsel)
| Cswitch (e, l) ->
Cswitch (subst_exp map e, List.map (fun (s, sl) -> s, subst_stm_list map sl) l)
| Cwhile (e, l) ->
Cwhile (subst_exp map e, subst_stm_list map l)
Cswitch (subst_exp map e,
List.map (fun (s, sl) -> s, subst_stm_list map sl) l)
| Cwhile (e, l) ->
Cwhile (subst_exp map e, subst_stm_list map l)
| Cfor (x, i1, i2, l) ->
Cfor (x, i1, i2, subst_stm_list map l)
Cfor (x, i1, i2, subst_stm_list map l)
and subst_stm_list map =
List.map (subst_stm map)
List.map (subst_stm map)
and subst_lhs map lhs =
and subst_lhs map lhs =
match lhs with
| Cvar n ->
if NamesEnv.mem n map then
NamesEnv.find n map
else
lhs
| Cvar n ->
if NamesEnv.mem n map then
NamesEnv.find n map
else
lhs
| Cfield (lhs, s) -> Cfield (subst_lhs map lhs, s)
| Carray (lhs, n) -> Carray (subst_lhs map lhs, n)
| Cderef lhs -> Cderef (subst_lhs map lhs)
@ -51,15 +52,15 @@ and subst_exp_list map =
and subst_block map b =
{ b with block_body = subst_stm_list map b.block_body }
let assoc_map_for_fun sf =
let assoc_map_for_fun sf =
match sf.Obc.out with
| [] -> NamesEnv.empty
| [vd] when Obc.is_scalar_type vd ->
NamesEnv.empty
| [vd] when Obc.is_scalar_type vd ->
NamesEnv.empty
| out ->
let fill_field map vd =
NamesEnv.add (name vd.Obc.v_name)
NamesEnv.add (name vd.Obc.v_name)
(Cfield (Cderef (Cvar "self"), name vd.Obc.v_name)) map
in
List.fold_left fill_field NamesEnv.empty out
in
List.fold_left fill_field NamesEnv.empty out

368
compiler/minils/sequential/java.ml
View file

@ -51,34 +51,34 @@ let java_type_default_value = function
| Tid t ->
begin try
let { info = ty_desc } = find_type (t) in
begin match ty_desc with
| Tenum _ ->
"int", "0"
| _ ->
let t = shortname t in
if t = "bool"
then ("boolean", "false")
else (t, "null")
end
begin match ty_desc with
| Tenum _ ->
"int", "0"
| _ ->
let t = shortname t in
if t = "bool"
then ("boolean", "false")
else (t, "null")
end
with Not_found ->
begin try
let { t_desc = tdesc } =
List.find (fun {t_name = tn} -> tn = (shortname t)) !o_types in
begin match tdesc with
| Type_enum _ ->
"int", "0"
| _ ->
let t = shortname t in
if t = "bool"
then ("boolean", "false")
else (t, "null")
end
with Not_found ->
let t = shortname t in
if t = "bool"
then ("boolean", "false")
else (t, "null")
end
begin try
let { t_desc = tdesc } =
List.find (fun {t_name = tn} -> tn = (shortname t)) !o_types in
begin match tdesc with
| Type_enum _ ->
"int", "0"
| _ ->
let t = shortname t in
if t = "bool"
then ("boolean", "false")
else (t, "null")
end
with Not_found ->
let t = shortname t in
if t = "bool"
then ("boolean", "false")
else (t, "null")
end
end
let print_type ff ty =
@ -125,8 +125,8 @@ let rec print_tags ff n = function
| [] -> ()
| tg :: tgs' ->
fprintf ff "@ public static final int %a = %d;"
print_name tg
n;
print_name tg
n;
print_tags ff (n+1) tgs'
(* assumes tn is already translated with jname_of_name *)
@ -140,23 +140,23 @@ let print_type_to_file java_dir headers { t_name = tn; t_desc = td} =
match td with
| Type_abs -> ()
| Type_enum tgs ->
let out_ch = open_out (java_dir ^ "/" ^ tn ^ ".java") in
let ff = formatter_of_out_channel out_ch in
Misc.print_header_info ff "/*" "*/";
List.iter (fprintf ff "%s") headers;
(* fprintf ff "@[<v>package %s;@\n@\n" headers; *)
print_enum_type ff tn tgs;
fprintf ff "@.";
close_out out_ch
let out_ch = open_out (java_dir ^ "/" ^ tn ^ ".java") in
let ff = formatter_of_out_channel out_ch in
Misc.print_header_info ff "/*" "*/";
List.iter (fprintf ff "%s") headers;
(* fprintf ff "@[<v>package %s;@\n@\n" headers; *)
print_enum_type ff tn tgs;
fprintf ff "@.";
close_out out_ch
| Type_struct fields ->
let out_ch = open_out (java_dir ^ "/" ^ tn ^ ".java") in
let ff = formatter_of_out_channel out_ch in
Misc.print_header_info ff "/*" "*/";
List.iter (fprintf ff "%s") headers;
(* fprintf ff "@[<v>package %s;@\n@\n" headers; *)
print_struct_type ff tn fields;
fprintf ff "@.";
close_out out_ch
let out_ch = open_out (java_dir ^ "/" ^ tn ^ ".java") in
let ff = formatter_of_out_channel out_ch in
Misc.print_header_info ff "/*" "*/";
List.iter (fprintf ff "%s") headers;
(* fprintf ff "@[<v>package %s;@\n@\n" headers; *)
print_struct_type ff tn fields;
fprintf ff "@.";
close_out out_ch
let print_types java_dir headers tps =
List.iter (print_type_to_file java_dir headers) tps
@ -174,20 +174,20 @@ let print_const ff c ts =
| Cconstr t ->
let s =
match t with
| Name("true")
| Modname({id = "true"}) -> "true"
| Name("false")
| Modname({id = "false"}) -> "false"
| Name(tg)
| Modname({id = tg}) ->
(fst
| Name("true")
| Modname({id = "true"}) -> "true"
| Name("false")
| Modname({id = "false"}) -> "false"
| Name(tg)
| Modname({id = tg}) ->
(fst
(List.find
(fun (tn, tgs) ->
List.exists (fun tg' -> tg = tg') tgs)
List.exists (fun tg' -> tg = tg') tgs)
ts))
^ "." ^ (jname_of_name tg)
^ "." ^ (jname_of_name tg)
in
fprintf ff "%s" s
fprintf ff "%s" s
let position a xs =
let rec walk i = function
@ -224,14 +224,14 @@ let priority = function
| "|" -> 1
| _ -> 0
let rec print_lhs ff e avs single =
match e with
| Var x ->
print_var ff x avs single
| Mem x -> print_ident ff x
| Field(e, field) ->
print_lhs ff e avs single;
fprintf ff ".%s" (jname_of_name (shortname field))
let rec print_lhs ff e avs single =
match e with
| Var x ->
print_var ff x avs single
| Mem x -> print_ident ff x
| Field(e, field) ->
print_lhs ff e avs single;
fprintf ff ".%s" (jname_of_name (shortname field))
let rec print_exp ff e p avs ts single =
match e with
@ -240,12 +240,13 @@ let rec print_exp ff e p avs ts single =
| Op (op, es) -> print_op ff op es p avs ts single
| Struct_lit(type_name,fields) ->
let fields =
List.sort
(fun (ln1,_) (ln2,_) -> String.compare (shortname ln1) (shortname ln2))
fields in
List.sort
(fun (ln1,_) (ln2,_) ->
String.compare (shortname ln1) (shortname ln2))
fields in
let exps = List.map (fun (_,e) -> e) fields in
fprintf ff "new %a(@[<hov>"
print_shortname type_name;
print_shortname type_name;
print_exps ff exps 0 avs ts single;
fprintf ff "@])"
@ -254,9 +255,9 @@ and print_exps ff es p avs ts single =
| [] -> ()
| [e] -> print_exp ff e p avs ts single
| e :: es' ->
print_exp ff e p avs ts single;
fprintf ff ",@ ";
print_exps ff es' p avs ts single
print_exp ff e p avs ts single;
fprintf ff ",@ ";
print_exps ff es' p avs ts single
and print_op ff op es p avs ts single =
match (shortname op), es with
@ -278,27 +279,27 @@ and print_op ff op es p avs ts single =
print_exp ff e 6 avs ts single;
| _ ->
begin
begin
match op with
| Name(op_name) ->
print_name ff op_name;
| Modname({ qual = mod_name; id = op_name }) ->
fprintf ff "%a.%a"
print_name (String.uncapitalize mod_name)
print_name op_name
end;
fprintf ff "@[(";
print_exps ff es 0 avs ts single;
fprintf ff ")@]"
begin
match op with
| Name(op_name) ->
print_name ff op_name;
| Modname({ qual = mod_name; id = op_name }) ->
fprintf ff "%a.%a"
print_name (String.uncapitalize mod_name)
print_name op_name
end;
fprintf ff "@[(";
print_exps ff es 0 avs ts single;
fprintf ff ")@]"
end
let rec print_proj ff xs ao avs single =
let rec walk ind = function
| [] -> ()
| x :: xs' ->
print_lhs ff x avs single;
fprintf ff " = %s.c_%d;@ " ao ind;
walk (ind + 1) xs'
print_lhs ff x avs single;
fprintf ff " = %s.c_%d;@ " ao ind;
walk (ind + 1) xs'
in walk 1 xs
@ -315,46 +316,46 @@ let obj_call_to_string = function
let rec print_act ff a objs avs ts single =
match a with
| Assgn (x, e) ->
fprintf ff "@[";
print_asgn ff x e avs ts single;
fprintf ff ";@]"
fprintf ff "@[";
print_asgn ff x e avs ts single;
fprintf ff ";@]"
| Step_ap (xs, o, es) ->
let o = obj_call_to_string o in
(match xs with
| [x] ->
print_lhs ff x avs single;
fprintf ff " = %s.step(" o;
fprintf ff "@[";
let o = obj_call_to_string o in
(match xs with
| [x] ->
print_lhs ff x avs single;
fprintf ff " = %s.step(" o;
fprintf ff "@[";
print_exps ff es 0 avs ts single;
fprintf ff "@]";
fprintf ff ");@ "
| xs ->
let cn = (List.find (fun od -> od.obj = o) objs).cls in
let at = (jname_of_name (shortname cn)) ^ "Answer" in
let ao = o ^ "_ans" in
fprintf ff "%s %s = new %s();@ " at ao at;
fprintf ff "%s = %s.step(" ao o;
fprintf ff "@[";
fprintf ff ");@ "
| xs ->
let cn = (List.find (fun od -> od.obj = o) objs).cls in
let at = (jname_of_name (shortname cn)) ^ "Answer" in
let ao = o ^ "_ans" in
fprintf ff "%s %s = new %s();@ " at ao at;
fprintf ff "%s = %s.step(" ao o;
fprintf ff "@[";
print_exps ff es 0 avs ts single;
fprintf ff "@]";
fprintf ff ");@ ";
print_proj ff xs ao avs single)
fprintf ff ");@ ";
print_proj ff xs ao avs single)
| Comp (a1, a2) ->
print_act ff a1 objs avs ts single;
(match a2 with
| Nothing -> ()
| _ -> fprintf ff "@ ");
print_act ff a2 objs avs ts single
print_act ff a1 objs avs ts single;
(match a2 with
| Nothing -> ()
| _ -> fprintf ff "@ ");
print_act ff a2 objs avs ts single
| Case (e, grds) ->
let grds =
List.map
(fun (ln,act) -> (shortname ln),act) grds in
if bool_case grds
then print_if ff e grds objs avs ts single
else (fprintf ff "@[<v>@[<v 2>switch (%a) {@ "
(fun ff e -> print_exp ff e 0 avs ts single) e;
print_grds ff grds objs avs ts single;
fprintf ff "@]@ }@]");
let grds =
List.map
(fun (ln,act) -> (shortname ln),act) grds in
if bool_case grds
then print_if ff e grds objs avs ts single
else (fprintf ff "@[<v>@[<v 2>switch (%a) {@ "
(fun ff e -> print_exp ff e 0 avs ts single) e;
print_grds ff grds objs avs ts single;
fprintf ff "@]@ }@]");
| Reinit o -> fprintf ff "%s.reset();" o
| Nothing -> ()
@ -362,57 +363,57 @@ and print_grds ff grds objs avs ts single =
match grds with
| [] -> ()
| [(tg, act)] ->
(* retrieve class name *)
let cn = (fst
(List.find
(fun (tn, tgs) ->
List.exists (fun tg' -> tg = tg') tgs)
ts)) in
fprintf ff "@[<v 2>case %a.%a:@ "
print_name cn
print_name tg;
print_act ff act objs avs ts single;
fprintf ff "@ break;@]";
(* retrieve class name *)
let cn = (fst
(List.find
(fun (tn, tgs) ->
List.exists (fun tg' -> tg = tg') tgs)
ts)) in
fprintf ff "@[<v 2>case %a.%a:@ "
print_name cn
print_name tg;
print_act ff act objs avs ts single;
fprintf ff "@ break;@]";
| (tg, act) :: grds' ->
(* retrieve class name *)
let cn = (fst
(List.find
(fun (tn, tgs) ->
List.exists (fun tg' -> tg = tg') tgs)
ts)) in
fprintf ff "@[<v 2>case %a.%a:@ "
print_name cn
print_name tg;
print_act ff act objs avs ts single;
fprintf ff "@ break;@ @]@ ";
print_grds ff grds' objs avs ts single
(* retrieve class name *)
let cn = (fst
(List.find
(fun (tn, tgs) ->
List.exists (fun tg' -> tg = tg') tgs)
ts)) in
fprintf ff "@[<v 2>case %a.%a:@ "
print_name cn
print_name tg;
print_act ff act objs avs ts single;
fprintf ff "@ break;@ @]@ ";
print_grds ff grds' objs avs ts single
and print_if ff e grds objs avs ts single =
match grds with
| [("true", a)] ->
fprintf ff "@[<v>@[<v 2>if (%a) {@ "
(fun ff e -> print_exp ff e 0 avs ts single) e;
print_act ff a objs avs ts single;
fprintf ff "@]@ }@]"
fprintf ff "@[<v>@[<v 2>if (%a) {@ "
(fun ff e -> print_exp ff e 0 avs ts single) e;
print_act ff a objs avs ts single;
fprintf ff "@]@ }@]"
| [("false", a)] ->
fprintf ff "@[<v>@[<v 2>if (!%a) {@ "
(fun ff e -> print_exp ff e 6 avs ts single) e;
print_act ff a objs avs ts single;
fprintf ff "@]@ }@]"
fprintf ff "@[<v>@[<v 2>if (!%a) {@ "
(fun ff e -> print_exp ff e 6 avs ts single) e;
print_act ff a objs avs ts single;
fprintf ff "@]@ }@]"
| [("true", a1); ("false", a2)] ->
fprintf ff "@[<v>@[<v 2>if (%a) {@ "
(fun ff e -> print_exp ff e 0 avs ts single) e;
print_act ff a1 objs avs ts single;
fprintf ff "@]@ @[<v 2>} else {@ ";
print_act ff a2 objs avs ts single;
fprintf ff "@]@ }@]"
fprintf ff "@[<v>@[<v 2>if (%a) {@ "
(fun ff e -> print_exp ff e 0 avs ts single) e;
print_act ff a1 objs avs ts single;
fprintf ff "@]@ @[<v 2>} else {@ ";
print_act ff a2 objs avs ts single;
fprintf ff "@]@ }@]"
| [("false", a2); ("true", a1)] ->
fprintf ff "@[<v>@[<v 2>if (%a) {@ "
(fun ff e -> print_exp ff e 0 avs ts single) e;
print_act ff a1 objs avs ts single;
fprintf ff "@]@ @[<v 2>} else {@ ";
print_act ff a2 objs avs ts single;
fprintf ff "@]@ }@]"
fprintf ff "@[<v>@[<v 2>if (%a) {@ "
(fun ff e -> print_exp ff e 0 avs ts single) e;
print_act ff a1 objs avs ts single;
fprintf ff "@]@ @[<v 2>} else {@ ";
print_act ff a2 objs avs ts single;
fprintf ff "@]@ }@]"
| _ -> assert false
and print_asgn ff x e avs ts single =
@ -443,19 +444,19 @@ let rec print_objs ff ods =
match ods with
| [] -> ()
| od :: ods' ->
print_obj ff od;
fprintf ff "@ ";
print_objs ff ods'
print_obj ff od;
fprintf ff "@ ";
print_objs ff ods'
let print_comps ff fds=
let rec walk n = function
| [] -> ()
| fd :: fds' ->
fprintf ff "@ ";
fprintf ff "public ";
fprintf ff "public ";
print_type ff fd.v_type;
fprintf ff " c_%s;" (string_of_int n);
walk (n + 1) fds'
walk (n + 1) fds'
in walk 1 fds
let print_ans_struct ff name fields =
@ -480,9 +481,9 @@ let rec print_in ff = function
let rec print_mem ff = function
| [] -> ()
| vd :: m' ->
print_vd ff vd;
fprintf ff "@ ";
print_mem ff m'
print_vd ff vd;
fprintf ff "@ ";
print_mem ff m'
let print_loc ff vds = print_mem ff vds
@ -501,7 +502,8 @@ let print_step ff n s objs ts single =
print_act ff s.bd objs
(List.map (fun vd -> vd.v_name) s.out) ts single;
fprintf ff "@ @ return ";
if single then fprintf ff "%s" (jname_of_name (Ident.name (List.hd s.out).v_name))
if single
then fprintf ff "%s" (jname_of_name (Ident.name (List.hd s.out).v_name))
else fprintf ff "step_ans";
fprintf ff ";@]@ }@ @]"
@ -513,7 +515,7 @@ let print_reset ff r ts =
let print_class ff headers ts single opened_mod cl =
let clid = jname_of_name cl.cl_id in
List.iter (fprintf ff "%s") headers;
(* fprintf ff "@[<v>package %s;@\n@\n" headers; *)
(* fprintf ff "@[<v>package %s;@\n@\n" headers; *)
(* import opened modules *)
List.iter
(fun m ->
@ -545,17 +547,17 @@ let print_class_and_answer_to_file java_dir headers ts opened_mod cl =
let out_ch = open_out (java_dir ^ "/" ^ clid ^ "Answer.java") in
let ff = formatter_of_out_channel out_ch in
Misc.print_header_info ff "/*" "*/";
List.iter (fprintf ff "%s") headers;
(* fprintf ff "@[<v>package %s;@\n@\n" headers; *)
List.iter (fprintf ff "%s") headers;
(* fprintf ff "@[<v>package %s;@\n@\n" headers; *)
List.iter
(fun m ->
fprintf ff "import %s.*;@\n" (String.uncapitalize m))
opened_mod;
(fun m ->
fprintf ff "import %s.*;@\n" (String.uncapitalize m))
opened_mod;
print_ans_struct ff (clid ^ "Answer") cl.step.out;
fprintf ff "@.";
close_out out_ch;
print_class_to_file false
let print_classes java_dir headers ts opened_mod cls =
List.iter
(print_class_and_answer_to_file java_dir headers ts opened_mod)
@ -563,11 +565,11 @@ let print_classes java_dir headers ts opened_mod cls =
(******************************)
let print java_dir p =
let headers =
List.map snd
(List.filter
(fun (tag,_) -> tag = "java")
p.o_pragmas) in
let headers =
List.map snd
(List.filter
(fun (tag,_) -> tag = "java")
p.o_pragmas) in
print_types java_dir headers p.o_types;
o_types := p.o_types;
print_classes
@ -578,7 +580,7 @@ let print java_dir p =
| { t_desc = Type_abs } -> []
| { t_name = tn; t_desc = Type_enum tgs } -> [tn, tgs]
| { t_name = tn; t_desc = Type_struct fields } ->
[tn, (List.map fst fields)])
[tn, (List.map fst fields)])
p.o_types))
p.o_opened
p.o_defs

438
compiler/minils/sequential/mls2obc.ml
View file

@ -15,121 +15,122 @@ open Signature
open Obc
open Control
open Static
let rec encode_name_params n =
function
| [] -> n
| p :: params -> encode_name_params (n ^ ("__" ^ (string_of_int p))) params
| [] -> n
| p :: params -> encode_name_params (n ^ ("__" ^ (string_of_int p))) params
let encode_longname_params n params =
match n with
| Name n -> Name (encode_name_params n params)
| Modname { qual = qual; id = id } ->
Modname { qual = qual; id = encode_name_params id params; }
let is_op = function
| Name n -> Name (encode_name_params n params)
| Modname { qual = qual; id = id } ->
Modname { qual = qual; id = encode_name_params id params; }
let is_op = function
| Modname { qual = "Pervasives"; id = _ } -> true | _ -> false
let op_from_string op = Modname { qual = "Pervasives"; id = op; }
let rec lhs_of_idx_list e = function
let rec lhs_of_idx_list e = function
| [] -> e | idx :: l -> Array (lhs_of_idx_list e l, idx)
let array_elt_of_exp idx e =
match e with
| Const (Carray (_, c)) ->
Const c
| _ ->
| _ ->
Lhs (Array(lhs_of_exp e, Lhs idx))
(** Creates the expression that checks that the indices
in idx_list are in the bounds. If idx_list=[e1;..;ep]
and bounds = [n1;..;np], it returns
e1 <= n1 && .. && ep <= np *)
let rec bound_check_expr idx_list bounds =
match (idx_list, bounds) with
| ([ idx ], [ n ]) -> Op (op_from_string "<", [ idx; Const (Cint n) ])
| (idx :: idx_list, n :: bounds) ->
Op (op_from_string "&",
[ Op (op_from_string "<", [ idx; Const (Cint n) ]);
bound_check_expr idx_list bounds ])
| (_, _) -> assert false
| ([ idx ], [ n ]) -> Op (op_from_string "<", [ idx; Const (Cint n) ])
| (idx :: idx_list, n :: bounds) ->
Op (op_from_string "&",
[ Op (op_from_string "<", [ idx; Const (Cint n) ]);
bound_check_expr idx_list bounds ])
| (_, _) -> assert false
let rec translate_type const_env =
function
| Types.Tid id when id = Initial.pint -> Tint
| Types.Tid id when id = Initial.pfloat -> Tfloat
| Types.Tid id when id = Initial.pbool -> Tbool
| Types.Tid id -> Tid id
| Types.Tarray (ty, n) ->
Tarray (translate_type const_env ty, int_of_size_exp const_env n)
| Types.Tprod ty -> assert false
| Types.Tid id when id = Initial.pint -> Tint
| Types.Tid id when id = Initial.pfloat -> Tfloat
| Types.Tid id when id = Initial.pbool -> Tbool
| Types.Tid id -> Tid id
| Types.Tarray (ty, n) ->
Tarray (translate_type const_env ty, int_of_size_exp const_env n)
| Types.Tprod ty -> assert false
let rec translate_const const_env =
function
| Minils.Cint v -> Cint v
| Minils.Cfloat v -> Cfloat v
| Minils.Cconstr c -> Cconstr c
| Minils.Carray (n, c) ->
Carray (int_of_size_exp const_env n, translate_const const_env c)
| Minils.Cint v -> Cint v
| Minils.Cfloat v -> Cfloat v
| Minils.Cconstr c -> Cconstr c
| Minils.Carray (n, c) ->
Carray (int_of_size_exp const_env n, translate_const const_env c)
let rec translate_pat map =
function
| Minils.Evarpat x -> [ var_from_name map x ]
| Minils.Etuplepat pat_list ->
List.fold_right (fun pat acc -> (translate_pat map pat) @ acc)
pat_list []
| Minils.Evarpat x -> [ var_from_name map x ]
| Minils.Etuplepat pat_list ->
List.fold_right (fun pat acc -> (translate_pat map pat) @ acc)
pat_list []
(* [translate e = c] *)
let rec
translate const_env map (m, si, j, s) (({ Minils.e_desc = desc } as e)) =
translate const_env map (m, si, j, s) (({ Minils.e_desc = desc } as e)) =
match desc with
| Minils.Econst v -> Const (translate_const const_env v)
| Minils.Evar n -> Lhs (var_from_name map n)
| Minils.Econstvar n -> Const (Cint (int_of_size_exp const_env (SVar n)))
| Minils.Ecall ( { Minils.op_name = n; Minils.op_kind = Minils.Eop }, e_list, _) ->
Op (n, List.map (translate const_env map (m, si, j, s)) e_list)
| Minils.Ewhen (e, _, _) -> translate const_env map (m, si, j, s) e
| Minils.Efield (e, field) ->
let e = translate const_env map (m, si, j, s) e
in Lhs (Field (lhs_of_exp e, field))
| Minils.Estruct f_e_list ->
let type_name =
(match e.Minils.e_ty with
| Types.Tid name -> name
| _ -> assert false) in
let f_e_list =
List.map
(fun (f, e) -> (f, (translate const_env map (m, si, j, s) e)))
f_e_list
in Struct_lit (type_name, f_e_list)
(*Array operators*)
| Minils.Earray e_list ->
Array_lit (List.map (translate const_env map (m, si, j, s)) e_list)
| Minils.Earray_op (Minils.Eselect (idx, e)) ->
let e = translate const_env map (m, si, j, s) e in
let idx_list =
List.map (fun e -> Const (Cint (int_of_size_exp const_env e))) idx
in
| Minils.Econst v -> Const (translate_const const_env v)
| Minils.Evar n -> Lhs (var_from_name map n)
| Minils.Econstvar n -> Const (Cint (int_of_size_exp const_env (SVar n)))
| Minils.Ecall ( { Minils.op_name = n;
Minils.op_kind = Minils.Eop }, e_list, _) ->
Op (n, List.map (translate const_env map (m, si, j, s)) e_list)
| Minils.Ewhen (e, _, _) -> translate const_env map (m, si, j, s) e
| Minils.Efield (e, field) ->
let e = translate const_env map (m, si, j, s) e
in Lhs (Field (lhs_of_exp e, field))
| Minils.Estruct f_e_list ->
let type_name =
(match e.Minils.e_ty with
| Types.Tid name -> name
| _ -> assert false) in
let f_e_list =
List.map
(fun (f, e) -> (f, (translate const_env map (m, si, j, s) e)))
f_e_list
in Struct_lit (type_name, f_e_list)
(*Array operators*)
| Minils.Earray e_list ->
Array_lit (List.map (translate const_env map (m, si, j, s)) e_list)
| Minils.Earray_op (Minils.Eselect (idx, e)) ->
let e = translate const_env map (m, si, j, s) e in
let idx_list =
List.map (fun e -> Const (Cint (int_of_size_exp const_env e))) idx
in
Lhs (lhs_of_idx_list (lhs_of_exp e) idx_list)
| _ -> (*Minils_printer.print_exp stdout e; flush stdout;*) assert false
| _ -> (*Minils_printer.print_exp stdout e; flush stdout;*) assert false
(* [translate pat act = si, j, d, s] *)
and translate_act const_env map ((m, _, _, _) as context) pat
({ Minils.e_desc = desc } as act) =
({ Minils.e_desc = desc } as act) =
match pat, desc with
| Minils.Etuplepat p_list, Minils.Etuple act_list ->
comp (List.map2 (translate_act const_env map context) p_list act_list)
| pat, Minils.Ewhen (e, _, _) ->
translate_act const_env map context pat e
| pat, Minils.Emerge (x, c_act_list) ->
let lhs = var_from_name map x
in
| Minils.Etuplepat p_list, Minils.Etuple act_list ->
comp (List.map2 (translate_act const_env map context) p_list act_list)
| pat, Minils.Ewhen (e, _, _) ->
translate_act const_env map context pat e
| pat, Minils.Emerge (x, c_act_list) ->
let lhs = var_from_name map x
in
Case (Lhs lhs,
translate_c_act_list const_env map context pat c_act_list)
| Minils.Evarpat n, _ ->
Assgn (var_from_name map n, translate const_env map context act)
| _ -> (*Minils_printer.print_exp stdout act;*) assert false
translate_c_act_list const_env map context pat c_act_list)
| Minils.Evarpat n, _ ->
Assgn (var_from_name map n, translate const_env map context act)
| _ -> (*Minils_printer.print_exp stdout act;*) assert false
and translate_c_act_list const_env map context pat c_act_list =
List.map
@ -138,26 +139,27 @@ and translate_c_act_list const_env map context pat c_act_list =
and comp s_list =
List.fold_right (fun s rest -> Comp (s, rest)) s_list Nothing
let rec
translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e }
(m, si, j, s) =
translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e }
(m, si, j, s) =
let { Minils.e_desc = desc; Minils.e_ty = ty; Minils.e_ck = ck } = e
in
match (pat, desc) with
match (pat, desc) with
| Minils.Evarpat n, Minils.Efby (opt_c, e) ->
let x = var_from_name map n in
let si =
(match opt_c with
| None -> si
| Some c -> (Assgn (x, Const (translate_const const_env c))) :: si) in
| None -> si
| Some c ->
(Assgn (x, Const (translate_const const_env c))) :: si) in
let ty = translate_type const_env ty in
let m = (n, ty) :: m in
let action =
Assgn (var_from_name map n,
translate const_env map (m, si, j, s) e)
in
m, si, j, (control map ck action) :: s
m, si, j, (control map ck action) :: s
| pat, Minils.Ecall ({ Minils.op_name = n; Minils.op_params = params;
Minils.op_kind = Minils.Enode },
@ -172,14 +174,14 @@ let rec
let action = Step_ap (name_list, Context o, c_list) in
let s =
(match r with
| None -> (control map ck action) :: s
| Some r ->
let ra =
control map (Minils.Con (ck, Name "true", r)) (Reinit o)
in ra :: (control map ck action) :: s
| None -> (control map ck action) :: s
| Some r ->
let ra =
control map (Minils.Con (ck, Name "true", r)) (Reinit o)
in ra :: (control map ck action) :: s
)
in
m, si, j, s
in
m, si, j, s
| Minils.Etuplepat p_list, Minils.Etuple act_list ->
List.fold_right2
@ -194,10 +196,10 @@ let rec
let action =
Assgn (Field (x, f), translate const_env map (m, si, j, s) e2)
in
m, si, j, (control map ck copy) :: (control map ck action) :: s
m, si, j, (control map ck copy) :: (control map ck action) :: s
| Minils.Evarpat x,
Minils.Earray_op (Minils.Eselect_slice (idx1, idx2, e)) ->
Minils.Earray_op (Minils.Eselect_slice (idx1, idx2, e)) ->
let idx1 = int_of_size_exp const_env idx1 in
let idx2 = int_of_size_exp const_env idx2 in
let cpt = Ident.fresh "i" in
@ -206,13 +208,13 @@ let rec
Op (op_from_string "+", [ Lhs (Var cpt); Const (Cint idx1) ]) in
let action =
For (cpt, 0, (idx2 - idx1) + 1,
Assgn (Array (var_from_name map x, Lhs (Var cpt)),
Lhs (Array (lhs_of_exp e, idx))))
in
m, si, j, (control map ck action) :: s
Assgn (Array (var_from_name map x, Lhs (Var cpt)),
Lhs (Array (lhs_of_exp e, idx))))
in
m, si, j, (control map ck action) :: s
| Minils.Evarpat x,
Minils.Earray_op (Minils.Eselect_dyn (idx, bounds, e1, e2)) ->
| Minils.Evarpat x,
Minils.Earray_op (Minils.Eselect_dyn (idx, bounds, e1, e2)) ->
let x = var_from_name map x in
let e1 = translate const_env map (m, si, j, s) e1 in
let bounds = List.map (int_of_size_exp const_env) bounds in
@ -224,12 +226,12 @@ let rec
let cond = bound_check_expr idx bounds in
let action =
Case (cond,
[ ((Name "true"), true_act); ((Name "false"), false_act) ])
in
m, si, j, (control map ck action) :: s
[ ((Name "true"), true_act); ((Name "false"), false_act) ])
in
m, si, j, (control map ck action) :: s
| Minils.Evarpat x,
Minils.Earray_op (Minils.Eupdate (idx, e1, e2)) ->
Minils.Earray_op (Minils.Eupdate (idx, e1, e2)) ->
let x = var_from_name map x in
let copy = Assgn (x, translate const_env map (m, si, j, s) e1) in
let idx =
@ -238,25 +240,25 @@ let rec
let action = Assgn (lhs_of_idx_list x idx,
translate const_env map (m, si, j, s) e2)
in
m, si, j, (control map ck copy) :: (control map ck action) :: s
m, si, j, (control map ck copy) :: (control map ck action) :: s
| Minils.Evarpat x,
Minils.Earray_op (Minils.Erepeat (n, e)) ->
| Minils.Evarpat x,
Minils.Earray_op (Minils.Erepeat (n, e)) ->
let cpt = Ident.fresh "i" in
let action =
For (cpt, 0, int_of_size_exp const_env n,
Assgn (Array (var_from_name map x, Lhs (Var cpt)),
translate const_env map (m, si, j, s) e))
in
m, si, j, (control map ck action) :: s
Assgn (Array (var_from_name map x, Lhs (Var cpt)),
translate const_env map (m, si, j, s) e))
in
m, si, j, (control map ck action) :: s
| Minils.Evarpat x,
Minils.Earray_op (Minils.Econcat (e1, e2)) ->
| Minils.Evarpat x,
Minils.Earray_op (Minils.Econcat (e1, e2)) ->
let cpt1 = Ident.fresh "i" in
let cpt2 = Ident.fresh "i" in
let x = var_from_name map x
in
(match e1.Minils.e_ty, e2.Minils.e_ty with
(match e1.Minils.e_ty, e2.Minils.e_ty with
| Types.Tarray (_, n1), Types.Tarray (_, n2) ->
let e1 = translate const_env map (m, si, j, s) e1 in
let e2 = translate const_env map (m, si, j, s) e2 in
@ -264,23 +266,23 @@ let rec
let n2 = int_of_size_exp const_env n2 in
let a1 =
For (cpt1, 0, n1,
Assgn (Array (x, Lhs (Var cpt1)),
Lhs (Array (lhs_of_exp e1, Lhs (Var cpt1))))) in
Assgn (Array (x, Lhs (Var cpt1)),
Lhs (Array (lhs_of_exp e1, Lhs (Var cpt1))))) in
let idx =
Op (op_from_string "+", [ Const (Cint n1); Lhs (Var cpt2) ]) in
let a2 =
For (cpt2, 0, n2,
Assgn (Array (x, idx),
Lhs (Array (lhs_of_exp e2, Lhs (Var cpt2)))))
Assgn (Array (x, idx),
Lhs (Array (lhs_of_exp e2, Lhs (Var cpt2)))))
in
m, si, j,
(control map ck a1) :: (control map ck a2) :: s
m, si, j,
(control map ck a1) :: (control map ck a2) :: s
| _ -> assert false
)
)
| pat, Minils.Earray_op (
Minils.Eiterator (it,
{ Minils.op_name = f; Minils.op_params = params;
Minils.Eiterator (it,
{ Minils.op_name = f; Minils.op_params = params;
Minils.op_kind = k },
n, e_list, reset)) ->
let name_list = translate_pat map pat in
@ -288,9 +290,9 @@ let rec
List.map (translate const_env map (m, si, j, s)) e_list in
let o = gen_symbol () in
let n = int_of_size_exp const_env n in
let si =
(match k with
| Minils.Eop -> si
let si =
(match k with
| Minils.Eop -> si
| Minils.Enode -> (Reinit o) :: si) in
let params = List.map (int_of_size_exp const_env) params in
let j = (o, (encode_longname_params f params), n) :: j in
@ -299,10 +301,10 @@ let rec
translate_iterator const_env map it x name_list o n c_list in
let s =
(match reset with
| None -> (control map ck action) :: s
| Some r ->
(control map (Minils.Con (ck, Name "true", r)) (Reinit o)) ::
(control map ck action) :: s
| None -> (control map ck action) :: s
| Some r ->
(control map (Minils.Con (ck, Name "true", r)) (Reinit o)) ::
(control map ck action) :: s
)
in (m, si, j, s)
@ -312,87 +314,87 @@ let rec
and translate_iterator const_env map it x name_list o n c_list =
match it with
| Minils.Imap ->
let c_list =
List.map (array_elt_of_exp (Var x)) c_list in
let name_list = List.map (fun l -> Array (l, Lhs (Var x))) name_list in
let objn = Array_context (o, Var x) in
| Minils.Imap ->
let c_list =
List.map (array_elt_of_exp (Var x)) c_list in
let name_list = List.map (fun l -> Array (l, Lhs (Var x))) name_list in
let objn = Array_context (o, Var x) in
For (x, 0, n, Step_ap (name_list, objn, c_list))
| Minils.Imapfold ->
let (c_list, acc_in) = split_last c_list in
let c_list = List.map (array_elt_of_exp (Var x)) c_list in
let objn = Array_context (o, Var x) in
let (name_list, acc_out) = split_last name_list in
let name_list = List.map (fun l -> Array (l, Lhs (Var x))) name_list in
| Minils.Imapfold ->
let (c_list, acc_in) = split_last c_list in
let c_list = List.map (array_elt_of_exp (Var x)) c_list in
let objn = Array_context (o, Var x) in
let (name_list, acc_out) = split_last name_list in
let name_list = List.map (fun l -> Array (l, Lhs (Var x))) name_list in
Comp (Assgn (acc_out, acc_in),
For (x, 0, n,
Step_ap (name_list @ [ acc_out ], objn,
c_list @ [ Lhs acc_out ])))
| Minils.Ifold ->
let (c_list, acc_in) = split_last c_list in
let c_list = List.map (array_elt_of_exp (Var x)) c_list in
let objn = Array_context (o, Var x) in
let acc_out = last_element name_list in
| Minils.Ifold ->
let (c_list, acc_in) = split_last c_list in
let c_list = List.map (array_elt_of_exp (Var x)) c_list in
let objn = Array_context (o, Var x) in
let acc_out = last_element name_list in
Comp (Assgn (acc_out, acc_in),
For (x, 0, n,
Step_ap (name_list, objn, c_list @ [ Lhs acc_out ])))
let translate_eq_list const_env map act_list =
List.fold_right (translate_eq const_env map) act_list ([], [], [], [])
let remove m d_list =
List.filter (fun { Minils.v_name = n } -> not (List.mem_assoc n m)) d_list
let var_decl l =
List.map (fun (x, t) -> mk_var_dec x t) l
let obj_decl l = List.map (fun (x, t, i) -> { obj = x; cls = t; size = i; }) l
let translate_var_dec const_env map l =
let one_var { Minils.v_name = x; Minils.v_type = t } =
mk_var_dec x (translate_type const_env t)
in
List.map one_var l
List.map one_var l
let translate_contract const_env map =
function
| None -> ([], [], [], [], [], [])
| Some
{
Minils.c_eq = eq_list;
Minils.c_local = d_list;
Minils.c_controllables = c_list;
Minils.c_assume = e_a;
Minils.c_enforce = e_c
} ->
let (m, si, j, s_list) = translate_eq_list const_env map eq_list in
let d_list = remove m d_list in
let d_list = translate_var_dec const_env map d_list in
let c_list = translate_var_dec const_env map c_list
in (m, si, j, s_list, d_list, c_list)
| None -> ([], [], [], [], [], [])
| Some
{
Minils.c_eq = eq_list;
Minils.c_local = d_list;
Minils.c_controllables = c_list;
Minils.c_assume = e_a;
Minils.c_enforce = e_c
} ->
let (m, si, j, s_list) = translate_eq_list const_env map eq_list in
let d_list = remove m d_list in
let d_list = translate_var_dec const_env map d_list in
let c_list = translate_var_dec const_env map c_list
in (m, si, j, s_list, d_list, c_list)
(** Returns a map, mapping variables names to the variables
where they will be stored. *)
let subst_map inputs outputs locals mems =
(* Create a map that simply maps each var to itself *)
let m =
List.fold_left (fun m { Minils.v_name = x } -> Env.add x (Var x) m)
List.fold_left (fun m { Minils.v_name = x } -> Env.add x (Var x) m)
Env.empty (inputs @ outputs @ locals)
in
List.fold_left (fun m x -> Env.add x (Mem x) m) m mems
in
List.fold_left (fun m x -> Env.add x (Mem x) m) m mems
let translate_node_aux const_env
{
Minils.n_name = f;
Minils.n_input = i_list;
Minils.n_output = o_list;
Minils.n_local = d_list;
Minils.n_equs = eq_list;
Minils.n_contract = contract;
Minils.n_params = params
} =
{
Minils.n_name = f;
Minils.n_input = i_list;
Minils.n_output = o_list;
Minils.n_local = d_list;
Minils.n_equs = eq_list;
Minils.n_contract = contract;
Minils.n_params = params
} =
let mem_vars = List.flatten (List.map Minils.Vars.memory_vars eq_list) in
let subst_map = subst_map i_list o_list d_list mem_vars in
let (m, si, j, s_list) = translate_eq_list const_env subst_map eq_list in
@ -414,57 +416,57 @@ let translate_node_aux const_env
controllables = c_list;
bd = s;
}
in
{ cl_id = f; mem = m; objs = j; reset = si; step = step; }
in
{ cl_id = f; mem = m; objs = j; reset = si; step = step; }
let build_params_list env params_names params_values =
List.fold_left2 (fun env { p_name = n } v -> NamesEnv.add n (SConst v) env)
List.fold_left2 (fun env { p_name = n } v -> NamesEnv.add n (SConst v) env)
env params_names params_values
let translate_node const_env n =
let translate_one p =
let const_env = build_params_list const_env n.Minils.n_params p in
let c = translate_node_aux const_env n
in
{ c with cl_id = encode_name_params c.cl_id p; }
in
{ c with cl_id = encode_name_params c.cl_id p; }
in
match n.Minils.n_params_instances with
match n.Minils.n_params_instances with
| [] -> [ translate_node_aux const_env n ]
| params_lists -> List.map translate_one params_lists
let translate_ty_def const_env { Minils.t_name = name; Minils.t_desc = tdesc
} =
} =
let tdesc =
match tdesc with
| Minils.Type_abs -> Type_abs
| Minils.Type_enum tag_name_list -> Type_enum tag_name_list
| Minils.Type_struct field_ty_list ->
Type_struct
(List.map
(fun { f_name = f; f_type = ty } ->
(f, translate_type const_env ty))
field_ty_list)
| Minils.Type_abs -> Type_abs
| Minils.Type_enum tag_name_list -> Type_enum tag_name_list
| Minils.Type_struct field_ty_list ->
Type_struct
(List.map
(fun { f_name = f; f_type = ty } ->
(f, translate_type const_env ty))
field_ty_list)
in { t_name = name; t_desc = tdesc; }
let build_const_env cd_list =
List.fold_left
(fun env cd -> NamesEnv.add cd.Minils.c_name cd.Minils.c_value env)
NamesEnv.empty cd_list
let program {
Minils.p_pragmas = p_pragmas_list;
Minils.p_opened = p_module_list;
Minils.p_types = p_type_list;
Minils.p_nodes = p_node_list;
Minils.p_consts = p_const_list
} =
Minils.p_pragmas = p_pragmas_list;
Minils.p_opened = p_module_list;
Minils.p_types = p_type_list;
Minils.p_nodes = p_node_list;
Minils.p_consts = p_const_list
} =
let const_env = build_const_env p_const_list
in
{
o_pragmas = p_pragmas_list;
o_opened = p_module_list;
o_types = List.map (translate_ty_def const_env) p_type_list;
o_defs = List.flatten (List.map (translate_node const_env) p_node_list);
}
{
o_pragmas = p_pragmas_list;
o_opened = p_module_list;
o_types = List.map (translate_ty_def const_env) p_type_list;
o_defs = List.flatten (List.map (translate_node const_env) p_node_list);
}

148
compiler/minils/sequential/obc.ml
View file

@ -33,15 +33,15 @@ type type_dec =
t_desc : tdesc }
and tdesc =
| Type_abs
| Type_enum of name list
| Type_struct of (name * ty) list
| Type_abs
| Type_enum of name list
| Type_struct of (name * ty) list
type const =
| Cint of int
| Cfloat of float
| Cconstr of longname
| Carray of int * const
| Cint of int
| Cfloat of float
| Cconstr of longname
| Carray of int * const
type lhs =
| Var of var_name
@ -56,7 +56,7 @@ and exp =
| Struct_lit of type_name * (field_name * exp) list
| Array_lit of exp list
type obj_call =
type obj_call =
| Context of obj_name
| Array_context of obj_name * lhs
@ -75,7 +75,7 @@ type var_dec =
type obj_dec =
{ obj : obj_name;
cls : instance_name;
cls : instance_name;
size : int; }
type step_fun =
@ -83,8 +83,8 @@ type step_fun =
out : var_dec list;
local : var_dec list;
controllables : var_dec list; (* GD : ugly patch to delay controllable
variables definition to target code
generation *)
variables definition to target code
generation *)
bd : act }
type reset_fun = act
@ -109,9 +109,9 @@ let mk_var_dec name ty =
to this variable declaration is scalar (ie a type that can
be returned by a C function). *)
let is_scalar_type vd =
match vd.v_type with
| Tint | Tfloat | Tbool -> true
| _ -> false
match vd.v_type with
| Tint | Tfloat | Tbool -> true
| _ -> false
let rec var_name x =
match x with
@ -120,7 +120,7 @@ let rec var_name x =
| Field(x,_) -> var_name x
| Array(l, _) -> var_name l
(** Returns whether an object of name n belongs to
(** Returns whether an object of name n belongs to
a list of var_dec. *)
let rec vd_mem n = function
| [] -> false
@ -130,7 +130,7 @@ let rec vd_mem n = function
in a list of var_dec. *)
let rec vd_find n = function
| [] -> Format.printf "Not found var %s\n" (name n); raise Not_found
| vd::l ->
| vd::l ->
if vd.v_name = n then vd else vd_find n l
let lhs_of_exp = function
@ -147,9 +147,9 @@ struct
| Tfloat -> fprintf ff "float"
| Tbool -> fprintf ff "bool"
| Tid(id) -> print_longname ff id
| Tarray(ty, n) ->
print_type ff ty;
fprintf ff "^%d" n
| Tarray(ty, n) ->
print_type ff ty;
fprintf ff "^%d" n
let print_vd ff vd =
fprintf ff "@[<v>";
@ -170,19 +170,19 @@ struct
| Cfloat f -> fprintf ff "%f" f
| Cconstr(tag) -> print_longname ff tag
| Carray(n,c) ->
print_c ff c;
fprintf ff "^%d" n
print_c ff c;
fprintf ff "^%d" n
let rec print_lhs ff e =
let rec print_lhs ff e =
match e with
| Var x -> print_ident ff x
| Mem x -> fprintf ff "mem("; print_ident ff x; fprintf ff ")"
| Field (l, f) -> print_lhs ff l; fprintf ff ".%s" (shortname f)
| Array(x, idx) ->
print_lhs ff x;
fprintf ff "[";
print_exp ff idx;
fprintf ff "]"
| Var x -> print_ident ff x
| Mem x -> fprintf ff "mem("; print_ident ff x; fprintf ff ")"
| Field (l, f) -> print_lhs ff l; fprintf ff ".%s" (shortname f)
| Array(x, idx) ->
print_lhs ff x;
fprintf ff "[";
print_exp ff idx;
fprintf ff "]"
and print_exps ff e_list = print_list_r print_exp "" "," "" ff e_list
@ -191,14 +191,14 @@ struct
| Const c -> print_c ff c
| Op(op, e_list) -> print_op ff op e_list
| Struct_lit(_,f_e_list) ->
fprintf ff "@[<v 1>";
print_list_r
(fun ff (field, e) -> print_longname ff field;fprintf ff " = ";
print_exp ff e)
"{" ";" "}" ff f_e_list;
fprintf ff "@]"
fprintf ff "@[<v 1>";
print_list_r
(fun ff (field, e) -> print_longname ff field;fprintf ff " = ";
print_exp ff e)
"{" ";" "}" ff f_e_list;
fprintf ff "@]"
| Array_lit e_list ->
fprintf ff "@[";
fprintf ff "@[";
print_list_r print_exp "[" ";" "]" ff e_list;
fprintf ff "@]"
@ -214,45 +214,45 @@ struct
let print_obj_call ff = function
| Context o -> print_name ff o
| Array_context (o, i) ->
fprintf ff "%a[%a]"
print_name o
print_lhs i
fprintf ff "%a[%a]"
print_name o
print_lhs i
let rec print_act ff a =
match a with
| Assgn (x, e) -> print_asgn ff "" x e
| Comp (a1, a2) ->
fprintf ff "@[<v>";
print_act ff a1;
fprintf ff ";@,";
print_act ff a2;
fprintf ff "@]"
fprintf ff "@[<v>";
print_act ff a1;
fprintf ff ";@,";
print_act ff a2;
fprintf ff "@]"
| Case(e, tag_act_list) ->
fprintf ff "@[<v>@[<v 2>switch (";
print_exp ff e; fprintf ff ") {@,";
print_tag_act_list ff tag_act_list;
fprintf ff "@]@,}@]"
fprintf ff "@[<v>@[<v 2>switch (";
print_exp ff e; fprintf ff ") {@,";
print_tag_act_list ff tag_act_list;
fprintf ff "@]@,}@]"
| For(x, i1, i2, act) ->
fprintf ff "@[<v>@[<v 2>for %s=%d to %d : {@, %a @]@,}@]"
(name x) i1 i2
print_act act
fprintf ff "@[<v>@[<v 2>for %s=%d to %d : {@, %a @]@,}@]"
(name x) i1 i2
print_act act
| Step_ap (var_list, o, es) ->
print_list print_lhs "(" "," ")" ff var_list;
fprintf ff " = "; print_obj_call ff o; fprintf ff ".step(";
fprintf ff "@["; print_exps ff es; fprintf ff "@]";
fprintf ff ")"
print_list print_lhs "(" "," ")" ff var_list;
fprintf ff " = "; print_obj_call ff o; fprintf ff ".step(";
fprintf ff "@["; print_exps ff es; fprintf ff "@]";
fprintf ff ")"
| Reinit o ->
print_name ff o; fprintf ff ".reset()"
print_name ff o; fprintf ff ".reset()"
| Nothing -> fprintf ff "()"
and print_tag_act_list ff tag_act_list =
print_list
(fun ff (tag, a) ->
fprintf ff "@[<hov 2>case@ ";
print_longname ff tag;
fprintf ff ":@ ";
print_act ff a;
fprintf ff "@]") "" "" "" ff tag_act_list
fprintf ff "@[<hov 2>case@ ";
print_longname ff tag;
fprintf ff ":@ ";
print_act ff a;
fprintf ff "@]") "" "" "" ff tag_act_list
let print_step ff { inp = inp; out = out; local = nl; bd = bd } =
fprintf ff "@[<v 2>";
@ -297,18 +297,18 @@ struct
match tdesc with
| Type_abs -> fprintf ff "@[type %s@\n@]" name
| Type_enum(tag_name_list) ->
fprintf ff "@[type %s = " name;
print_list_r print_name "" "|" "" ff tag_name_list;
fprintf ff "@\n@]"
fprintf ff "@[type %s = " name;
print_list_r print_name "" "|" "" ff tag_name_list;
fprintf ff "@\n@]"
| Type_struct(f_ty_list) ->
fprintf ff "@[type %s = " name;
fprintf ff "@[<v 1>";
print_list
(fun ff (field, ty) ->
print_name ff field;
fprintf ff ": ";
print_type ff ty) "{" ";" "}" ff f_ty_list;
fprintf ff "@]@.@]"
fprintf ff "@[type %s = " name;
fprintf ff "@[<v 1>";
print_list
(fun ff (field, ty) ->
print_name ff field;
fprintf ff ": ";
print_type ff ty) "{" ";" "}" ff f_ty_list;
fprintf ff "@]@.@]"
let print_open_module ff name =
fprintf ff "@[open ";
@ -323,6 +323,6 @@ struct
let print oc p =
let ff = formatter_of_out_channel oc in
fprintf ff "@[-- Code generated by the MiniLucid Compiler@.";
fprintf ff "@[<v>"; print_prog ff p; fprintf ff "@]@]@."
fprintf ff "@[<v>"; print_prog ff p; fprintf ff "@]@]@."
end

107
compiler/minils/transformations/callgraph.ml
View file

@ -17,97 +17,98 @@ let rec string_of_int_list = function
| n::l -> (string_of_int n)^", "^(string_of_int_list l)
let add_node_params n params =
if NamesEnv.mem n !nodes_instances then
nodes_instances := NamesEnv.add n
if NamesEnv.mem n !nodes_instances then
nodes_instances := NamesEnv.add n
(params::(NamesEnv.find n !nodes_instances)) !nodes_instances
else
nodes_instances := NamesEnv.add n [params] !nodes_instances
let rec node_by_name s = function
| [] -> raise Not_found
| n::l ->
| n::l ->
if n.n_name = s then
n
n
else
node_by_name s l
node_by_name s l
let build env params_names params_values =
List.fold_left2 (fun m { p_name = n } v -> NamesEnv.add n (SConst v) m)
let build env params_names params_values =
List.fold_left2 (fun m { p_name = n } v -> NamesEnv.add n (SConst v) m)
env params_names params_values
let rec collect_exp nodes env e =
match e.e_desc with
| Emerge(_, c_e_list) ->
List.iter (fun (_, e) -> collect_exp nodes env e) c_e_list
List.iter (fun (_, e) -> collect_exp nodes env e) c_e_list
| Eifthenelse(e1, e2, e3) ->
collect_exp nodes env e1;
collect_exp nodes env e2;
collect_exp nodes env e3
collect_exp nodes env e1;
collect_exp nodes env e2;
collect_exp nodes env e3
| Ewhen(e, _, _) | Efby(_, e) | Efield(e, _) ->
collect_exp nodes env e
collect_exp nodes env e
| Evar _ | Econstvar _ | Econst _ -> ()
| Estruct(f_e_list) ->
List.iter (fun (_, e) -> collect_exp nodes env e) f_e_list
List.iter (fun (_, e) -> collect_exp nodes env e) f_e_list
| Etuple e_list | Earray e_list ->
List.iter (collect_exp nodes env) e_list
| Efield_update(_, e1, e2) ->
collect_exp nodes env e1;
collect_exp nodes env e2
(* Do the real work: call node *)
| Ecall( { op_name = ln; op_params = params; op_kind = Eop }, e_list, _) ->
List.iter (collect_exp nodes env) e_list
| Ecall( { op_name = ln; op_params = params; op_kind = Enode }, e_list, _) ->
List.iter (collect_exp nodes env) e_list;
let params = List.map (int_of_size_exp env) params in
call_node_instance nodes ln params
| Efield_update(_, e1, e2) ->
collect_exp nodes env e1;
collect_exp nodes env e2
(* Do the real work: call node *)
| Ecall( { op_name = ln; op_params = params; op_kind = Eop }, e_list, _) ->
List.iter (collect_exp nodes env) e_list
| Ecall( { op_name = ln; op_params = params; op_kind = Enode },
e_list, _) ->
List.iter (collect_exp nodes env) e_list;
let params = List.map (int_of_size_exp env) params in
call_node_instance nodes ln params
| Earray_op op ->
collect_array_exp nodes env op
and collect_array_exp nodes env = function
| Eselect_dyn (e_list, _, e1, e2) ->
List.iter (collect_exp nodes env) e_list;
collect_exp nodes env e1;
collect_exp nodes env e2
| Eselect_dyn (e_list, _, e1, e2) ->
List.iter (collect_exp nodes env) e_list;
collect_exp nodes env e1;
collect_exp nodes env e2
| Eupdate (_, e1, e2) | Econcat (e1, e2) ->
collect_exp nodes env e1;
collect_exp nodes env e2
collect_exp nodes env e1;
collect_exp nodes env e2
| Eselect (_,e) | Eselect_slice (_ , _, e) | Erepeat (_,e) ->
collect_exp nodes env e
collect_exp nodes env e
| Eiterator (_, { op_name = ln; op_params = params }, _, e_list, _) ->
List.iter (collect_exp nodes env) e_list;
let params = List.map (int_of_size_exp env) params in
call_node_instance nodes ln params
and collect_eqs nodes env eq =
List.iter (collect_exp nodes env) e_list;
let params = List.map (int_of_size_exp env) params in
call_node_instance nodes ln params
and collect_eqs nodes env eq =
collect_exp nodes env eq.eq_rhs
and call_node_instance nodes ln params =
match params with
| [] -> ()
| params ->
let n = node_by_name (shortname ln) nodes in
node_call nodes n params
match params with
| [] -> ()
| params ->
let n = node_by_name (shortname ln) nodes in
node_call nodes n params
and node_call nodes n params =
match params with
| [] ->
List.iter (collect_eqs nodes !global_env) n.n_equs
| [] ->
List.iter (collect_eqs nodes !global_env) n.n_equs
| params ->
add_node_params n.n_name params;
let env = build !global_env n.n_params params in
List.iter (collect_eqs nodes env) n.n_equs
add_node_params n.n_name params;
let env = build !global_env n.n_params params in
List.iter (collect_eqs nodes env) n.n_equs
let node n =
let inst =
if NamesEnv.mem n.n_name !nodes_instances then
let inst =
if NamesEnv.mem n.n_name !nodes_instances then
NamesEnv.find n.n_name !nodes_instances
else
[] in
{ n with n_params_instances = inst }
{ n with n_params_instances = inst }
let build_const_env cd_list =
List.fold_left (fun env cd -> NamesEnv.add
cd.Minils.c_name cd.Minils.c_value env)
List.fold_left (fun env cd -> NamesEnv.add
cd.Minils.c_name cd.Minils.c_value env)
NamesEnv.empty cd_list
let program p =
@ -116,7 +117,7 @@ let program p =
| [] -> node_call p.p_nodes n []
| _ -> ()
in
global_env := build_const_env p.p_consts;
List.iter try_call_node p.p_nodes;
{ p with p_nodes = List.map node p.p_nodes }
global_env := build_const_env p.p_consts;
List.iter try_call_node p.p_nodes;
{ p with p_nodes = List.map node p.p_nodes }

94
compiler/minils/transformations/normalize.ml
View file

@ -21,7 +21,7 @@ let equation (d_list, eq_list) ({ e_ty = te; e_ck = ck } as e) =
let n = Ident.fresh "_v" in
let d_list = (mk_var_dec ~clock:ck n te) :: d_list in
let eq_list = (mk_equation (Evarpat n) e) :: eq_list in
(d_list, eq_list), n
(d_list, eq_list), n
let intro context e =
match e.e_desc with
@ -41,8 +41,8 @@ let rec whenc context e c n =
(context, e :: e_list))
e_list (context, []) in
context, { e with e_desc = Etuple(e_list); e_ck = Con(e.e_ck, c, n) }
(* | Emerge _ -> let context, x = equation context e in
context, when_on_c c n { e with e_desc = Evar(x) } *)
(* | Emerge _ -> let context, x = equation context e in
context, when_on_c c n { e with e_desc = Evar(x) } *)
| _ -> context, when_on_c c n e
(* transforms [merge x (c1, (e11,...,e1n));...;(ck, (ek1,...,ekn))] into *)
@ -91,7 +91,7 @@ let const e c =
| Con(ck_on, tag, x) ->
Ewhen({ e with e_desc = const ck_on; e_ck = ck_on }, tag, x)
| Cvar { contents = Clink ck } -> const ck in
const e.e_ck
const e.e_ck
(* normal form for expressions and equations: *)
(* - e ::= op(e,...,e) | x | C | e when C(x) *)
@ -132,28 +132,29 @@ let rec translate kind context e =
let context, act = translate merge_kind context e in
context, ((tag, act) :: ta_list))
tag_e_list (context, []) in
context, merge e n ta_list
context, merge e n ta_list
| Eifthenelse(e1, e2, e3) ->
let context, e1 = translate Any context e1 in
let context, e2 = translate Act context e2 in
let context, e3 = translate Act context e3 in
ifthenelse context e1 e2 e3
ifthenelse context e1 e2 e3
| Etuple(e_list) ->
let context, e_list = translate_list kind context e_list in
context, { e with e_desc = Etuple(e_list) }
context, { e with e_desc = Etuple(e_list) }
| Ewhen(e1, c, n) ->
let context, e1 = translate kind context e1 in
whenc context e1 c n
whenc context e1 c n
| Ecall(op_desc, e_list, r) ->
let context, e_list = translate_list function_args_kind context e_list in
context, { e with e_desc = Ecall(op_desc, e_list, r) }
let context, e_list =
translate_list function_args_kind context e_list in
context, { e with e_desc = Ecall(op_desc, e_list, r) }
| Efby(v, e1) ->
let context, e1 = translate Exp context e1 in
let context, e1' =
if constant e1 then context, e1
else let context, n = equation context e1 in
context, { e1 with e_desc = Evar(n) } in
context, { e with e_desc = Efby(v, e1') }
if constant e1 then context, e1
else let context, n = equation context e1 in
context, { e1 with e_desc = Evar(n) } in
context, { e with e_desc = Efby(v, e1') }
| Evar _ -> context, e
| Econst(c) -> context, { e with e_desc = const e (Econst c) }
| Econstvar x -> context, { e with e_desc = const e (Econstvar x) }
@ -169,45 +170,46 @@ let rec translate kind context e =
l (context, []) in
context, { e with e_desc = Estruct l }
| Efield_update (f, e1, e2) ->
let context, e1 = translate VRef context e1 in
let context, e2 = translate Exp context e2 in
context, { e with e_desc = Efield_update(f, e1, e2) }
| Earray(e_list) ->
let context, e_list = translate_list kind context e_list in
context, { e with e_desc = Earray(e_list) }
| Earray_op op ->
let context, e1 = translate VRef context e1 in
let context, e2 = translate Exp context e2 in
context, { e with e_desc = Efield_update(f, e1, e2) }
| Earray(e_list) ->
let context, e_list = translate_list kind context e_list in
context, { e with e_desc = Earray(e_list) }
| Earray_op op ->
let context, op = translate_array_exp kind context op in
context, { e with e_desc = Earray_op op }
context, { e with e_desc = Earray_op op }
in add context kind e
and translate_array_exp kind context op =
match op with
| Erepeat (n,e') ->
let context, e' = translate VRef context e' in
context, Erepeat(n, e')
| Eselect (idx,e') ->
let context, e' = translate VRef context e' in
context, Eselect(idx, e')
let context, e' = translate VRef context e' in
context, Erepeat(n, e')
| Eselect (idx,e') ->
let context, e' = translate VRef context e' in
context, Eselect(idx, e')
| Eselect_dyn (idx, bounds, e1, e2) ->
let context, e1 = translate VRef context e1 in
let context, idx = translate_list Exp context idx in
let context, e2 = translate Exp context e2 in
context, Eselect_dyn(idx, bounds, e1, e2)
let context, e1 = translate VRef context e1 in
let context, idx = translate_list Exp context idx in
let context, e2 = translate Exp context e2 in
context, Eselect_dyn(idx, bounds, e1, e2)
| Eupdate (idx, e1, e2) ->
let context, e1 = translate VRef context e1 in
let context, e2 = translate Exp context e2 in
context, Eupdate(idx, e1, e2)
let context, e1 = translate VRef context e1 in
let context, e2 = translate Exp context e2 in
context, Eupdate(idx, e1, e2)
| Eselect_slice (idx1, idx2, e') ->
let context, e' = translate VRef context e' in
context, Eselect_slice(idx1, idx2, e')
| Econcat (e1, e2) ->
let context, e1 = translate VRef context e1 in
let context, e2 = translate VRef context e2 in
context, Econcat(e1, e2)
let context, e' = translate VRef context e' in
context, Eselect_slice(idx1, idx2, e')
| Econcat (e1, e2) ->
let context, e1 = translate VRef context e1 in
let context, e2 = translate VRef context e2 in
context, Econcat(e1, e2)
| Eiterator (it, op_desc, n, e_list, reset) ->
let context, e_list = translate_list function_args_kind context e_list in
context, Eiterator(it, op_desc, n, e_list, reset)
let context, e_list =
translate_list function_args_kind context e_list in
context, Eiterator(it, op_desc, n, e_list, reset)
and translate_list kind context e_list =
match e_list with
[] -> context, []
@ -220,7 +222,7 @@ let rec translate_eq context eq =
(* applies distribution rules *)
(* [x = v fby e] should verifies that x is local *)
(* [(p1,...,pn) = (e1,...,en)] into [p1 = e1;...;pn = en] *)
let rec distribute ((d_list, eq_list) as context)
let rec distribute ((d_list, eq_list) as context)
({ eq_lhs = pat; eq_rhs = e } as eq) =
match pat, e.e_desc with
| Evarpat(x), Efby _ when not (vd_mem x d_list) ->
@ -229,11 +231,11 @@ let rec translate_eq context eq =
{ eq with eq_rhs = { e with e_desc = Evar n } } :: eq_list
| Etuplepat(pat_list), Etuple(e_list) ->
let eqs = List.map2 mk_equation pat_list e_list in
List.fold_left distribute context eqs
List.fold_left distribute context eqs
| _ -> d_list, eq :: eq_list in
let context, e = translate Any context eq.eq_rhs in
distribute context { eq with eq_rhs = e }
distribute context { eq with eq_rhs = e }
let translate_eq_list d_list eq_list =
List.fold_left

31
compiler/minils/transformations/schedule.ml
View file

@ -40,45 +40,44 @@ let n1_list = head e1 in
let n2_list = head e2 in
*)
(* clever scheduling *)
let schedule eq_list =
let rec recook = function
| [] -> []
| node :: node_list -> node >> (recook node_list)
and (>>) node node_list =
try
insert node node_list
with
Not_found -> node :: node_list
Not_found -> node :: node_list
and insert node = function
| [] -> raise Not_found
| node1 :: node_list ->
if linked node node1 then raise Not_found
else
try
node1 :: (insert node node_list)
with
| Not_found ->
if join (containt node) (containt node1)
then node :: node1 :: node_list
else raise Not_found in
if linked node node1 then raise Not_found
else
try
node1 :: (insert node node_list)
with
| Not_found ->
if join (containt node) (containt node1)
then node :: node1 :: node_list
else raise Not_found in
let node_list, _ = DataFlowDep.build eq_list in
let node_list = recook (topological node_list) in
let node_list = List.rev node_list in
let node_list = recook node_list in
let node_list = List.rev node_list in
List.map containt node_list
List.map containt node_list
let schedule_contract ({ c_eq = eqs } as c) =
let eqs = schedule eqs in
{ c with c_eq = eqs }
let node ({ n_contract = contract; n_equs = eq_list } as node) =
let contract = optional schedule_contract contract in
let contract = optional schedule_contract contract in
let eq_list = schedule eq_list in
{ node with n_equs = eq_list; n_contract = contract }

20
compiler/preproc.ml
View file

@ -12,8 +12,8 @@ open Unix
(** [date] is a string denoting the current date. *)
let date =
let days = [| "sunday"; "monday"; "tuesday"; "wednesday"; "thursday"; "friday";
"saturday" |]
let days = [| "sunday"; "monday"; "tuesday"; "wednesday"; "thursday";
"friday"; "saturday" |]
and months = [| "january"; "february"; "march"; "april"; "may"; "june";
"july"; "august"; "september"; "october"; "november";
"december" |] in
@ -43,14 +43,14 @@ let env = [("DATE", date); ("STDLIB", stdlib)]
in [subst] and replaces them according to the couple found in the
environment defined above. *)
let filter =
object
inherit Ast.map as super
method expr e = match e with
| <:expr< $str:s$ >> when List.mem_assoc s env ->
let repl = try Sys.getenv s with Not_found -> List.assoc s env in
<:expr@here< $str:repl$ >>
| x -> x
end;;
object
inherit Ast.map as super
method expr e = match e with
| <:expr< $str:s$ >> when List.mem_assoc s env ->
let repl = try Sys.getenv s with Not_found -> List.assoc s env in
<:expr@here< $str:repl$ >>
| x -> x
end;;
(** Tell Camlp4 about it. *)
AstFilters.register_str_item_filter filter#str_item

11
compiler/utilities/global/compiler_utils.ml
View file

@ -22,7 +22,7 @@ let language_error lang =
let comment s =
if !verbose then Printf.printf "** %s done **\n" s; flush stdout
let do_pass f d p pp enabled =
if enabled
@ -58,9 +58,9 @@ let clean_dir dir =
dir
let init_compiler modname source_name ic =
Location.initialize source_name ic;
Modules.initialize modname;
Initial.initialize ()
Location.initialize source_name ic;
Modules.initialize modname;
Initial.initialize ()
let doc_verbose = "\t\t\tSet verbose mode"
and doc_version = "\t\tThe version of the compiler"
@ -75,7 +75,8 @@ and doc_target =
^ " java or z3z)"
and doc_full_type_info = "\t\t\tPrint full type information"
and doc_target_path =
"<path>\tGenerated files will be placed in <path>\n\t\t\t(the directory is cleaned)"
"<path>\tGenerated files will be placed in <path>\n\t\t\t(the directory is"
^ " cleaned)"
and doc_noinit = "\t\tDisable initialization analysis"
let errmsg = "Options are:"

49
compiler/utilities/global/dep.ml
View file

@ -25,13 +25,13 @@ struct
(* associate a graph node for each name declaration *)
let rec nametograph g var_list is_antidep n_to_graph =
let add_node env x =
if Env.mem x env then
let l = Env.find x env in
Env.add x ((g, is_antidep)::l) env
else
Env.add x [(g, is_antidep)] env
if Env.mem x env then
let l = Env.find x env in
Env.add x ((g, is_antidep)::l) env
else
Env.add x [(g, is_antidep)] env
in
List.fold_left add_node n_to_graph var_list in
List.fold_left add_node n_to_graph var_list in
let rec nametograph_env g var_list node_env =
List.fold_left (fun env x -> Env.add x g env) node_env var_list in
@ -42,35 +42,36 @@ struct
| eq :: eqs ->
let g = make eq in
let node_env = nametograph_env g (Read.def [] eq) node_env in
let n_to_graph = nametograph g (Read.def [] eq)
let n_to_graph = nametograph g (Read.def [] eq)
(Read.antidep eq) n_to_graph in
init_graph eqs (g :: g_list) n_to_graph node_env
init_graph eqs (g :: g_list) n_to_graph node_env
in
let rec make_graph g_list names_to_graph =
let attach_one node (g, is_antidep) =
if is_antidep then
add_depends g node
else
add_depends node g
if is_antidep then
add_depends g node
else
add_depends node g
in
let attach node n =
try
let l = Env.find n names_to_graph in
List.iter (attach_one node) l
List.iter (attach_one node) l
with
| Not_found -> () in
match g_list with
| [] -> ()
| node :: g_list ->
let names = Read.read (containt node) in
List.iter (attach node) names;
make_graph g_list names_to_graph in
let g_list, names_to_graph, node_env = init_graph eqs [] Env.empty Env.empty in
make_graph g_list names_to_graph;
g_list, node_env
match g_list with
| [] -> ()
| node :: g_list ->
let names = Read.read (containt node) in
List.iter (attach node) names;
make_graph g_list names_to_graph in
let g_list, names_to_graph, node_env =
init_graph eqs [] Env.empty Env.empty in
make_graph g_list names_to_graph;
g_list, node_env
end

39
compiler/utilities/graph.ml
View file

@ -9,8 +9,8 @@
(* graph manipulation *)
(* $Id$ *)
type 'a graph =
{ g_top: 'a node list;
g_bot: 'a node list }
{ g_top: 'a node list;
g_bot: 'a node list }
and 'a node =
{ g_containt: 'a;
@ -38,9 +38,12 @@ let add_depends node1 node2 =
)
let remove_depends node1 node2 =
if not (node1.g_tag = node2.g_tag) then (
node1.g_depends_on <- List.filter (fun n -> n.g_tag <> node2.g_tag) node1.g_depends_on;
node2.g_depends_by <- List.filter (fun n -> n.g_tag <> node1.g_tag) node2.g_depends_by
if not (node1.g_tag = node2.g_tag)
then (
node1.g_depends_on <-
List.filter (fun n -> n.g_tag <> node2.g_tag) node1.g_depends_on;
node2.g_depends_by <-
List.filter (fun n -> n.g_tag <> node1.g_tag) node2.g_depends_by
)
let graph top_list bot_list = { g_top = top_list; g_bot = bot_list }
@ -49,15 +52,15 @@ let graph top_list bot_list = { g_top = top_list; g_bot = bot_list }
let topological g_list =
let rec sortrec g_list seq =
match g_list with
| [] -> seq
| g :: g_list ->
if g.g_visited then sortrec g_list seq
else
begin
g.g_visited <- true;
let seq = sortrec g.g_depends_on seq in
sortrec g_list (g :: seq)
end in
| [] -> seq
| g :: g_list ->
if g.g_visited then sortrec g_list seq
else
begin
g.g_visited <- true;
let seq = sortrec g.g_depends_on seq in
sortrec g_list (g :: seq)
end in
let seq = sortrec g_list [] in
List.iter
(fun ({ g_visited = _ } as node) -> node.g_visited <- false) g_list;
@ -104,8 +107,8 @@ let cycle g_list =
| Cycle(index) -> Some(flush index)
(** [accessible useful_nodes g_list] returns the list of
accessible nodes starting from useful_nodes and belonging to
g_list. *)
accessible nodes starting from useful_nodes and belonging to
g_list. *)
let accessible useful_nodes g_list =
let rec follow g =
if not g.g_visited then
@ -119,8 +122,8 @@ let accessible useful_nodes g_list =
List.fold_left read [] g_list
(** [exists_path nodes n1 n2] returns whether there is a path
from n1 to n2 in the graph. nodes is the list of all the nodes
in the graph. *)
from n1 to n2 in the graph. nodes is the list of all the nodes
in the graph. *)
let exists_path nodes n1 n2 =
List.mem n2 (accessible [n1] nodes)

18
compiler/utilities/misc.ml
View file

@ -34,7 +34,7 @@ let locate_stdlib () =
let stdlib = try
Sys.getenv "HEPTLIB"
with
Not_found -> standard_lib in
Not_found -> standard_lib in
Printf.printf "Standard library in %s\n" stdlib
let show_version () =
@ -141,13 +141,13 @@ let unique l =
Hashtbl.fold (fun key data accu -> key :: accu) tbl []
let rec incomplete_map f l =
match l with
match l with
| [] -> []
| [a] -> [a]
| a::l -> (f a)::(incomplete_map f l)
let rec last_element l =
match l with
match l with
| [] -> assert false
| [v] -> v
| v::l -> last_element l
@ -157,9 +157,9 @@ let rec last_element l =
let rec split_last = function
| [] -> assert false
| [a] -> [], a
| v::l ->
| v::l ->
let l, a = split_last l in
v::l, a
v::l, a
let remove x l =
List.filter (fun y -> x <> y) l
@ -174,7 +174,7 @@ let repeat_list v n =
| 0 -> []
| n -> v::(aux (n-1))
in
aux n
aux n
(** Same as List.mem_assoc but using the value instead of the key. *)
let rec memd_assoc value = function
@ -184,8 +184,8 @@ let rec memd_assoc value = function
(** Same as List.assoc but searching for a data and returning the key. *)
let rec assocd value = function
| [] -> raise Not_found
| (k,d)::l ->
| (k,d)::l ->
if d = value then
k
k
else
assocd value l
assocd value l

6
compiler/utilities/misc.mli
View file

@ -126,11 +126,11 @@ val unique : 'a list -> 'a list
val incomplete_map : ('a -> 'a) -> 'a list -> 'a list
(** [last_element l] returns the last element of the list l.*)
val last_element : 'a list -> 'a
val last_element : 'a list -> 'a
(** [split_last l] returns the list l without its last element
(** [split_last l] returns the list l without its last element
and the last element of the list .*)
val split_last : 'a list -> ('a list * 'a)
val split_last : 'a list -> ('a list * 'a)
(** [remove x l] removes all occurrences of x from list l.*)
val remove : 'a -> 'a list -> 'a list

63
compiler/utilities/pp_tools.ml
View file

@ -13,9 +13,9 @@ open Format
let rec print_list print lp sep rp ff = function
| [] -> ()
| x::l ->
fprintf ff "%s%a" lp print x;
List.iter (fprintf ff "%s@,%a" sep print) l;
fprintf ff "%s" rp
fprintf ff "%s%a" lp print x;
List.iter (fprintf ff "%s@,%a" sep print) l;
fprintf ff "%s" rp
let rec print_list_r print lp sep rp ff = function
@ -23,7 +23,7 @@ let rec print_list_r print lp sep rp ff = function
| x :: l ->
fprintf ff "%s%a" lp print x;
List.iter (fprintf ff "%s@ %a" sep print) l;
fprintf ff "%s" rp
fprintf ff "%s" rp
let rec print_list_l print lp sep rp ff = function
@ -31,11 +31,11 @@ let rec print_list_l print lp sep rp ff = function
| x :: l ->
fprintf ff "%s%a" lp print x;
List.iter (fprintf ff "@ %s%a" sep print) l;
fprintf ff "%s" rp
fprintf ff "%s" rp
let print_couple print1 print2 lp sep rp ff (c1, c2) =
fprintf ff "%s%a%s@,%a%s" lp print1 c1 sep print2 c2 rp
fprintf ff "%s%a%s@,%a%s" lp print1 c1 sep print2 c2 rp
let print_opt print ff = function
@ -58,32 +58,33 @@ let print_type_params ff pl =
(* Map and Set redefinition to allow pretty printing
module type P = sig
type t
val fprint : Format.formatter -> t -> unit
end
module type P = sig
type t
val fprint : Format.formatter -> t -> unit
end
module type ELT = sig
type t
val compare : t -> t -> int
val fprint : Format.formatter -> t -> unit
end
module type ELT = sig
type t
val compare : t -> t -> int
val fprint : Format.formatter -> t -> unit
end
module SetMake (Elt : ELT) = struct
module M = Set.Make(Elt)
include M
let fprint ff es =
Format.fprintf ff "@[<hov>{@ ";
iter (fun e -> Format.fprintf ff "%a@ " Elt.fprint e) es;
Format.fprintf ff "}@]";
end
module SetMake (Elt : ELT) = struct
module M = Set.Make(Elt)
include M
let fprint ff es =
Format.fprintf ff "@[<hov>{@ ";
iter (fun e -> Format.fprintf ff "%a@ " Elt.fprint e) es;
Format.fprintf ff "}@]";
end
module MapMake (Key : ELT) (Elt : P) = struct
module M = Map.Make(Key)
include M
let fprint prp eem =
Format.fprintf prp "[@[<hv 2>";
iter (fun k m -> Format.fprintf prp "@ | %a -> %a" Key.fprint k Elt.fprint m) eem;
Format.fprintf prp "@]@ ]";
end
module MapMake (Key : ELT) (Elt : P) = struct
module M = Map.Make(Key)
include M
let fprint prp eem =
Format.fprintf prp "[@[<hv 2>";
iter (fun k m ->
Format.fprintf prp "@ | %a -> %a" Key.fprint k Elt.fprint m) eem;
Format.fprintf prp "@]@ ]";
end
*)

18
compiler/utilities/pp_tools.mli
View file

@ -11,7 +11,7 @@
(** {2 list couple and option generic functions} *)
(** Most of theses functions export breaks or breaking spaces
to the calling printer. *)
(** Print the list [x1...xn] as [lp x1 sep \@, x2 ... sep \@, xn rp]
and nothing if the list is empty,
no space is added, but a break right after every [sep]. *)
@ -25,30 +25,30 @@ val print_list :
val print_list_r :
(Format.formatter -> 'a -> unit) ->
string -> string -> string -> Format.formatter -> 'a list -> unit
(** Print the list [x1...xn] : [lp x1 \@ sep x2 ... \@ sep xn rp]
and nothing if the list is empty
a breaking space is added before every [sep]. *)
val print_list_l :
(Format.formatter -> 'a -> unit) ->
string -> string -> string -> Format.formatter -> 'a list -> unit
(** Print the couple [(c1,c2)] as [lp c1 sep \@, c2 rp]
no space is added, but a break right after [sep]. *)
no space is added, but a break right after [sep]. *)
val print_couple :
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
string -> string -> string -> Format.formatter -> 'a * 'b -> unit
(** Print something only in the case of [Some] *)
(** Print something only in the case of [Some] *)
val print_opt : ('a -> 'b -> unit) -> 'a -> 'b option -> unit
(** Print [sep][s] only when [Some(s)]. *)
val print_opt2 :
(Format.formatter -> 'a -> unit) ->
string -> Format.formatter -> 'a option -> unit
(** {2 Common and usual syntax} *)
(** Theses functions are not exporting breaks
and they assume the same from the print functions passed as arguments *)
@ -56,5 +56,5 @@ val print_opt2 :
(** Print a record as [{field1;\@ field2;\@ ...}] with an hv<2> box *)
val print_record :
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
val print_type_params : Format.formatter -> string list -> unit