Commit 23353de9 authored by Maximilien Colange's avatar Maximilien Colange

Constant propagation in expressions used for LU bounds computation.

parent d1311e43
...@@ -633,6 +633,7 @@ struct ...@@ -633,6 +633,7 @@ struct
* if x is compared to e in the guard of t, then e \in S * if x is compared to e in the guard of t, then e \in S
* if x is not reset in t, then comp_expressions p l' c \subset S * if x is not reset in t, then comp_expressions p l' c \subset S
* returns a pair (L,U) * returns a pair (L,U)
* NB: the compExpr arrays are initialized by the function build_lu.
*) *)
let comp_expressions ta p l c = let comp_expressions ta p l c =
ta.procs.(p).procLocations.(l).compExpr.(c) ta.procs.(p).procLocations.(l).compExpr.(c)
...@@ -695,6 +696,39 @@ struct ...@@ -695,6 +696,39 @@ struct
| ClockArray(a,_) -> (*TODO*) failwith "cannot compute bounds for arrays of clocks" | ClockArray(a,_) -> (*TODO*) failwith "cannot compute bounds for arrays of clocks"
| _ -> [] | _ -> []
(* a non-recursive constant evaluation *)
let flat_constant_eval ta = function
| ConstVariable id ->
assert(id >= 0 && id < Array.length ta.constvalues);
Constant ta.constvalues.(id)
| ClockArray (a, l) when List.for_all (function | Constant _ -> true | _ -> false) l ->
let cellindex = VarContext.index_of_cell ta.clocks a (List.map (function Constant k -> k) l) in
Clock cellindex
| Array (a, l) when List.for_all (function | Constant _ -> true | _ -> false) l ->
let cellindex = VarContext.index_of_cell ta.vars a (List.map (function Constant k -> k) l) in
Variable cellindex
| ConstArray (a, l) when List.for_all (function | Constant _ -> true | _ -> false) l ->
let cellindex = VarContext.index_of_cell ta.constants a (List.map (function Constant k -> k) l) in
Constant ta.constvalues.(cellindex)
| _ as e -> e
let rec constant_eval ta = function
| ClockArray (a, l) ->
flat_constant_eval ta (ClockArray (a, List.map (constant_eval ta) l))
| Array (a, l) ->
flat_constant_eval ta (Array (a, List.map (constant_eval ta) l))
| ConstArray (a, l) ->
flat_constant_eval ta (ConstArray (a, List.map (constant_eval ta) l))
| Sum (e1, e2) ->
flat_constant_eval ta (Sum (constant_eval ta e1, constant_eval ta e2))
| Product (e1, e2) ->
flat_constant_eval ta (Product (constant_eval ta e1, constant_eval ta e2))
| Substraction (e1, e2) ->
flat_constant_eval ta (Substraction (constant_eval ta e1, constant_eval ta e2))
| Division (e1, e2) ->
flat_constant_eval ta (Division (constant_eval ta e1, constant_eval ta e2))
| _ as e -> flat_constant_eval ta e
(* compute all the local LU bounds *) (* compute all the local LU bounds *)
let build_lu ta = let build_lu ta =
let nclocks = VarContext.size ta.clocks in let nclocks = VarContext.size ta.clocks in
...@@ -804,8 +838,25 @@ struct ...@@ -804,8 +838,25 @@ struct
end end
done done
) loc.locEdges ) loc.locEdges
done done (* location loop *)
done done; (* fixpoint loop *)
(* We try to simplify the sets of expressions
* i.e. do constant propagation.
* TODO we should also remove duplicates if any
*)
(* for each location *)
for l=0 to (Array.length proc.procLocations)-1 do
let loc = proc.procLocations.(l) in
(* for each clock *)
for cl=0 to nclocks-1 do
let lcur, ucur = loc.compExpr.(cl) in
let lnew = List.map (constant_eval ta) lcur
and unew = List.map (constant_eval ta) ucur
in
loc.compExpr.(cl) <- lnew, unew;
done (* clock loop *)
done (* location loop *)
done done
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment