Skip to content
Snippets Groups Projects
Commit bb6b76d9 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

The -exec mode now supports partial assignment of arrays (a[i]=...).

parent 50541ca9
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/socExecEvalPredef.ml
+ 42
− 42
View file @ bb6b76d9
(* Time-stamp: <modified the 19/03/2013 (at 14:40) by Erwan Jahier> *)
(* Time-stamp: <modified the 20/03/2013 (at 17:25) by Erwan Jahier> *)
open SocExecValue
open Soc
......@@ -7,59 +7,59 @@ open Soc
let (lustre_plus : ctx -> ctx) =
fun ctx ->
let ns =
let (vn,vv) =
match [get_val "x" ctx; get_val "y" ctx] with
| [I x1; I x2] -> "z"::ctx.cpath,I(x1+x2)
| [F i1; F i2] -> "z"::ctx.cpath,F(i1+.i2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_times ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [I x1; I x2] -> "z"::ctx.cpath,I(x1 * x2)
| [F x1; F x2] -> "z"::ctx.cpath,F(x1 *. x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_div ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [I x1; I x2] -> "z"::ctx.cpath,I(x1 / x2)
| [F x1; F x2] -> "z"::ctx.cpath,F(x1 /. x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_minus ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [I x1; I x2] -> "z"::ctx.cpath,I(x1 - x2)
| [F x1; F x2] -> "z"::ctx.cpath,F(x1 -. x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_mod ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [I x1; I x2] -> "z"::ctx.cpath,I(x1 mod x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_eq ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [I x1; I x2] -> "z"::ctx.cpath,B(x1 = x2)
| [F x1; F x2] -> "z"::ctx.cpath,B(x1 = x2)
......@@ -67,129 +67,129 @@ let lustre_eq ctx =
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_uminus ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx]) with
| [I x1] -> "z"::ctx.cpath,I(- x1)
| [F x1] -> "z"::ctx.cpath,F(-. x1)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_real2int ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx]) with
| [F x1] -> "z"::ctx.cpath,I(int_of_float x1)
| [U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_int2real ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx]) with
| [I x1] -> "z"::ctx.cpath,F(float_of_int x1)
| [U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_not ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx]) with
| [B x1] -> "z"::ctx.cpath,B(not x1)
| [U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_lt ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [I x1; I x2] -> "z"::ctx.cpath,B(x1 < x2)
| [F x1; F x2] -> "z"::ctx.cpath,B(x1 < x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_gt ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [I x1; I x2] -> "z"::ctx.cpath,B(x1 > x2)
| [F x1; F x2] -> "z"::ctx.cpath,B(x1 > x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_lte ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [I x1; I x2] -> "z"::ctx.cpath,B(x1 <= x2)
| [F x1; F x2] -> "z"::ctx.cpath,B(x1 <= x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_gte ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [I x1; I x2] -> "z"::ctx.cpath,B(x1 >= x2)
| [F x1; F x2] -> "z"::ctx.cpath,B(x1 >= x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_and ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [B x1; B x2] -> "z"::ctx.cpath,B(x1 && x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_neq ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [B x1; B x2] -> "z"::ctx.cpath,B(x1 <> x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_or ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [B x1; B x2] -> "z"::ctx.cpath,B(x1 || x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_impl ctx =
let ns =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
| [B x1; B x2] -> "z"::ctx.cpath,B(not x1 or x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_if ctx =
let ns =
let (vn,vv) =
match ([get_val "c" ctx; get_val "xt" ctx; get_val "xe" ctx]) with
| [B c; I x1; I x2] -> "z"::ctx.cpath,I(if c then x1 else x2)
| [B c; F x1; F x2] -> "z"::ctx.cpath,F(if c then x1 else x2)
......@@ -203,14 +203,14 @@ let lustre_if ctx =
| [U;_; _] | [_;U;U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
let lustre_hat tl ctx =
let i = match tl with
| [_;Soc.Array(_,i)] -> i
| _ -> assert false
in
let ns =
let (vn,vv) =
match ([get_val "x" ctx]) with
| [B x] -> "z"::ctx.cpath,A(Array.make i (B x))
| [I x] -> "z"::ctx.cpath,A(Array.make i (I x))
......@@ -219,12 +219,12 @@ let lustre_hat tl ctx =
| [U] -> "z"::ctx.cpath,U
| _ -> assert false
in
{ ctx with s = sadd ctx.s ns }
{ ctx with s = sadd ctx.s vn vv }
(* That one is different *)
let lustre_xor ctx = assert false
let lustre_diese ctx = assert false
(* let ns = *)
(* let (vn,vv) = *)
(* let values = [get_val "x" ctx; get_val "y" ctx] in *)
(* let l = List.filter (fun x -> x=B true) values in *)
(* "z"::ctx.cpath,B(List.length l = 1) *)
......
src/socExecValue.ml
+ 97
− 7
View file @ bb6b76d9
(* Time-stamp: <modified the 19/03/2013 (at 18:03) by Erwan Jahier> *)
(* Time-stamp: <modified the 20/03/2013 (at 17:27) by Erwan Jahier> *)
open Soc
......@@ -15,6 +15,14 @@ let (path_to_string: ident list -> string) =
type subst = (path * t)
(* soc environnement holding memory values.
Each soc have a list of memories, which is actually a list of soc
instances (in the licc terminology).
Hence we need a kind of mapping from instance list (the path in the
call tree) to values.
*)
(* type substs = subst list *)
type substs =
| Node of (ident * substs) list
......@@ -25,12 +33,90 @@ type ctx = {
s:substs;
}
(**************************************************************************)
let rec (get_top_var_type : Soc.var_expr -> Soc.var_type) =
fun ve ->
match ve with
| Var(_,vt) -> vt
| Index(ve,_,_)
| Field(ve, _) -> get_top_var_type ve
| Const(id,_) -> assert false
type access = Idx of int | Fld of ident
let rec (get_access : Soc.var_expr -> access list) =
fun ve ->
match ve with
| Var(id,_) -> []
| Index(ve,i,_) -> (Idx i)::(get_access ve)
| Field(ve, (n,_)) -> (Fld n)::(get_access ve)
| Const(id,_) -> assert false
let rec (update_val : t -> t -> access list -> t) =
fun pre_v v access ->
(* Replace access(pre_v) by v in pre_v *)
match pre_v,access with
| _,[] -> v
| A a, (Idx i)::access ->
let a_i = update_val a.(i) v access in
a.(i) <- a_i;
A a
| _,_ -> assert false (* finish me (field struct) *)
let (update_leaf : var_expr -> t -> t -> substs) =
fun ve v pre_v ->
let access = get_access ve in
let new_v = update_val pre_v v access in
Leaf(new_v)
let rec (create_val : Soc.var_type -> t -> access list -> t) =
fun vt v access ->
(* The same as update in the case where no previous value exists *)
match vt,access with
| _,[] -> v
| Array(vt,size), (Idx i)::access ->
let a = Array.make size U in
let a_i = create_val vt v access in
a.(i) <- a_i;
A a
| _,_ -> assert false (* finish me (field struct) *)
let (create_leaf : var_expr -> t -> substs) =
fun ve v ->
let access = get_access ve in
let top_vt = get_top_var_type ve in
let new_v = create_val top_vt v access in
Leaf(new_v)
(* should be able to replace sadd actually *)
let (sadd_partial : substs -> var_expr -> path -> t -> substs) =
fun ct ve x v ->
(* update ct by associating x::ve to v in ct ; *)
let rec aux ct (x,v) =
match ct,x with
| Leaf(pre_v),[] -> update_leaf ve v pre_v
| Node(l),n::t -> (
try
let s = aux (List.assoc n l) (t,v) in
Node((n,s)::(List.remove_assoc n l))
with Not_found ->
if t = [] then Node((n, create_leaf ve v)::l)
else
let new_substs = aux (Node []) (t,v) in
Node((n,new_substs)::l)
)
| _,[] -> assert false
| Leaf(_),_ -> assert false
in
aux ct (List.rev x,v)
(* let rec (sadd : substs -> subst -> substs) = *)
(* fun ct (x,v) -> *)
(* (x,v)::(List.remove_assoc x ct) *)
let (sadd : substs -> subst -> substs) =
fun ct (x,v) ->
let (sadd : substs -> path -> t -> substs) =
fun ct x v ->
let rec aux ct (x,v) =
match ct,x with
| Leaf(_),[] -> Leaf(v)
......@@ -49,6 +135,10 @@ let (sadd : substs -> subst -> substs) =
in
aux ct (List.rev x,v)
(**************************************************************************)
(* let filter_top_subst s = *)
(* List.fold_left *)
(* (fun acc (idl,v) -> *)
......@@ -219,7 +309,7 @@ let (substitute_args_and_params : var_expr list -> var list -> ctx -> substs) =
assert (List.length args = List.length params);
let arg_ctx = { ctx with cpath = List.tl ctx.cpath } in
let s = List.map2 (fun arg (pn,_) -> pn::ctx.cpath, get_value arg_ctx arg) args params in
let s = List.fold_left sadd ctx.s s in
let s = List.fold_left (fun acc (vn,vv) -> sadd acc vn vv) ctx.s s in
s
let (substitute_params_and_args : var list -> var_expr list -> ctx -> substs) =
......@@ -233,7 +323,7 @@ let (substitute_params_and_args : var list -> var_expr list -> ctx -> substs) =
)
args params
in
let s = List.fold_left sadd ctx.s s in
let s = List.fold_left (fun acc (vn,vv) -> sadd acc vn vv) ctx.s s in
s
let empty_ctx: ctx = {
......@@ -251,11 +341,11 @@ let rec (create_ctx : Soc.tbl -> Soc.t -> ctx) =
| Some(vt, Some(value)) ->
let name = (SocPredef.get_mem_name soc.key vt)::cpath in
let value = get_value empty_ctx value in
sadd mem (name,value)
sadd mem name value
| Some(vt, None) ->
let name = (SocPredef.get_mem_name soc.key vt)::cpath in
let value = U in
sadd mem (name,value)
sadd mem name value
| None -> mem
in
List.fold_left (init_instances cpath) mem soc.instances
......
src/socExecValue.mli
+ 14
− 6
View file @ bb6b76d9
(* Time-stamp: <modified the 19/03/2013 (at 16:16) by Erwan Jahier> *)
(* Time-stamp: <modified the 20/03/2013 (at 17:23) by Erwan Jahier> *)
(** Manipulating data in the Soc interpreter *)
type t = | I of int | F of float | B of bool | E of Soc.ident | A of t array
| U (* to set uninitialized mem *)
type subst = (Soc.ident list * t)
type path = Soc.ident list
type subst = (path * t)
(* Not really a good name anymore. Memory ? *)
type substs
(* = *)
(* | Node of (Soc.ident * substs) list *)
(* | Leaf of t *)
val sadd : substs -> subst -> substs
(* update the memory. The path correspond to a path in the call tree,
except the last ident that is the variable name we want to
associate a value to.
*)
val sadd : substs -> path -> t -> substs
(* ditto, but in the case of a partial assignment (e.g., a[i] = something). *)
val sadd_partial : substs -> Soc.var_expr -> path -> t -> substs
type ctx = {
......
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