diff --git a/lustrec.odocl b/lustrec.odocl
index 0c300095da789fb78db641cab067588b5fd9c230..6e8696909198d6e43399fb5bc51899ecc6cde785 100644
--- a/lustrec.odocl
+++ b/lustrec.odocl
@@ -7,6 +7,9 @@ backends/C/C_backend_main
backends/C/C_backend_makefile
backends/C/C_backend_spec
backends/C/C_backend_src
+backends/Horn/Horn_backend_common
+backends/Horn/Horn_backend_printers
+backends/Horn/Horn_backend_collecting_sem
backends/Horn/Horn_backend
plugins/scopes/Scopes
Basic_library
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 32651e4f590fbc33b39df36398851aff39c2948f..b49df21c24164c0403485f0178a68d3b6c51c6e2 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -182,7 +182,7 @@ let rec pp_c_val self pp_var fmt v =
| Cst c -> pp_c_const fmt c
| Array vl -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
| Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
- | Power (v, n) -> assert false
+ | Power (v, n) -> (Format.eprintf "internal error: C_backend_common.pp_c_val %a@." pp_val v; assert false)
| LocalVar v -> pp_var fmt v
| StateVar v ->
(* array memory vars are represented by an indirection to a local var with the right type,
diff --git a/src/backends/C/c_backend_makefile.ml b/src/backends/C/c_backend_makefile.ml
index 3bfee7e70f340fedf1efbe19333e42a5dc25cc49..a006cd7b8ff40c0e0ef24b59be08b52e4e63315d 100644
--- a/src/backends/C/c_backend_makefile.ml
+++ b/src/backends/C/c_backend_makefile.ml
@@ -70,7 +70,7 @@ let print_makefile basename nodename (dependencies: dep_t list) fmt =
fprintf fmt "@.";
(* Main binary *)
- fprintf fmt "%s_%s:@." basename nodename;
+ fprintf fmt "%s_%s: %s.c %s_main.c@." basename nodename basename basename;
fprintf fmt "\t${GCC} -O0 -I${INC} -I. -c %s.c@." basename;
fprintf fmt "\t${GCC} -O0 -I${INC} -I. -c %s_main.c@." basename;
fprintf_dependencies fmt dependencies;
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 0b08a7ebc0eb335493f65f43ca97295e0aa97363..f4a3b532584d6505f3bb243fcae401b72235a30c 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -325,6 +325,7 @@ let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
and pp_machine_instr dependencies (m: machine_t) self fmt instr =
match instr with
+ | MNoReset _ -> ()
| MReset i ->
pp_machine_reset m self fmt i
| MLocalAssign (i,v) ->
@@ -361,7 +362,7 @@ and pp_machine_instr dependencies (m: machine_t) self fmt instr =
(pp_c_val self (pp_c_var_read m)) g
(Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl
| MComment s ->
- fprintf fmt "//%s@ " s
+ fprintf fmt "/*%s*/@ " s
and pp_machine_branch dependencies m self fmt (t, h) =
diff --git a/src/backends/Horn/horn_backend_printers.ml b/src/backends/Horn/horn_backend_printers.ml
index 37ecfeea9fec01575d0cb942eba84facd202631d..530ebe510b1069e5555f42b0725d558cac18a66f 100644
--- a/src/backends/Horn/horn_backend_printers.ml
+++ b/src/backends/Horn/horn_backend_printers.ml
@@ -42,7 +42,7 @@ let pp_horn_tag fmt t =
let rec pp_horn_const fmt c =
match c with
| Const_int i -> pp_print_int fmt i
- | Const_real (_,_s) -> pp_print_string fmt s
+ | Const_real (_,_,s) -> pp_print_string fmt s
| Const_tag t -> pp_horn_tag fmt t
| _ -> assert false
@@ -51,7 +51,7 @@ let rec pp_horn_const fmt c =
but an offset suffix may be added for array variables
*)
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
- match v with
+ match v.value_desc with
| Cst c -> pp_horn_const fmt c
| Array _
| Access _ -> assert false (* no arrays *)
@@ -65,7 +65,7 @@ let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
(* Prints a [value] indexed by the suffix list [loop_vars] *)
let rec pp_value_suffix self pp_value fmt value =
- match value with
+ match value.value_desc with
| Fun (n, vl) ->
Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
| _ ->
@@ -77,7 +77,7 @@ let rec pp_value_suffix self pp_value fmt value =
- [value]: assigned value
- [pp_var]: printer for variables
*)
-let pp_assign m pp_var fmt var_type var_name value =
+let pp_assign m pp_var fmt var_name value =
let self = m.mname.node_id in
fprintf fmt "(= %a %a)"
(pp_horn_val ~is_lhs:true self pp_var) var_name
@@ -156,7 +156,7 @@ let pp_instance_call machines reset_instances m fmt i inputs outputs =
| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
fprintf fmt "@[<v 5>(and ";
fprintf fmt "(= %a (ite %a %a %a))"
- (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (LocalVar o) (* output var *)
+ (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
(pp_horn_var m) mem_m
(pp_horn_val self (pp_horn_var m)) i1
(pp_horn_val self (pp_horn_var m)) i2
@@ -172,7 +172,7 @@ let pp_instance_call machines reset_instances m fmt i inputs outputs =
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
(Utils.pp_final_char_if_non_empty "@ " inputs)
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
- (List.map (fun v -> LocalVar v) outputs)
+ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
(Utils.pp_final_char_if_non_empty "@ " outputs)
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
@@ -186,7 +186,7 @@ let pp_instance_call machines reset_instances m fmt i inputs outputs =
inputs
(Utils.pp_final_char_if_non_empty "@ " inputs)
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
- (List.map (fun v -> LocalVar v) outputs)
+ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
)
@@ -202,14 +202,14 @@ let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ide
| MLocalAssign (i,v) ->
pp_assign
m (pp_horn_var m) fmt
- i.var_type (LocalVar i) v;
+ (mk_val (LocalVar i) i.var_type) v;
reset_instances
| MStateAssign (i,v) ->
pp_assign
m (pp_horn_var m) fmt
- i.var_type (StateVar i) v;
+ (mk_val (StateVar i) i.var_type) v;
reset_instances
- | MStep ([i0], i, vl) when Basic_library.is_internal_fun i ->
+ | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
assert false (* This should not happen anymore *)
| MStep (il, i, vl) ->
(* if reset instance, just print the call over mem_m , otherwise declare mem_m =
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index 879d4313f800333e05c8f07368d7d7cd748e867c..6c368487fc0f873d4106bba3ba04a48a181919d1 100755
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -42,11 +42,8 @@ let rec occurs cvar ck =
| Ctuple ckl ->
List.exists (occurs cvar) ckl
| Con (ck',_,_) -> occurs cvar ck'
- | Pck_up (ck',_) -> occurs cvar ck'
- | Pck_down (ck',_) -> occurs cvar ck'
- | Pck_phase (ck',_) -> occurs cvar ck'
- | Cvar _ -> ck=cvar
- | Cunivar _ | Pck_const (_,_) -> false
+ | Cvar -> ck=cvar
+ | Cunivar -> false
| Clink ck' -> occurs cvar ck'
| Ccarrying (_,ck') -> occurs cvar ck'
@@ -70,14 +67,11 @@ let rec generalize ck =
| Ctuple clist ->
List.iter generalize clist
| Con (ck',cr,_) -> generalize ck'; generalize_carrier cr
- | Cvar cset ->
+ | Cvar ->
if ck.cscoped then
raise (Scope_clock ck);
- ck.cdesc <- Cunivar cset
- | Pck_up (ck',_) -> generalize ck'
- | Pck_down (ck',_) -> generalize ck'
- | Pck_phase (ck',_) -> generalize ck'
- | Pck_const (_,_) | Cunivar _ -> ()
+ ck.cdesc <- Cunivar
+ | Cunivar -> ()
| Clink ck' ->
generalize ck'
| Ccarrying (cr,ck') ->
@@ -123,59 +117,21 @@ let rec instantiate inst_ck_vars inst_cr_vars ck =
| Con (ck',c,l) ->
let c' = instantiate_carrier c inst_cr_vars in
{ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)}
- | Cvar _ | Pck_const (_,_) -> ck
- | Pck_up (ck',k) ->
- {ck with cdesc = Pck_up ((instantiate inst_ck_vars inst_cr_vars ck'),k)}
- | Pck_down (ck',k) ->
- {ck with cdesc = Pck_down ((instantiate inst_ck_vars inst_cr_vars ck'),k)}
- | Pck_phase (ck',q) ->
- {ck with cdesc = Pck_phase ((instantiate inst_ck_vars inst_cr_vars ck'),q)}
+ | Cvar -> ck
| Clink ck' ->
{ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')}
| Ccarrying (cr,ck') ->
let cr' = instantiate_carrier cr inst_cr_vars in
{ck with cdesc =
Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')}
- | Cunivar cset ->
+ | Cunivar ->
try
List.assoc ck.cid !inst_ck_vars
with Not_found ->
- let var = new_ck (Cvar cset) true in
+ let var = new_ck Cvar true in
inst_ck_vars := (ck.cid, var)::!inst_ck_vars;
var
-(** [subsume pck1 cset1] subsumes clock [pck1] by clock subset
- [cset1]. The clock constraint is actually recursively transfered to
- the clock variable appearing in [pck1] *)
-let subsume pck1 cset1 =
- let rec aux pck cset =
- match cset with
- | CSet_all ->
- ()
- | CSet_pck (k,(a,b)) ->
- match pck.cdesc with
- | Cvar cset' ->
- pck.cdesc <- Cvar (intersect cset' cset)
- | Pck_up (pck',k') ->
- let rat = if a=0 then (0,1) else (a,b*k') in
- aux pck' (CSet_pck ((k*k'),rat))
- | Pck_down (pck',k') ->
- let k''=k/(gcd k k') in
- aux pck' (CSet_pck (k'',(a*k',b)))
- | Pck_phase (pck',(a',b')) ->
- let (a'',b'')= max_rat (sum_rat (a,b) (-a',b')) (0,1) in
- aux pck' (CSet_pck (k, (a'',b'')))
- | Pck_const (n,(a',b')) ->
- if n mod k <> 0 || (max_rat (a,b) (a',b')) <> (a',b') then
- raise (Subsume (pck1, cset1))
- | Clink pck' ->
- aux pck' cset
- | Cunivar _ -> ()
- | Ccarrying (_,ck') ->
- aux ck' cset
- | _ -> raise (Subsume (pck1, cset1))
- in
- aux pck1 cset1
let rec update_scope_carrier scoped cr =
if (not scoped) then
@@ -196,22 +152,13 @@ let rec update_scope scoped ck =
| Ctuple clist ->
List.iter (update_scope scoped) clist
| Con (ck',cr,_) -> update_scope scoped ck'(*; update_scope_carrier scoped cr*)
- | Cvar cset ->
- ck.cdesc <- Cvar cset
- | Pck_up (ck',_) -> update_scope scoped ck'
- | Pck_down (ck',_) -> update_scope scoped ck'
- | Pck_phase (ck',_) -> update_scope scoped ck'
- | Pck_const (_,_) | Cunivar _ -> ()
+ | Cvar | Cunivar -> ()
| Clink ck' ->
update_scope scoped ck'
| Ccarrying (cr,ck') ->
update_scope_carrier scoped cr; update_scope scoped ck'
end
-(* Unifies two static pclocks. *)
-let unify_static_pck ck1 ck2 =
- if (period ck1 <> period ck2) || (phase ck1 <> phase ck2) then
- raise (Unify (ck1,ck2))
(* Unifies two clock carriers *)
let unify_carrier cr1 cr2 =
@@ -279,8 +226,6 @@ let try_unify_carrier ck1 ck2 loc =
with
| Unify (ck1',ck2') ->
raise (Error (loc, Clock_clash (ck1',ck2')))
- | Subsume (ck,cset) ->
- raise (Error (loc, Clock_set_mismatch (ck,cset)))
| Mismatch (cr1,cr2) ->
raise (Error (loc, Carrier_mismatch (cr1,cr2)))
@@ -292,102 +237,40 @@ let rec unify ck1 ck2 =
if ck1==ck2 then
()
else
- let left_const = is_concrete_pck ck1 in
- let right_const = is_concrete_pck ck2 in
- if left_const && right_const then
- unify_static_pck ck1 ck2
- else
- match ck1.cdesc,ck2.cdesc with
- | Cvar cset1,Cvar cset2->
- if ck1.cid < ck2.cid then
- begin
- ck2.cdesc <- Clink (simplify ck1);
- update_scope ck2.cscoped ck1;
- subsume ck1 cset2
- end
- else
- begin
- ck1.cdesc <- Clink (simplify ck2);
- update_scope ck1.cscoped ck2;
- subsume ck2 cset1
- end
- | Cvar cset, Pck_up (_,_) | Cvar cset, Pck_down (_,_)
- | Cvar cset, Pck_phase (_,_) | Cvar cset, Pck_const (_,_) ->
- if (occurs ck1 ck2) then
- begin
- if (simplify ck2 = ck1) then
- ck2.cdesc <- Clink (simplify ck1)
- else
- raise (Unify (ck1,ck2));
- end
- else
- begin
- ck1.cdesc <- Clink (simplify ck2);
- subsume ck2 cset
- end
- | Pck_up (_,_), Cvar cset | Pck_down (_,_), Cvar cset
- | Pck_phase (_,_), Cvar cset | Pck_const (_,_), Cvar cset ->
- if (occurs ck2 ck1) then
- begin
- if ((simplify ck1) = ck2) then
- ck1.cdesc <- Clink (simplify ck2)
- else
- raise (Unify (ck1,ck2));
- end
- else
- begin
- ck2.cdesc <- Clink (simplify ck1);
- subsume ck1 cset
- end
- | (Cvar cset,_) when (not (occurs ck1 ck2)) ->
- subsume ck2 cset;
- update_scope ck1.cscoped ck2;
- ck1.cdesc <- Clink (simplify ck2)
- | (_, (Cvar cset)) when (not (occurs ck2 ck1)) ->
- subsume ck1 cset;
- update_scope ck2.cscoped ck1;
- ck2.cdesc <- Clink (simplify ck1)
- | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
- unify_carrier cr1 cr2;
- unify ck1' ck2'
- | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
- raise (Unify (ck1,ck2))
- | Carrow (c1,c2), Carrow (c1',c2') ->
- unify c1 c1'; unify c2 c2'
- | Ctuple ckl1, Ctuple ckl2 ->
- if (List.length ckl1) <> (List.length ckl2) then
- raise (Unify (ck1,ck2));
- List.iter2 unify ckl1 ckl2
- | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
- unify_carrier c1 c2;
- unify ck' ck''
- | Pck_const (i,r), Pck_const (i',r') ->
- if i<>i' || r <> r' then
- raise (Unify (ck1,ck2))
- | (_, Pck_up (pck2',k)) when (not right_const) ->
- let ck1' = simplify (new_ck (Pck_down (ck1,k)) true) in
- unify ck1' pck2'
- | (_,Pck_down (pck2',k)) when (not right_const) ->
- subsume ck1 (CSet_pck (k,(0,1)));
- let ck1' = simplify (new_ck (Pck_up (ck1,k)) true) in
- unify ck1' pck2'
- | (_,Pck_phase (pck2',(a,b))) when (not right_const) ->
- subsume ck1 (CSet_pck (b,(a,b)));
- let ck1' = simplify (new_ck (Pck_phase (ck1,(-a,b))) true) in
- unify ck1' pck2'
- | Pck_up (pck1',k),_ ->
- let ck2' = simplify (new_ck (Pck_down (ck2,k)) true) in
- unify pck1' ck2'
- | Pck_down (pck1',k),_ ->
- subsume ck2 (CSet_pck (k,(0,1)));
- let ck2' = simplify (new_ck (Pck_up (ck2,k)) true) in
- unify pck1' ck2'
- | Pck_phase (pck1',(a,b)),_ ->
- subsume ck2 (CSet_pck (b,(a,b)));
- let ck2' = simplify (new_ck (Pck_phase (ck2,(-a,b))) true) in
- unify pck1' ck2'
- | Cunivar _, _ | _, Cunivar _ -> ()
- | _,_ -> raise (Unify (ck1,ck2))
+ match ck1.cdesc,ck2.cdesc with
+ | Cvar, Cvar ->
+ if ck1.cid < ck2.cid then
+ begin
+ ck2.cdesc <- Clink (simplify ck1);
+ update_scope ck2.cscoped ck1
+ end
+ else
+ begin
+ ck1.cdesc <- Clink (simplify ck2);
+ update_scope ck1.cscoped ck2
+ end
+ | (Cvar, _) when (not (occurs ck1 ck2)) ->
+ update_scope ck1.cscoped ck2;
+ ck1.cdesc <- Clink (simplify ck2)
+ | (_, Cvar) when (not (occurs ck2 ck1)) ->
+ update_scope ck2.cscoped ck1;
+ ck2.cdesc <- Clink (simplify ck1)
+ | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
+ unify_carrier cr1 cr2;
+ unify ck1' ck2'
+ | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
+ raise (Unify (ck1,ck2))
+ | Carrow (c1,c2), Carrow (c1',c2') ->
+ unify c1 c1'; unify c2 c2'
+ | Ctuple ckl1, Ctuple ckl2 ->
+ if (List.length ckl1) <> (List.length ckl2) then
+ raise (Unify (ck1,ck2));
+ List.iter2 unify ckl1 ckl2
+ | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
+ unify_carrier c1 c2;
+ unify ck' ck''
+ | Cunivar, _ | _, Cunivar -> ()
+ | _,_ -> raise (Unify (ck1,ck2))
(** [unify ck1 ck2] semi-unifies clocks [ck1] and [ck2]. Raises [Unify
(ck1,ck2)] if the clocks are not semi-unifiable.*)
@@ -398,7 +281,7 @@ let rec semi_unify ck1 ck2 =
()
else
match ck1.cdesc,ck2.cdesc with
- | Cvar cset1,Cvar cset2->
+ | Cvar, Cvar ->
if ck1.cid < ck2.cid then
begin
ck2.cdesc <- Clink (simplify ck1);
@@ -409,8 +292,8 @@ let rec semi_unify ck1 ck2 =
ck1.cdesc <- Clink (simplify ck2);
update_scope ck1.cscoped ck2
end
- | (Cvar cset,_) -> raise (Unify (ck1,ck2))
- | (_, (Cvar cset)) when (not (occurs ck2 ck1)) ->
+ | (Cvar, _) -> raise (Unify (ck1,ck2))
+ | (_, Cvar) when (not (occurs ck2 ck1)) ->
update_scope ck2.cscoped ck1;
ck2.cdesc <- Clink (simplify ck1)
| Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
@@ -430,7 +313,7 @@ let rec semi_unify ck1 ck2 =
| Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
semi_unify_carrier c1 c2;
semi_unify ck' ck''
- | Cunivar _, _ | _, Cunivar _ -> ()
+ | Cunivar, _ | _, Cunivar -> ()
| _,_ -> raise (Unify (ck1,ck2))
(* Returns the value corresponding to a pclock (integer) factor
@@ -456,8 +339,6 @@ let try_unify ck1 ck2 loc =
with
| Unify (ck1',ck2') ->
raise (Error (loc, Clock_clash (ck1',ck2')))
- | Subsume (ck,cset) ->
- raise (Error (loc, Clock_set_mismatch (ck,cset)))
| Mismatch (cr1,cr2) ->
raise (Error (loc, Carrier_mismatch (cr1,cr2)))
@@ -467,8 +348,6 @@ let try_semi_unify ck1 ck2 loc =
with
| Unify (ck1',ck2') ->
raise (Error (loc, Clock_clash (ck1',ck2')))
- | Subsume (ck,cset) ->
- raise (Error (loc, Clock_set_mismatch (ck,cset)))
| Mismatch (cr1,cr2) ->
raise (Error (loc, Carrier_mismatch (cr1,cr2)))
@@ -500,8 +379,6 @@ let try_sub_unify sub ck1 ck2 loc =
with
| Unify (ck1',ck2') ->
raise (Error (loc, Clock_clash (ck1',ck2')))
- | Subsume (ck,cset) ->
- raise (Error (loc, Clock_set_mismatch (ck,cset)))
| Mismatch (cr1,cr2) ->
raise (Error (loc, Carrier_mismatch (cr1,cr2)))
@@ -515,7 +392,7 @@ let unify_tuple_clock ref_ck_opt ck loc =
let rec aux ck =
match (repr ck).cdesc with
| Con _
- | Cvar _ ->
+ | Cvar ->
begin
match !ck_var with
| None ->
@@ -539,7 +416,7 @@ let unify_imported_clock ref_ck_opt ck loc =
let ck_var = ref ref_ck_opt in
let rec aux ck =
match (repr ck).cdesc with
- | Cvar _ ->
+ | Cvar ->
begin
match !ck_var with
| None ->
@@ -744,10 +621,6 @@ let clock_eq env eq =
let clock_coreclock env cck id loc scoped =
match cck.ck_dec_desc with
| Ckdec_any -> new_var scoped
- | Ckdec_pclock (n,(a,b)) ->
- let ck = new_ck (Pck_const (n,(a,b))) scoped in
- if n mod b <> 0 then raise (Error (loc,Invalid_const ck));
- ck
| Ckdec_bool cl ->
let temp_env = Env.add_value env id (new_var true) in
(* We just want the id to be present in the environment *)
@@ -837,19 +710,9 @@ let check_imported_pclocks loc ck_node =
| Carrow (ck1,ck2) -> aux ck1; aux ck2
| Ctuple cl -> List.iter aux cl
| Con (ck',_,_) -> aux ck'
- | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) ->
- raise (Error (loc, (Invalid_imported_clock ck_node)))
- | Pck_const (n,p) ->
- begin
- match !pck with
- | None -> pck := Some (n,p)
- | Some (n',p') ->
- if (n,p) <> (n',p') then
- raise (Error (loc, (Invalid_imported_clock ck_node)))
- end
| Clink ck' -> aux ck'
| Ccarrying (_,ck') -> aux ck'
- | Cvar _ | Cunivar _ ->
+ | Cvar | Cunivar ->
match !pck with
| None -> ()
| Some (_,_) ->
diff --git a/src/clocks.ml b/src/clocks.ml
index 7b703487051ed2a74c7f8fb896e51613e52f05db..8756e2476685b2c742e091b6a15fbedf6fa74dad 100755
--- a/src/clocks.ml
+++ b/src/clocks.ml
@@ -15,10 +15,10 @@
open Utils
open Format
-(* Clock type sets, for subtyping. *)
-type clock_set =
- CSet_all
- | CSet_pck of int*rat
+(* (\* Clock type sets, for subtyping. *\) *)
+(* type clock_set = *)
+(* CSet_all *)
+(* | CSet_pck of int*rat *)
(* Clock carriers basically correspond to the "c" in "x when c" *)
type carrier_desc =
@@ -44,19 +44,19 @@ and clock_desc =
| Carrow of clock_expr * clock_expr
| Ctuple of clock_expr list
| Con of clock_expr * carrier_expr * ident
- | Pck_up of clock_expr * int
- | Pck_down of clock_expr * int
- | Pck_phase of clock_expr * rat
- | Pck_const of int * rat
- | Cvar of clock_set (* Monomorphic clock variable *)
- | Cunivar of clock_set (* Polymorphic clock variable *)
+ (* | Pck_up of clock_expr * int *)
+ (* | Pck_down of clock_expr * int *)
+ (* | Pck_phase of clock_expr * rat *)
+ (* | Pck_const of int * rat *)
+ | Cvar (* of clock_set *) (* Monomorphic clock variable *)
+ | Cunivar (* of clock_set *) (* Polymorphic clock variable *)
| Clink of clock_expr (* During unification, make links instead of substitutions *)
| Ccarrying of carrier_expr * clock_expr
type error =
| Clock_clash of clock_expr * clock_expr
- | Not_pck
- | Clock_set_mismatch of clock_expr * clock_set
+ (* | Not_pck *)
+ (* | Clock_set_mismatch of clock_expr * clock_set *)
| Cannot_be_polymorphic of clock_expr
| Invalid_imported_clock of clock_expr
| Invalid_const of clock_expr
@@ -66,22 +66,11 @@ type error =
| Clock_extrusion of clock_expr * clock_expr
exception Unify of clock_expr * clock_expr
-exception Subsume of clock_expr * clock_set
exception Mismatch of carrier_expr * carrier_expr
exception Scope_carrier of carrier_expr
exception Scope_clock of clock_expr
exception Error of Location.t * error
-let print_ckset fmt s =
- match s with
- | CSet_all -> ()
- | CSet_pck (k,q) ->
- let (a,b) = simplify_rat q in
- if k = 1 && a = 0 then
- fprintf fmt "<:P"
- else
- fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
-
let rec print_carrier fmt cr =
(* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
match cr.carrier_desc with
@@ -104,18 +93,8 @@ let rec print_ck_long fmt ck =
(fprintf_list ~sep:" * " print_ck_long) cklist
| Con (ck,c,l) ->
fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
- | Pck_up (ck,k) ->
- fprintf fmt "%a*^%i" print_ck_long ck k
- | Pck_down (ck,k) ->
- fprintf fmt "%a/^%i" print_ck_long ck k
- | Pck_phase (ck,q) ->
- fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
- | Pck_const (n,p) ->
- fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
- | Cvar cset ->
- fprintf fmt "'_%i%a" ck.cid print_ckset cset
- | Cunivar cset ->
- fprintf fmt "'%i%a" ck.cid print_ckset cset
+ | Cvar -> fprintf fmt "'_%i" ck.cid
+ | Cunivar -> fprintf fmt "'%i" ck.cid
| Clink ck' ->
fprintf fmt "link %a" print_ck_long ck'
| Ccarrying (cr,ck') ->
@@ -129,11 +108,9 @@ let rec bottom =
let new_ck desc scoped =
incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped}
-let new_var scoped =
- new_ck (Cvar CSet_all) scoped
+let new_var scoped = new_ck Cvar scoped
-let new_univar () =
- new_ck (Cunivar CSet_all) false
+let new_univar () = new_ck Cunivar false
let new_carrier_id = ref (-1)
@@ -187,23 +164,17 @@ let uncarrier ck =
(* Removes all links in a clock. Only used for clocks
simplification though. *)
-let rec deep_repr ck =
+let rec simplify ck =
match ck.cdesc with
| Carrow (ck1,ck2) ->
- new_ck (Carrow (deep_repr ck1, deep_repr ck2)) ck.cscoped
+ new_ck (Carrow (simplify ck1, simplify ck2)) ck.cscoped
| Ctuple cl ->
- new_ck (Ctuple (List.map deep_repr cl)) ck.cscoped
+ new_ck (Ctuple (List.map simplify cl)) ck.cscoped
| Con (ck', c, l) ->
- new_ck (Con (deep_repr ck', c, l)) ck.cscoped
- | Pck_up (ck',k) ->
- new_ck (Pck_up (deep_repr ck',k)) ck.cscoped
- | Pck_down (ck',k) ->
- new_ck (Pck_down (deep_repr ck',k)) ck.cscoped
- | Pck_phase (ck',q) ->
- new_ck (Pck_phase (deep_repr ck',q)) ck.cscoped
- | Pck_const (_,_) | Cvar _ | Cunivar _ -> ck
- | Clink ck' -> deep_repr ck'
- | Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, deep_repr ck')) ck.cscoped
+ new_ck (Con (simplify ck', c, l)) ck.cscoped
+ | Cvar | Cunivar -> ck
+ | Clink ck' -> simplify ck'
+ | Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, simplify ck')) ck.cscoped
(** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock
(ensured by language syntax) *)
@@ -233,54 +204,21 @@ let clock_current ck =
let clock_of_impnode_clock ck =
let ck = repr ck in
match ck.cdesc with
- | Carrow _ | Clink _ | Cvar _ | Cunivar _ ->
+ | Carrow _ | Clink _ | Cvar | Cunivar ->
failwith "internal error clock_of_impnode_clock"
| Ctuple cklist -> List.hd cklist
- | Con (_,_,_) | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_)
- | Pck_const (_,_) | Ccarrying (_,_) -> ck
-
-(** [intersect set1 set2] returns the intersection of clock subsets
- [set1] and [set2]. *)
-let intersect set1 set2 =
- match set1,set2 with
- | CSet_all,_ -> set2
- | _,CSet_all -> set1
- | CSet_pck (k,q), CSet_pck (k',q') ->
- let k'',q'' = lcm k k',max_rat q q' in
- CSet_pck (k'',q'')
-
-(** [can_be_pck ck] returns true if [ck] "may be" a pclock (the uncertainty is
- due to clock variables) *)
-let rec can_be_pck ck =
- match (repr ck).cdesc with
- | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) | Pck_const (_,_)
- | Cvar _ | Cunivar _ ->
- true
- | Ccarrying (_,ck') -> can_be_pck ck
- | _ -> false
-
-(** [is_concrete_pck ck] returns true if [ck] is a concrete [pck] (pck
- transformations applied to a pck constant) *)
-let rec is_concrete_pck ck =
- match ck.cdesc with
- | Carrow (_,_) | Ctuple _ | Con (_,_,_)
- | Cvar _ | Cunivar _ -> false
- | Pck_up (ck',_) | Pck_down (ck',_) -> is_concrete_pck ck'
- | Pck_phase (ck',_) -> is_concrete_pck ck'
- | Pck_const (_,_) -> true
- | Clink ck' -> is_concrete_pck ck'
- | Ccarrying (_,ck') -> false
+ | Con (_,_,_)
+ | Ccarrying (_,_) -> ck
+
(** [is_polymorphic ck] returns true if [ck] is polymorphic. *)
let rec is_polymorphic ck =
match ck.cdesc with
- | Cvar _ | Pck_const (_,_) -> false
+ | Cvar -> false
| Carrow (ck1,ck2) -> (is_polymorphic ck1) || (is_polymorphic ck2)
| Ctuple ckl -> List.exists (fun c -> is_polymorphic c) ckl
| Con (ck',_,_) -> is_polymorphic ck'
- | Pck_up (ck',_) | Pck_down (ck',_) -> is_polymorphic ck'
- | Pck_phase (ck',_) -> is_polymorphic ck'
- | Cunivar _ -> true
+ | Cunivar -> true
| Clink ck' -> is_polymorphic ck'
| Ccarrying (_,ck') -> is_polymorphic ck'
@@ -290,15 +228,7 @@ let rec is_polymorphic ck =
let rec constrained_vars_of_clock ck =
let rec aux vars ck =
match ck.cdesc with
- | Pck_const (_,_) ->
- vars
- | Cvar cset ->
- begin
- match cset with
- | CSet_all -> vars
- | _ ->
- list_union [ck] vars
- end
+ | Cvar -> vars
| Carrow (ck1,ck2) ->
let l = aux vars ck1 in
aux l ck2
@@ -307,65 +237,12 @@ let rec constrained_vars_of_clock ck =
(fun acc ck' -> aux acc ck')
vars ckl
| Con (ck',_,_) -> aux vars ck'
- | Pck_up (ck',_) | Pck_down (ck',_) -> aux vars ck'
- | Pck_phase (ck',_) -> aux vars ck'
- | Cunivar cset ->
- begin
- match cset with
- | CSet_all -> vars
- | _ -> list_union [ck] vars
- end
+ | Cunivar -> vars
| Clink ck' -> aux vars ck'
| Ccarrying (_,ck') -> aux vars ck'
in
aux [] ck
-(** [period ck] returns the period of [ck]. Expects a constant pclock
- expression belonging to the correct clock set. *)
-let rec period ck =
- let rec aux ck =
- match ck.cdesc with
- | Carrow (_,_) | Ctuple _ | Con (_,_,_)
- | Cvar _ | Cunivar _ ->
- failwith "internal error: can only compute period of const pck"
- | Pck_up (ck',k) ->
- (aux ck')/.(float_of_int k)
- | Pck_down (ck',k) ->
- (float_of_int k)*.(aux ck')
- | Pck_phase (ck',_) ->
- aux ck'
- | Pck_const (n,_) ->
- float_of_int n
- | Clink ck' -> aux ck'
- | Ccarrying (_,ck') -> aux ck'
- in
- int_of_float (aux ck)
-
-(** [phase ck] returns the phase of [ck]. It is not expressed as a
- fraction of the period, but instead as an amount of time. Expects a
- constant expression belonging to the correct P_k *)
-let phase ck =
- let rec aux ck =
- match ck.cdesc with
- | Carrow (_,_) | Ctuple _ | Con (_,_,_)
- | Cvar _ | Cunivar _ ->
- failwith "internal error: can only compute phase of const pck"
- | Pck_up (ck',_) ->
- aux ck'
- | Pck_down (ck',k) ->
- aux ck'
- | Pck_phase (ck',(a,b)) ->
- let n = period ck' in
- let (a',b') = aux ck' in
- sum_rat (a',b') (n*a,b)
- | Pck_const (n,(a,b)) ->
- (n*a,b)
- | Clink ck' -> aux ck'
- | Ccarrying (_,ck') -> aux ck'
- in
- let (a,b) = aux ck in
- simplify_rat (a,b)
-
let eq_carrier cr1 cr2 =
match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with
| Carry_const id1, Carry_const id2 -> id1 = id2
@@ -380,7 +257,7 @@ let rec root ck =
match ck.cdesc with
| Ctuple (ck'::_)
| Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') -> root ck'
- | Pck_up _ | Pck_down _ | Pck_phase _ | Pck_const _ | Cvar _ | Cunivar _ -> ck
+ | Cvar | Cunivar -> ck
| Carrow _ | Ctuple _ -> failwith "Internal error root"
(* Returns the branch of clock [ck] in its clock tree *)
@@ -419,117 +296,34 @@ let rec disjoint_branches br1 br2 =
let disjoint ck1 ck2 =
eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
-(** [normalize pck] returns the normal form of clock [pck]. *)
-let normalize pck =
- let changed = ref true in
- let rec aux pck =
- match pck.cdesc with
- | Pck_up ({cdesc=Pck_up (pck',k')},k) ->
- changed:=true;
- new_ck (Pck_up (aux pck',k*k')) pck.cscoped
- | Pck_up ({cdesc=Pck_down (pck',k')},k) ->
- changed:=true;
- new_ck (Pck_down (new_ck (Pck_up (aux pck',k)) pck.cscoped,k')) pck.cscoped
- | Pck_up ({cdesc=Pck_phase (pck',(a,b))},k) ->
- changed:=true;
- new_ck (Pck_phase (new_ck (Pck_up (aux pck',k)) pck.cscoped,(a*k,b))) pck.cscoped
- | Pck_down ({cdesc=Pck_down (pck',k')},k) ->
- changed:=true;
- new_ck (Pck_down (aux pck',k*k')) pck.cscoped
- | Pck_down ({cdesc=Pck_phase (pck',(a,b))},k) ->
- changed:=true;
- new_ck (Pck_phase (new_ck (Pck_down (aux pck',k)) pck.cscoped,(a,b*k))) pck.cscoped
- | Pck_phase ({cdesc=Pck_phase (pck',(a',b'))},(a,b)) ->
- changed:=true;
- let (a'',b'') = sum_rat (a,b) (a',b') in
- new_ck (Pck_phase (aux pck',(a'',b''))) pck.cscoped
- | Pck_up (pck',k') ->
- new_ck (Pck_up (aux pck',k')) pck.cscoped
- | Pck_down (pck',k') ->
- new_ck (Pck_down (aux pck',k')) pck.cscoped
- | Pck_phase (pck',k') ->
- new_ck (Pck_phase (aux pck',k')) pck.cscoped
- | Ccarrying (cr,ck') ->
- new_ck (Ccarrying (cr, aux ck')) pck.cscoped
- | _ -> pck
- in
- let nf=ref pck in
- while !changed do
- changed:=false;
- nf:=aux !nf
- done;
- !nf
-
-(** [canonize pck] reduces transformations of [pck] and removes
- identity transformations. Expects a normalized periodic clock ! *)
-let canonize pck =
- let rec remove_id_trans pck =
- match pck.cdesc with
- | Pck_up (pck',1) | Pck_down (pck',1) | Pck_phase (pck',(0,_)) ->
- remove_id_trans pck'
- | _ -> pck
- in
- let pck =
- match pck.cdesc with
- | Pck_phase ({cdesc=Pck_down ({cdesc=Pck_up (v,k)},k')},k'') ->
- let gcd = gcd k k' in
- new_ck (Pck_phase
- (new_ck (Pck_down
- (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd))
- pck.cscoped,k''))
- pck.cscoped
- | Pck_down ({cdesc=Pck_up (v,k)},k') ->
- let gcd = gcd k k' in
- new_ck (Pck_down (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd)) pck.cscoped
- | _ -> pck
- in
- remove_id_trans pck
-
-(** [simplify pck] applies pclocks simplifications to [pck] *)
-let simplify pck =
- if (is_concrete_pck pck) then
- let n = period pck in
- let (a,b) = phase pck in
- let phase' = simplify_rat (a,b*n) in
- new_ck (Pck_const (n,phase')) pck.cscoped
- else
- let pck' = deep_repr pck in
- let nf_pck = normalize pck' in
- canonize nf_pck
-
let print_cvar fmt cvar =
match cvar.cdesc with
- | Cvar cset ->
+ | Cvar ->
(*
if cvar.cscoped
then
- fprintf fmt "[_%s%a]"
+ fprintf fmt "[_%s]"
(name_of_type cvar.cid)
- print_ckset cset
else
*)
- fprintf fmt "_%s%a"
+ fprintf fmt "_%s"
(name_of_type cvar.cid)
- print_ckset cset
- | Cunivar cset ->
+ | Cunivar ->
(*
if cvar.cscoped
then
- fprintf fmt "['%s%a]"
+ fprintf fmt "['%s]"
(name_of_type cvar.cid)
- print_ckset cset
else
*)
- fprintf fmt "'%s%a"
+ fprintf fmt "'%s"
(name_of_type cvar.cid)
- print_ckset cset
| _ -> failwith "Internal error print_cvar"
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
complexity. *)
let print_ck fmt ck =
let rec aux fmt ck =
- let ck = simplify ck in
match ck.cdesc with
| Carrow (ck1,ck2) ->
fprintf fmt "%a -> %a" aux ck1 aux ck2
@@ -538,15 +332,7 @@ let print_ck fmt ck =
(fprintf_list ~sep:" * " aux) cklist
| Con (ck,c,l) ->
fprintf fmt "%a on %s(%a)" aux ck l print_carrier c
- | Pck_up (ck,k) ->
- fprintf fmt "%a*.%i" aux ck k
- | Pck_down (ck,k) ->
- fprintf fmt "%a/.%i" aux ck k
- | Pck_phase (ck,q) ->
- fprintf fmt "%a->.%a" aux ck print_rat (simplify_rat q)
- | Pck_const (n,p) ->
- fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
- | Cvar cset ->
+ | Cvar ->
(*
if ck.cscoped
then
@@ -554,7 +340,7 @@ let print_ck fmt ck =
else
*)
fprintf fmt "_%s" (name_of_type ck.cid)
- | Cunivar cset ->
+ | Cunivar ->
(*
if ck.cscoped
then
@@ -575,19 +361,18 @@ let print_ck fmt ck =
(* prints only the Con components of a clock, useful for printing nodes *)
let rec print_ck_suffix fmt ck =
- let ck = simplify ck in
match ck.cdesc with
| Carrow _
| Ctuple _
- | Cvar _
- | Cunivar _ -> ()
+ | Cvar
+ | Cunivar -> ()
| Con (ck,c,l) ->
fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
| Clink ck' ->
print_ck_suffix fmt ck'
| Ccarrying (cr,ck') ->
fprintf fmt "%a" print_ck_suffix ck'
- | _ -> assert false
+
let pp_error fmt = function
| Clock_clash (ck1,ck2) ->
@@ -595,17 +380,10 @@ let pp_error fmt = function
fprintf fmt "Expected clock %a, got clock %a@."
print_ck ck1
print_ck ck2
- | Not_pck ->
- fprintf fmt "The clock of this expression must be periodic@."
| Carrier_mismatch (cr1, cr2) ->
fprintf fmt "Name clash. Expected clock %a, got clock %a@."
print_carrier cr1
print_carrier cr2
- | Clock_set_mismatch (ck,cset) ->
- reset_names ();
- fprintf fmt "Clock %a is not included in clock set %a@."
- print_ck ck
- print_ckset cset
| Cannot_be_polymorphic ck ->
reset_names ();
fprintf fmt "The main node cannot have a polymorphic clock: %a@."
@@ -630,11 +408,11 @@ let pp_error fmt = function
print_ck ck
let const_of_carrier cr =
- match (carrier_repr cr).carrier_desc with
- | Carry_const id -> id
- | Carry_name
- | Carry_var
- | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
+ match (carrier_repr cr).carrier_desc with
+ | Carry_const id -> id
+ | Carry_name
+ | Carry_var
+ | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
let uneval const cr =
(*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)
diff --git a/src/inliner.ml b/src/inliner.ml
index 50ac9b813e24b47d88c8f60d439bde55a431d0c8..de1f975dc4fff63266d42cabd7e5675502c1be66 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -39,6 +39,46 @@ let rename_eq rename eq =
eq_lhs = List.map rename eq.eq_lhs;
eq_rhs = rename_expr rename eq.eq_rhs
}
+
+let rec add_expr_reset_cond cond expr =
+ let aux = add_expr_reset_cond cond in
+ let new_desc =
+ match expr.expr_desc with
+ | Expr_const _
+ | Expr_ident _ -> expr.expr_desc
+ | Expr_tuple el -> Expr_tuple (List.map aux el)
+ | Expr_ite (c, t, e) -> Expr_ite (aux c, aux t, aux e)
+
+ | Expr_arrow (e1, e2) ->
+ (* we replace the expression e1 -> e2 by e1 -> (if cond then e1 else e2) *)
+ let e1 = aux e1 and e2 = aux e2 in
+ (* inlining is performed before typing. we can leave the fields free *)
+ let new_e2 = mkexpr expr.expr_loc (Expr_ite (cond, e1, e2)) in
+ Expr_arrow (e1, new_e2)
+
+ | Expr_fby _ -> assert false (* TODO: deal with fby. This hasn't been much handled yet *)
+
+ | Expr_array el -> Expr_array (List.map aux el)
+ | Expr_access (e, dim) -> Expr_access (aux e, dim)
+ | Expr_power (e, dim) -> Expr_power (aux e, dim)
+ | Expr_pre e -> Expr_pre (aux e)
+ | Expr_when (e, id, l) -> Expr_when (aux e, id, l)
+ | Expr_merge (id, cases) -> Expr_merge (id, List.map (fun (l,e) -> l, aux e) cases)
+
+ | Expr_appl (id, args, reset_opt) ->
+ (* we "add" cond to the reset field. *)
+ let new_reset = match reset_opt with
+ None -> cond
+ | Some cond' -> mkpredef_call cond'.expr_loc "||" [cond; cond']
+ in
+ Expr_appl (id, args, Some new_reset)
+
+
+ in
+ { expr with expr_desc = new_desc }
+
+let add_eq_reset_cond cond eq =
+ { eq with eq_rhs = add_expr_reset_cond cond eq.eq_rhs }
(*
let get_static_inputs input_arg_list =
List.fold_right (fun (vdecl, arg) res ->
@@ -54,6 +94,8 @@ let get_carrier_inputs input_arg_list =
else res)
input_arg_list []
*)
+
+
(*
expr, locals', eqs = inline_call id args' reset locals node nodes
@@ -64,12 +106,11 @@ We select the called node equations and variables.
the resulting expression is tuple_of_renamed_outputs
TODO: convert the specification/annotation/assert and inject them
-DONE: annotations
-TODO: deal with reset
*)
-let inline_call node orig_expr args reset locals caller =
- let loc = orig_expr.expr_loc in
- let uid = orig_expr.expr_tag in
+(** [inline_call node loc uid args reset locals caller] returns a tuple (expr,
+ locals, eqs, asserts)
+*)
+let inline_call node loc uid args reset locals caller =
let rename v =
if v = tag_true || v = tag_false || not (is_node_var node v) then v else
Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
@@ -97,35 +138,39 @@ let inline_call node orig_expr args reset locals caller =
v.var_dec_const,
Utils.option_map (rename_expr rename) v.var_dec_value) in
begin
-(*
- (try
- Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
- Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
- with Not_found -> ());
- (try
-Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
- with Not_found -> ());
-(*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
-*)
+ (*
+ (try
+ Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
+ Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
+ with Not_found -> ());
+ (try
+ Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
+ with Not_found -> ());
+ (*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
+ *)
vdecl
end
- (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
+ (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
in
let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in
let outputs' = List.map rename_var node.node_outputs in
let locals' =
- (List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs)
+ (List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs)
@ (List.map rename_var node.node_locals)
-in
+ in
(* checking we are at the appropriate (early) step: node_checks and
node_gencalls should be empty (not yet assigned) *)
assert (node.node_checks = []);
assert (node.node_gencalls = []);
- (* Bug included: todo deal with reset *)
- assert (reset = None);
-
- let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in
+ (* Expressing reset locally in equations *)
+ let eqs_r' =
+ match reset with
+ None -> eqs'
+ | Some cond -> List.map (add_eq_reset_cond cond) eqs'
+ in
+ let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs',
+ expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in
let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
in
let asserts' = (* We rename variables in assert expressions *)
@@ -134,7 +179,7 @@ in
{a with assert_expr =
let expr = a.assert_expr in
rename_expr rename expr
- })
+ })
node.node_asserts
in
let annots' =
@@ -142,7 +187,7 @@ in
in
expr,
inputs'@outputs'@locals'@locals,
- assign_inputs::eqs',
+ assign_inputs::eqs_r',
asserts',
annots'
@@ -194,7 +239,7 @@ let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
let called = node_of_top called in
let called' = inline_node called nodes in
let expr, locals', eqs'', asserts'', annots'' =
- inline_call called' expr args' reset locals' node in
+ inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in
expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
else
(* let _ = Format.eprintf "Not inlining call to %s@." id in *)
diff --git a/src/lustreSpec.ml b/src/lustreSpec.ml
index 991c5ed7102f5071d178efd3bce0c383da5e725f..dc05e1a1ee3438543ccc2ab82d225df5d82f1cfe 100644
--- a/src/lustreSpec.ml
+++ b/src/lustreSpec.ml
@@ -46,7 +46,7 @@ type clock_dec =
and clock_dec_desc =
| Ckdec_any
| Ckdec_bool of (ident * ident) list
- | Ckdec_pclock of int * rat
+
type constant =
| Const_int of int
@@ -241,6 +241,7 @@ type instr_t =
| MLocalAssign of var_decl * value_t
| MStateAssign of var_decl * value_t
| MReset of ident
+ | MNoReset of ident
| MStep of var_decl list * ident * value_t list
| MBranch of value_t * (label * instr_t list) list
| MComment of string
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 770462ff4b7088c55b7492162cfa652291ba8ca3..f17e061b9f27427814277c057bdb6095fe687930 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -36,6 +36,7 @@ let rec pp_instr fmt i =
| MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
| MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
| MReset i -> Format.fprintf fmt "reset %s" i
+ | MNoReset i -> Format.fprintf fmt "noreset %s" i
| MStep (il, i, vl) ->
Format.fprintf fmt "%a = %s (%a)"
(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
@@ -135,7 +136,7 @@ let dummy_var_decl name typ =
var_dec_const = false;
var_dec_value = None;
var_type = typ;
- var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true;
+ var_clock = Clocks.new_ck Clocks.Cvar true;
var_loc = Location.dummy_loc
}
@@ -352,7 +353,7 @@ let rec translate_expr node ((m, si, j, d, s) as args) expr =
| Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
let nd = node_from_name id in
Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
- | Expr_ite (g,t,e) -> (
+ (*| Expr_ite (g,t,e) -> (
(* special treatment depending on the active backend. For horn backend, ite
are preserved in expression. While they are removed for C or Java
backends. *)
@@ -360,7 +361,7 @@ let rec translate_expr node ((m, si, j, d, s) as args) expr =
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
| "C" | "java" | _ ->
(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
- )
+ )*)
| _ -> raise NormalizationError
in
mk_val value_desc expr.expr_type
@@ -373,16 +374,18 @@ let translate_guard node args expr =
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =
match expr.expr_desc with
| Expr_ite (c, t, e) -> let g = translate_guard node args c in
- conditional g [translate_act node args (y, t)]
+ conditional g
+ [translate_act node args (y, t)]
[translate_act node args (y, e)]
- | Expr_merge (x, hl) -> MBranch (translate_ident node args x, List.map (fun (t, h) -> t, [translate_act node args (y, h)]) hl)
+ | Expr_merge (x, hl) -> MBranch (translate_ident node args x,
+ List.map (fun (t, h) -> t, [translate_act node args (y, h)]) hl)
| _ -> MLocalAssign (y, translate_expr node args expr)
let reset_instance node args i r c =
match r with
| None -> []
| Some r -> let g = translate_guard node args r in
- [control_on_clock node args c (conditional g [MReset i] [])]
+ [control_on_clock node args c (conditional g [MReset i] [MNoReset i])]
let translate_eq node ((m, si, j, d, s) as args) eq =
(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
@@ -434,7 +437,7 @@ let translate_eq node ((m, si, j, d, s) as args) eq =
then []
else reset_instance node args o r call_ck) @
(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
-
+(*
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
are preserved. While they are replaced as if g then x = t else x = e in C or Java
backends. *)
@@ -450,6 +453,7 @@ let translate_eq node ((m, si, j, d, s) as args) eq =
(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
)
+*)
| [x], _ -> (
let var_x = get_node_var x node in
(m, si, j, d,
@@ -556,9 +560,9 @@ let translate_decl nd sch =
(* special treatment depending on the active backend. For horn backend,
common branches are not merged while they are in C or Java
backends. *)
- match !Options.output with
+ (*match !Options.output with
| "horn" -> s
- | "C" | "java" | _ -> join_guards_list s
+ | "C" | "java" | _ ->*) join_guards_list s
);
step_asserts =
let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index a44cd04ccd44517e18d5acdb37062d60d59baba8..8fafebffdc30df86dcc813e4e72e820c361828d7 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -88,6 +88,11 @@ let compile_source_to_header prog computed_types_env computed_clocks_env dirname
end
+let functional_backend () =
+ match !Options.output with
+ | "horn" | "lustre" | "acsl" -> true
+ | _ -> false
+
(* From prog to prog *)
let stage1 prog dirname basename =
(* Removing automata *)
@@ -122,7 +127,7 @@ let stage1 prog dirname basename =
(* Typing *)
let computed_types_env = type_decls type_env prog in
-
+
(* Clock calculus *)
let computed_clocks_env = clock_decls clock_env prog in
@@ -148,7 +153,7 @@ let stage1 prog dirname basename =
in
*)
(* Delay calculus *)
- (*
+ (* TO BE DONE LATER (Xavier)
if(!Options.delay_calculus)
then
begin
@@ -213,7 +218,7 @@ let stage1 prog dirname basename =
end
else
begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping FP numbers@,");
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
prog
end in
Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
@@ -221,7 +226,7 @@ let stage1 prog dirname basename =
(* Checking array accesses *)
if !Options.check then
begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. array access checks@,");
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
Access.check_prog prog;
end;
@@ -257,7 +262,7 @@ let stage2 prog =
let machine_code =
if !Options.optimization >= 4 && !Options.output <> "horn" then
begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 3)@,");
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: common sub-expression elimination@,");
Optimize_machine.machines_cse machine_code
end
else
@@ -267,7 +272,7 @@ let stage2 prog =
let machine_code, removed_table =
if !Options.optimization >= 2 && !Options.output <> "horn" then
begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 1)@ ");
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: constants inlining@,");
Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code
end
else
@@ -277,7 +282,7 @@ let stage2 prog =
let machine_code =
if !Options.optimization >= 3 && !Options.output <> "horn" then
begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 2)@ ");
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in
let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables)
@@ -292,7 +297,7 @@ let stage2 prog =
if !Options.salsa_enabled then
begin
check_main ();
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization (phase 3)@ ");
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,");
(* Selecting float constants for Salsa *)
let constEnv = List.fold_left (
fun accu c_topdecl ->
@@ -348,14 +353,14 @@ let stage3 prog machine_code dependencies basename =
let source_out = open_out source_file in
let fmt = formatter_of_out_channel source_out in
Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
- Horn_backend.translate fmt basename prog machine_code;
+ Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
(* Tracability file if option is activated *)
if !Options.traces then (
- let traces_file = destname ^ ".traces" in (* Could be changed *)
+ let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
let traces_out = open_out traces_file in
let fmt = formatter_of_out_channel traces_out in
Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
- Horn_backend.traces_file fmt basename prog machine_code;
+ Horn_backend_traces.traces_file fmt basename prog machine_code;
)
end
| "lustre" ->
diff --git a/src/normalization.ml b/src/normalization.ml
index 968fb2cc91be5da771271f536af3b8566b05d135..4a652118b09cae7f95c9e9b872adc9ff366ac026 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -393,8 +393,13 @@ let normalize_node node =
annots = List.map (fun v ->
let eq =
try
- List.find (fun eq -> eq.eq_lhs = [v.var_id]) (defs@assert_defs)
- with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
+ List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs)
+ with Not_found ->
+ (
+ Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id;
+ assert false
+ )
+ in
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
(["traceability"], pair)
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index c87b86b76823f051d468924071381605adeb0dc3..d4cc6c55ba4eb10c17d1ccb874461b092ef5e6a5 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -31,6 +31,7 @@ let rec eliminate elim instr =
| MLocalAssign (i,v) -> MLocalAssign (i, e_expr v)
| MStateAssign (i,v) -> MStateAssign (i, e_expr v)
| MReset i -> instr
+ | MNoReset i -> instr
| MStep (il, i, vl) -> MStep(il, i, List.map e_expr vl)
| MBranch (g,hl) ->
MBranch
@@ -51,7 +52,11 @@ and eliminate_expr elim expr =
| Cst _ | StateVar _ -> expr
let eliminate_dim elim dim =
- Dimension.expr_replace_expr (fun v -> try dimension_of_value (IMap.find v elim) with Not_found -> mkdim_ident dim.dim_loc v) dim
+ Dimension.expr_replace_expr
+ (fun v -> try
+ dimension_of_value (IMap.find v elim)
+ with Not_found -> mkdim_ident dim.dim_loc v)
+ dim
let unfold_expr_offset m offset expr =
List.fold_left
@@ -100,6 +105,7 @@ let rec simplify_instr_offset m instr =
| MLocalAssign (v, expr) -> MLocalAssign (v, simplify_expr_offset m expr)
| MStateAssign (v, expr) -> MStateAssign (v, simplify_expr_offset m expr)
| MReset id -> instr
+ | MNoReset id -> instr
| MStep (outputs, id, inputs) -> MStep (outputs, id, List.map (simplify_expr_offset m) inputs)
| MBranch (cond, brl)
-> MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)
diff --git a/src/parse.ml b/src/parse.ml
index 84ac6b3a049d18fb8080c5bd68237f36be1d681d..d54852e11588ac39bbc38a52facfedcd94bb65ab 100755
--- a/src/parse.ml
+++ b/src/parse.ml
@@ -32,7 +32,7 @@ let pp_error fmt err =
| Undefined_token tok -> fprintf fmt "undefined token '%s'" tok
| Unfinished_string -> fprintf fmt "unfinished string"
| Unfinished_comment -> fprintf fmt "unfinished comment"
- | Syntax_error -> fprintf fmt "syntax error"
+ | Syntax_error -> fprintf fmt ""
| Unfinished_annot -> fprintf fmt "unfinished annotation"
| Unfinished_node_spec -> fprintf fmt "unfinished node specification"
| Annot_error s -> fprintf fmt "impossible to parse the following annotation:@.%s@.@?" s
diff --git a/src/parser_lustre.mly b/src/parser_lustre.mly
index bc50bc6401167bdba79949392c0a64fc2b3dfbc0..ce9ff3715d9eef812cae1ea9022e5d10353468f1 100755
--- a/src/parser_lustre.mly
+++ b/src/parser_lustre.mly
@@ -623,7 +623,7 @@ when_list:
ident_list:
vdecl_ident {[$1]}
-| ident_list COMMA vdecl_ident {$3::$1}
+| vdecl_ident COMMA ident_list {$1::$3}
SCOL_opt:
SCOL {} | {}
diff --git a/src/typing.ml b/src/typing.ml
index d20b3c0ffaa2177dcda5f6d555cf49c3fa39d5b6..f6948d537d3e83db26943a12e6ee87b06c0d1f3d 100755
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -542,7 +542,7 @@ let type_eq env in_main undefined_vars eq =
in environment [env] *)
let type_coreclock env ck id loc =
match ck.ck_dec_desc with
- | Ckdec_any | Ckdec_pclock (_,_) -> ()
+ | Ckdec_any -> ()
| Ckdec_bool cl ->
let dummy_id_expr = expr_of_ident id loc in
let when_expr =