From acc2dbb3a79f2ba9ed0489bd8bff1bfc31846d4b Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Tue, 27 Jun 2017 14:41:45 +0200
Subject: [PATCH] soc2c: the generated C code for '=' and '<>' was wrong in
presence of arrays.
I've fixed that using memcmp, which should be fine since compared elements
are of the same types.
---
_oasis | 2 +-
src/lv6version.ml | 4 +-
src/main.ml | 4 +-
src/soc2c.ml | 25 ++++-
src/soc2cDep.mli | 4 +-
src/soc2cExtern.ml | 6 +-
src/soc2cHeap.ml | 21 ++--
src/soc2cHeap.mli | 4 +-
src/soc2cPredef.ml | 160 +++++++++++++++++----------
src/soc2cPredef.mli | 6 +-
src/soc2cStack.ml | 23 ++--
src/soc2cStack.mli | 4 +-
src/soc2cUtil.ml | 2 +-
src/socPredef2cHeap.ml | 31 +++++-
src/socPredef2cStack.ml | 28 ++++-
test/lus2lic.sum | 40 ++++---
test/should_work/array_equals.lus | 4 +
test/should_work/struct_equality.lus | 10 ++
utils/compare_exec_and_2c | 2 +-
19 files changed, 253 insertions(+), 127 deletions(-)
create mode 100644 test/should_work/struct_equality.lus
diff --git a/_oasis b/_oasis
index 76579496..03ad8c59 100644
--- a/_oasis
+++ b/_oasis
@@ -1,6 +1,6 @@
OASISFormat: 0.4
Name: lustre-v6
-Version: 1.699
+Version: 1.700
Synopsis: The Lustre V6 Verimag compiler
Description: This package contains:
(1) lus2lic: the (current) name of the compiler (and interpreter via -exec).
diff --git a/src/lv6version.ml b/src/lv6version.ml
index d78ce7fc..42d29581 100644
--- a/src/lv6version.ml
+++ b/src/lv6version.ml
@@ -1,7 +1,7 @@
(** Automatically generated from Makefile *)
let tool = "lus2lic"
let branch = "master"
-let commit = "699"
-let sha_1 = "e74551e8ee5b3ea2eb120c2bfcaea92ca8940c9e"
+let commit = "700"
+let sha_1 = "fd3bc9566365dd3042af3302ecab8e9311e76e2d"
let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
let maintainer = "jahier@imag.fr"
diff --git a/src/main.ml b/src/main.ml
index eb61eb00..2f30d2cb 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 19/10/2016 (at 16:28) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/06/2017 (at 14:26) by Erwan Jahier> *)
open Lv6Verbose
open AstV6
@@ -229,7 +229,7 @@ let
res = if x < 0.0 then -x else x;
tel
-const seuil = 0.0001;
+const seuil = 0.01;
node r_equal(x,y:real) returns (res:bool);
let
res = if r_abs(x)>1.0 then r_abs(1.0-(y/x)) < seuil else r_abs(x-y) < seuil;
diff --git a/src/soc2c.ml b/src/soc2c.ml
index cf62cccb..f10272e1 100644
--- a/src/soc2c.ml
+++ b/src/soc2c.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 01/06/2017 (at 16:12) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/06/2017 (at 11:37) by Erwan Jahier> *)
(* let put (os: out_channel) (fmt:('a, unit, string, unit) format4) : 'a = *)
@@ -110,12 +110,31 @@ let (step2c : Soc.tbl -> 'a soc_pp -> Soc.step_method -> unit) =
(* let sname = Soc2cDep.step_name sp.soc.key sm.name in *)
let sname = Soc2cDep.step_name sp.soc.key sm.name in
if sm.impl<>Extern then (
- let decl, def = Soc2cDep.get_step_prototype sm sp.soc in
+ let decl, def, ctype = Soc2cDep.get_step_prototype sm sp.soc in
sp.hput (Printf.sprintf "%s\n" decl);
sp.cput (Printf.sprintf "%s" def);
(match sm.impl with
| Extern -> ()
- | Predef -> sp.cput (Soc2cDep.get_predef_op sp.soc.key)
+ | Predef ->
+ (match sp.soc.key with
+ | ("Lustre::eq",(Array _)::_,_) ->
+ let str = Printf.sprintf
+ " *out = memcmp((const void *) i1, (const void *) i2, %s)!=0;\n" ctype in
+ sp.cput str
+ | ("Lustre::eq",(Struct _)::_,_) ->
+ let str = Printf.sprintf
+ " *out = memcmp((const void *) &i1, (const void *) &i2, %s)!=0;\n" ctype in
+ sp.cput str
+ | ("Lustre::neq",(Array _)::_,_) ->
+ let str = Printf.sprintf
+ " *out = !memcmp((const void *) i1, (const void *) i2, %s)!=0;\n" ctype in
+ sp.cput str
+ | ("Lustre::neq",(Struct _)::_,_) ->
+ let str = Printf.sprintf
+ " *out = !memcmp((const void *) &i1, (const void *) &i2, %s)!=0;\n" ctype in
+ sp.cput str
+ | n -> sp.cput (Soc2cDep.get_predef_op n)
+ )
| Gaol(vl, gaol) -> (
if Lv6MainArgs.global_opt.Lv6MainArgs.gen_wcet then
List.iter
diff --git a/src/soc2cDep.mli b/src/soc2cDep.mli
index 6e4aeddd..a2637d99 100644
--- a/src/soc2cDep.mli
+++ b/src/soc2cDep.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 06/10/2016 (at 17:28) by Erwan Jahier> *)
+(* Time-stamp: <modified the 26/06/2017 (at 16:39) by Erwan Jahier> *)
(** Choose between the various C code generators (heap-based, Stack
@@ -20,7 +20,7 @@ val step_name : Soc.key -> string -> string
"void step(ctx_type, int, int, int* );",
"void step(ctx_type ctx, int x, int y,int* z){",
*)
-val get_step_prototype : Soc.step_method -> Soc.t -> string * string
+val get_step_prototype : Soc.step_method -> Soc.t -> string * string * string
val string_of_var_expr: Soc.t -> Soc.var_expr -> string
diff --git a/src/soc2cExtern.ml b/src/soc2cExtern.ml
index b9f12dbd..c41a065e 100644
--- a/src/soc2cExtern.ml
+++ b/src/soc2cExtern.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 05/05/2017 (at 14:14) by Erwan Jahier> *)
+(* Time-stamp: <modified the 26/06/2017 (at 16:39) by Erwan Jahier> *)
open Soc2cIdent
@@ -141,7 +141,7 @@ let (gen_files : Soc.t -> Soc.tbl -> LicPrg.t -> string -> string -> string ->
List.iter (fun (sm,soc) ->
let sname = Soc2cDep.step_name soc.key sm.name in
- let proto_decl,_ = Soc2cDep.get_step_prototype sm soc in
+ let proto_decl,_,_ = Soc2cDep.get_step_prototype sm soc in
output_string ext_och proto_decl;
) extern_steps;
close_out ext_och;
@@ -156,7 +156,7 @@ let (gen_files : Soc.t -> Soc.tbl -> LicPrg.t -> string -> string -> string ->
output_string ext_occ (const_def licprg);
List.iter (fun (sm,soc) ->
let sname = Soc2cDep.step_name soc.key sm.name in
- let _,proto_begin = Soc2cDep.get_step_prototype sm soc in
+ let _,proto_begin,_ = Soc2cDep.get_step_prototype sm soc in
output_string ext_occ proto_begin;
output_string ext_occ (Printf.sprintf " /* finish me! */\n}\n")
) extern_steps;
diff --git a/src/soc2cHeap.ml b/src/soc2cHeap.ml
index 50899fc1..197a0b4e 100644
--- a/src/soc2cHeap.ml
+++ b/src/soc2cHeap.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 23/06/2017 (at 13:57) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/06/2017 (at 11:27) by Erwan Jahier> *)
open Soc2cUtil
open Soc2cIdent
@@ -99,17 +99,15 @@ let (inline_soc :
(String.concat " " le)^ " }\n"
in
Some str
- | "Lustre::diff" -> assert false
- | "Lustre::equal" -> assert false
| _ ->
try
if
Lv6MainArgs.global_opt.Lv6MainArgs.gen_c_inline_predef
- && Soc2cPredef.is_call_supported called_soc_name
+ && Soc2cPredef.is_call_supported called_soc.key
then
let vel_in = List.map (string_of_var_expr soc) vel_in in
let vel_out = List.map (string_of_var_expr soc) vel_out in
- Some (Soc2cPredef.gen_call called_soc_name soc vel_out vel_in)
+ Some (Soc2cPredef.gen_call called_soc.key soc vel_out vel_in)
else
None
with Not_found ->
@@ -119,7 +117,7 @@ let (inline_soc :
let (inlined_soc : Soc.key -> bool) =
fun key ->
let soc_name,_,_ = key in
- soc_name = "Lustre::if" || Soc2cPredef.is_call_supported soc_name
+ soc_name = "Lustre::if" || Soc2cPredef.is_call_supported key
(* exported *)
@@ -189,7 +187,7 @@ let (typedef_of_soc : Soc.t -> string) =
let str = Printf.sprintf "%s} %s;\n\n" str ctx_name_type in
str
-let (get_step_prototype : Soc.step_method -> Soc.t -> string * string) =
+let (get_step_prototype : Soc.step_method -> Soc.t -> string * string * string) =
fun sm soc ->
let sname = step_name soc.key sm.name in
let ctx = if SocUtils.is_memory_less soc then "" else
@@ -198,5 +196,12 @@ let (get_step_prototype : Soc.step_method -> Soc.t -> string * string) =
let ctx_decl = if SocUtils.is_memory_less soc then "" else
Printf.sprintf "%s_type*" (get_ctx_name soc.key)
in
+ let inputs, _ = soc.Soc.profile in
+ let ctype = match inputs with
+ | (_,t)::_ ->
+ Printf.sprintf "sizeof(%s)" (Soc2cUtil.data_type_to_c t "")
+ | [] -> "" (* soc without intputs won't need this output *)
+ in
Printf.sprintf "void %s(%s);\n" sname ctx_decl,
- Printf.sprintf "void %s(%s){\n" sname ctx
+ Printf.sprintf "void %s(%s){\n" sname ctx,
+ ctype
diff --git a/src/soc2cHeap.mli b/src/soc2cHeap.mli
index 5af3a1b4..53a6d726 100644
--- a/src/soc2cHeap.mli
+++ b/src/soc2cHeap.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 06/10/2016 (at 17:29) by Erwan Jahier> *)
+(* Time-stamp: <modified the 26/06/2017 (at 16:41) by Erwan Jahier> *)
(** Gathers all entities (functions, types) that implement the
heap-based C generator. *)
@@ -13,7 +13,7 @@ val gen_assign_var_expr : Soc.t -> Soc.var_expr -> Soc.var_expr -> string
(* Generates the C step name from the soc key and the soc step name *)
val step_name : Soc.key -> string -> string
-val get_step_prototype : Soc.step_method -> Soc.t -> string * string
+val get_step_prototype : Soc.step_method -> Soc.t -> string * string * string
val string_of_var_expr: Soc.t -> Soc.var_expr -> string
diff --git a/src/soc2cPredef.ml b/src/soc2cPredef.ml
index 8c4152a8..7bb3fb8a 100644
--- a/src/soc2cPredef.ml
+++ b/src/soc2cPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 06/10/2016 (at 17:32) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/06/2017 (at 14:40) by Erwan Jahier> *)
(* A local exception used to check if a predef is supported.
The idea is that when gen_call_do is called with empty lists,
@@ -9,12 +9,42 @@
*)
exception Is_supported
-let stdbin op ll rl =
+let stdbin op ll rl =
match (ll,rl) with
| ([l], [r1;r2]) -> Printf.sprintf " %s = %s %s %s;\n" l r1 op r2
| ([],[]) -> raise Is_supported
| _ -> assert false
+(* to deal with == and <> over arrays *)
+let stdbin_eq_array is_eq (op,tl,_) ll rl =
+ let cast = "(const void *)" in
+ let ctype = match tl with
+ | t::_ -> Printf.sprintf "sizeof(%s)" (Soc2cUtil.data_type_to_c t "")
+ | [] -> assert false
+ in
+ let not_opt = if is_eq then "" else "!" in
+ match (ll,rl) with
+ | ([l], [r1;r2]) ->
+ Printf.sprintf " %s = %smemcmp(%s %s, %s %s, %s)!=0;\n"
+ l not_opt cast r1 cast r2 ctype
+ | ([],[]) -> raise Is_supported
+ | _ -> assert false
+
+(* to deal with == and <> over structs *)
+let stdbin_eq_struct is_eq (op,tl,_) ll rl =
+ let cast = "(const void *)" in
+ let ctype = match tl with
+ | t::_ -> Printf.sprintf "sizeof(%s)" (Soc2cUtil.data_type_to_c t "")
+ | [] -> assert false
+ in
+ let not_opt = if is_eq then "" else "!" in
+ match (ll,rl) with
+ | ([l], [r1;r2]) ->
+ Printf.sprintf " %s = %smemcmp(%s &%s, %s &%s, %s)!=0;\n"
+ l not_opt cast r1 cast r2 ctype
+ | ([],[]) -> raise Is_supported
+ | _ -> assert false
+
let stduna op ll rl =
match (ll,rl) with
| ([l], [r]) -> Printf.sprintf " %s = %s %s;\n" l op r
@@ -30,65 +60,77 @@ let stdimpl ll rl =
(* exported *)
(* ZZZ code dupl with SocPredef2cHeap.get_predef_op *)
-let (gen_call_do : string -> string list -> string list -> string) =
- fun op vel_in vel_out ->
- let lstduna str = stduna str vel_in vel_out in
- let lstdbin str = stdbin str vel_in vel_out in
- let lstdimpl () = stdimpl vel_in vel_out in
- match op with
- | "Lustre::uminus" -> lstduna "-"
- | "Lustre::iuminus" -> lstduna "-"
- | "Lustre::ruminus" -> lstduna "-"
- | "Lustre::not" -> lstduna "!"
-
- | "Lustre::mod" -> lstdbin "%"
- | "Lustre::plus" -> lstdbin "+"
- | "Lustre::iplus" -> lstdbin "+"
- | "Lustre::rplus" -> lstdbin "+"
- | "Lustre::times" -> lstdbin "*"
- | "Lustre::itimes" -> lstdbin "*"
- | "Lustre::rtimes" -> lstdbin "*"
- | "Lustre::div" -> lstdbin "/"
- | "Lustre::idiv" -> lstdbin "/"
- | "Lustre::rdiv" -> lstdbin "/"
- | "Lustre::minus" -> lstdbin "-"
- | "Lustre::iminus" -> lstdbin "-"
- | "Lustre::rminus" -> lstdbin "-"
-
- | "Lustre::real2int" -> lstduna "(_integer)"
- | "Lustre::int2real" -> lstduna "(_real)"
-
- | "Lustre::lt" -> lstdbin "<"
- | "Lustre::ilt" -> lstdbin "<"
- | "Lustre::rlt" -> lstdbin "<"
- | "Lustre::gt" -> lstdbin ">"
- | "Lustre::igt" -> lstdbin ">"
- | "Lustre::rgt" -> lstdbin ">"
- | "Lustre::lte" -> lstdbin "<="
- | "Lustre::ilte"-> lstdbin "<="
- | "Lustre::rlte"-> lstdbin "<="
- | "Lustre::gte" -> lstdbin ">="
- | "Lustre::igte"-> lstdbin ">="
- | "Lustre::rgte"-> lstdbin ">="
-
- | "Lustre::and" -> lstdbin "&"
- | "Lustre::or" -> lstdbin "|"
- | "Lustre::xor" -> lstdbin "!="
- | "Lustre::impl" -> lstdimpl ()
-
- | "Lustre::equal" -> lstdbin "=="
- | "Lustre::diff" -> lstdbin "!="
-
- | _ -> raise Not_found
-
-let (gen_call : string -> Soc.t -> string list -> string list -> string) =
- fun op soc vel_in vel_out ->
+let (gen_call_do : Soc.key -> string list -> string list -> string) =
+ fun sk vel_in vel_out ->
+ let (op,tl,_) = sk in
+ let lstduna str = stduna str vel_in vel_out in
+ let lstdbin str = stdbin str vel_in vel_out in
+ let lstdimpl () = stdimpl vel_in vel_out in
+ match sk with
+ | "Lustre::uminus",_,_ -> lstduna "-"
+ | "Lustre::iuminus",_,_ -> lstduna "-"
+ | "Lustre::ruminus",_,_ -> lstduna "-"
+ | "Lustre::not",_,_ -> lstduna "!"
+
+ | "Lustre::mod",_,_ -> lstdbin "%"
+ | "Lustre::plus",_,_ -> lstdbin "+"
+ | "Lustre::iplus",_,_ -> lstdbin "+"
+ | "Lustre::rplus",_,_ -> lstdbin "+"
+ | "Lustre::times",_,_ -> lstdbin "*"
+ | "Lustre::itimes",_,_ -> lstdbin "*"
+ | "Lustre::rtimes",_,_ -> lstdbin "*"
+ | "Lustre::div",_,_ -> lstdbin "/"
+ | "Lustre::idiv",_,_ -> lstdbin "/"
+ | "Lustre::rdiv",_,_ -> lstdbin "/"
+ | "Lustre::minus",_,_ -> lstdbin "-"
+ | "Lustre::iminus",_,_ -> lstdbin "-"
+ | "Lustre::rminus",_,_ -> lstdbin "-"
+
+ | "Lustre::real2int",_,_ -> lstduna "(_integer)"
+ | "Lustre::int2real",_,_ -> lstduna "(_real)"
+
+ | "Lustre::lt",_,_ -> lstdbin "<"
+ | "Lustre::ilt",_,_ -> lstdbin "<"
+ | "Lustre::rlt",_,_ -> lstdbin "<"
+ | "Lustre::gt",_,_ -> lstdbin ">"
+ | "Lustre::igt",_,_ -> lstdbin ">"
+ | "Lustre::rgt",_,_ -> lstdbin ">"
+ | "Lustre::lte",_,_ -> lstdbin "<="
+ | "Lustre::ilte",_,_-> lstdbin "<="
+ | "Lustre::rlte",_,_-> lstdbin "<="
+ | "Lustre::gte",_,_ -> lstdbin ">="
+ | "Lustre::igte",_,_-> lstdbin ">="
+ | "Lustre::rgte",_,_-> lstdbin ">="
+
+ | "Lustre::and",_,_ -> lstdbin "&"
+ | "Lustre::or",_,_ -> lstdbin "|"
+ | "Lustre::xor",_,_ -> lstdbin "!="
+ | "Lustre::impl",_,_ -> lstdimpl ()
+
+ | (("Lustre::eq"|"Lustre::equal"),(Array _)::_,_) ->
+ stdbin_eq_array true sk vel_in vel_out
+ | (("Lustre::neq"|"Lustre::diff"),(Array _)::_,_) ->
+ stdbin_eq_array false sk vel_in vel_out
+ | (("Lustre::eq"|"Lustre::equal"),(Struct _)::_,_)->
+ stdbin_eq_struct true sk vel_in vel_out
+ | (("Lustre::neq"|"Lustre::diff"),(Struct _)::_,_)->
+ stdbin_eq_struct false sk vel_in vel_out
+
+ | "Lustre::eq",_,_ -> lstdbin "=="
+ | "Lustre::equal",_,_ -> lstdbin "=="
+ | "Lustre::neq",_,_ -> lstdbin "!="
+ | "Lustre::diff",_,_ -> lstdbin "!="
+
+ | _ -> raise Not_found
+
+let (gen_call : Soc.key -> Soc.t -> string list -> string list -> string) =
+ fun sk soc vel_in vel_out ->
assert ((vel_in,vel_out) <> ([],[]));
- gen_call_do op vel_in vel_out
+ gen_call_do sk vel_in vel_out
-let (is_call_supported : string -> bool) =
- fun op ->
- try ignore (gen_call_do op [] []); assert false (* sno *)
+let (is_call_supported : Soc.key -> bool) =
+ fun sk ->
+ try ignore (gen_call_do sk [] []); assert false (* sno *)
with
| Is_supported -> true
| Not_found -> false
diff --git a/src/soc2cPredef.mli b/src/soc2cPredef.mli
index f4aaeef6..a1d27e21 100644
--- a/src/soc2cPredef.mli
+++ b/src/soc2cPredef.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 06/10/2016 (at 17:32) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/06/2017 (at 11:10) by Erwan Jahier> *)
(* provides a direct definition to predefined arith operators.
@@ -6,6 +6,6 @@ raises Not_found if it is not used with such a predef op
*)
-val gen_call : string -> Soc.t -> string list -> string list -> string
+val gen_call : Soc.key -> Soc.t -> string list -> string list -> string
-val is_call_supported : string -> bool
+val is_call_supported : Soc.key -> bool
diff --git a/src/soc2cStack.ml b/src/soc2cStack.ml
index c827954f..21ae4437 100644
--- a/src/soc2cStack.ml
+++ b/src/soc2cStack.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 23/06/2017 (at 11:16) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/06/2017 (at 11:28) by Erwan Jahier> *)
open Soc2cUtil
open Soc2cIdent
@@ -137,14 +137,12 @@ let (inline_soc: Soc.t -> Soc.t -> Soc.var_expr list -> Soc.var_expr list ->
(String.concat " " le)^ " }\n"
in
Some str
- | "Lustre::diff" -> assert false
- | "Lustre::equal" -> assert false
| _ ->
try
if
Lv6MainArgs.global_opt.Lv6MainArgs.gen_c_inline_predef
- && Soc2cPredef.is_call_supported called_soc_name
+ && Soc2cPredef.is_call_supported called_soc.key
then
let vel_in_str = List.map (string_of_var_expr soc) vel_in in
let vel_in = List.map2
@@ -157,7 +155,7 @@ let (inline_soc: Soc.t -> Soc.t -> Soc.var_expr list -> Soc.var_expr list ->
(fun v s -> if is_soc_output v soc && ve_not_an_array v
then "*"^s else s) vel_out vel_out_str
in
- Some (Soc2cPredef.gen_call called_soc_name soc vel_out vel_in)
+ Some (Soc2cPredef.gen_call called_soc.key soc vel_out vel_in)
else
None
with Not_found ->
@@ -167,7 +165,7 @@ let (inline_soc: Soc.t -> Soc.t -> Soc.var_expr list -> Soc.var_expr list ->
let (inlined_soc : Soc.key -> bool) =
fun key ->
let soc_name,_,_ = key in
- soc_name = "Lustre::if" || Soc2cPredef.is_call_supported soc_name
+ soc_name = "Lustre::if" || Soc2cPredef.is_call_supported key
(* exported *)
@@ -229,7 +227,7 @@ let (typedef_of_soc : Soc.t -> string) =
"void step(int x, int y, int* res, soc_ctx_type* ctx){"
*)
-let (get_step_prototype : Soc.step_method -> Soc.t -> string * string) =
+let (get_step_prototype : Soc.step_method -> Soc.t -> string * string * string) =
fun sm soc ->
let sname = step_name soc.key sm.name in
let inputs, outputs = soc.Soc.profile in
@@ -254,11 +252,18 @@ let (get_step_prototype : Soc.step_method -> Soc.t -> string * string) =
let out_params_decl = List.map (to_param_decl true) outputs in
let params = String.concat "," (in_params@out_params) in
let params_decl = String.concat "," (in_params_decl@out_params_decl) in
+ let ctype = match inputs with
+ | (_,t)::_ ->
+ Printf.sprintf "sizeof(%s)" (Soc2cUtil.data_type_to_c t "")
+ | [] -> "" (* soc without intputs won't need this output *)
+ in
if SocUtils.is_memory_less soc then
Printf.sprintf "void %s(%s);\n" sname params_decl,
- Printf.sprintf "void %s(%s){\n" sname params
+ Printf.sprintf "void %s(%s){\n" sname params,
+ ctype
else
let ctx = Printf.sprintf "%s_type* ctx" (get_ctx_name soc.key) in
let ctx_decl = Printf.sprintf "%s_type*" (get_ctx_name soc.key) in
Printf.sprintf "void %s(%s,%s);\n" sname params_decl ctx_decl,
- Printf.sprintf "void %s(%s,%s){" sname params ctx
+ Printf.sprintf "void %s(%s,%s){" sname params ctx,
+ ctype
diff --git a/src/soc2cStack.mli b/src/soc2cStack.mli
index 44b7044d..0876d028 100644
--- a/src/soc2cStack.mli
+++ b/src/soc2cStack.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 06/10/2016 (at 17:28) by Erwan Jahier> *)
+(* Time-stamp: <modified the 26/06/2017 (at 16:41) by Erwan Jahier> *)
(** Gathers all entities (functions, types) that implement the
heap-based C generator. *)
@@ -21,7 +21,7 @@ val step_name : Soc.key -> string -> string
(** Returns the prototype (.c) and the decl (.h) of the step function.
For the stack based approach, we need to arg I/O params.
*)
-val get_step_prototype : Soc.step_method -> Soc.t -> string * string
+val get_step_prototype : Soc.step_method -> Soc.t -> string * string * string
val string_of_var_expr: Soc.t -> Soc.var_expr -> string
diff --git a/src/soc2cUtil.ml b/src/soc2cUtil.ml
index c121c7e2..0064d6ae 100644
--- a/src/soc2cUtil.ml
+++ b/src/soc2cUtil.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 21/11/2016 (at 17:03) by Erwan Jahier> *)
+(* Time-stamp: <modified the 26/06/2017 (at 17:00) by Erwan Jahier> *)
open Soc2cIdent
open Data
diff --git a/src/socPredef2cHeap.ml b/src/socPredef2cHeap.ml
index 44509b58..db4e51cf 100644
--- a/src/socPredef2cHeap.ml
+++ b/src/socPredef2cHeap.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 10/01/2017 (at 17:59) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/06/2017 (at 11:38) by Erwan Jahier> *)
open Data
open Soc
@@ -6,13 +6,30 @@ open Soc2cIdent
(* A boring but simple module... *)
-(* XXX should i use gen_assign here? for the time being, its useless as
- there is no binop (nor unop) over arrays.
-*)
let (lustre_binop : Soc.key -> string -> string) =
fun sk op ->
- let ctx = get_ctx_name sk in
- Printf.sprintf " %s.out = (%s.i1 %s %s.i2);\n" ctx ctx op ctx
+ let ctx = get_ctx_name sk in
+ let cast = "(const void *)" in
+ let ctype = match sk with
+ | _,t::_,_ -> Printf.sprintf "sizeof(%s)" (Soc2cUtil.data_type_to_c t "")
+ | _, [],_ -> assert false
+ in
+ (match sk with
+ | (("Lustre::eq"|"Lustre::equal"),(Array _)::_,_) ->
+ Printf.sprintf " %s.out = memcmp(%s %s.i1, %s %s.i2, %s)!=0;\n"
+ ctx ctx cast ctx cast ctype
+ | (("Lustre::eq"|"Lustre::equal"),(Struct _)::_,_) ->
+ Printf.sprintf " %s.out = memcmp(%s &%s.i1, %s &%s.i2, %s)!=0;\n"
+ ctx ctx cast ctx cast ctype
+ | (("Lustre::neq"|"Lustre::diff"),(Array _)::_,_) ->
+ Printf.sprintf " %s.out = !memcmp(%s %s.i1, %s %s.i2, %s)!=0;\n"
+ ctx ctx cast ctx cast ctype
+ | (("Lustre::neq"|"Lustre::diff"),(Struct _)::_,_) ->
+ Printf.sprintf " %s.out = !memcmp(%s &%s.i1, %s &%s.i2, %s)!=0;\n"
+ ctx ctx cast ctx cast ctype
+ | _ ->
+ Printf.sprintf " %s.out = (%s.i1 %s %s.i2);\n" ctx ctx op ctx
+ )
let (lustre_unop : Soc.key -> string -> string) =
fun sk op ->
@@ -155,9 +172,11 @@ let (get_predef_op: Soc.key -> string) =
| "Lustre::ruminus"-> lustre_unop sk "-"
| "Lustre::eq" -> lustre_binop sk "=="
+ | "Lustre::equal" -> lustre_binop sk "=="
| "Lustre::and" -> lustre_binop sk "&&"
| "Lustre::neq" -> lustre_binop sk "!="
+ | "Lustre::diff" -> lustre_binop sk "!="
| "Lustre::or" -> lustre_binop sk "||"
| "Lustre::xor" -> lustre_binop sk "!="
diff --git a/src/socPredef2cStack.ml b/src/socPredef2cStack.ml
index 8260a645..a2b2111d 100644
--- a/src/socPredef2cStack.ml
+++ b/src/socPredef2cStack.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 10/01/2017 (at 18:04) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/06/2017 (at 11:38) by Erwan Jahier> *)
open Data
open Soc
@@ -6,12 +6,26 @@ open Soc2cIdent
(* A boring but simple module... *)
-(* XXX should i use gen_assign here? for the time being, its useless as
- there is no binop (nor unop) over arrays.
-*)
let (lustre_binop : Soc.key -> string -> string) =
- fun sk op ->
- Printf.sprintf " *out = (i1 %s i2);\n" op
+ fun sk op ->
+ let cast = "(const void *)" in
+ let ctype = match sk with
+ | _,t::_,_ -> Printf.sprintf "sizeof(%s)" (Soc2cUtil.data_type_to_c t "")
+ | _, [],_ -> assert false
+ in
+ (match sk with
+ | (("Lustre::eq"|"Lustre::equal"),(Array _)::_,_) ->
+ Printf.sprintf " *out = memcmp(%s i1, %s i2, %s)!=0;\n" cast cast ctype
+ | (("Lustre::eq"|"Lustre::equal"),(Struct _)::_,_) ->
+ Printf.sprintf " *out = memcmp(%s &i1, %s &i2, %s)!=0;\n" cast cast ctype
+ | (("Lustre::neq"|"Lustre::diff"),(Array _)::_,_) ->
+ Printf.sprintf " *out = !memcmp(%s i1, %s i2, %s)!=0;\n" cast cast ctype
+ | (("Lustre::neq"|"Lustre::diff"),(Struct _)::_,_) ->
+ Printf.sprintf " *out = !memcmp(%s &i1, %s &i2, %s)!=0;\n" cast cast ctype
+
+ | _ ->
+ Printf.sprintf " *out = (i1 %s i2);\n" op
+ )
let (lustre_unop : Soc.key -> string -> string) =
fun sk op ->
@@ -160,9 +174,11 @@ let (get_predef_op: Soc.key -> string) =
| "Lustre::ruminus"-> lustre_unop sk "-"
| "Lustre::eq" -> lustre_binop sk "=="
+ | "Lustre::equal" -> lustre_binop sk "=="
| "Lustre::and" -> lustre_binop sk "&&"
| "Lustre::neq" -> lustre_binop sk "!="
+ | "Lustre::diff" -> lustre_binop sk "!="
| "Lustre::or" -> lustre_binop sk "||"
| "Lustre::xor" -> lustre_binop sk "!="
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index 0f056dd2..92485024 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,5 +1,5 @@
==> lus2lic0.sum <==
-Test Run By jahier on Fri Jun 23 10:28:36
+Test Run By jahier on Tue Jun 27 14:29:44
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic0 tests ===
@@ -64,7 +64,7 @@ XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/lecte
XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/s.lus
==> lus2lic1.sum <==
-Test Run By jahier on Fri Jun 23 10:28:36
+Test Run By jahier on Tue Jun 27 14:29:45
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic1 tests ===
@@ -401,7 +401,7 @@ PASS: sh multipar.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus {}
==> lus2lic2.sum <==
-Test Run By jahier on Fri Jun 23 10:29:29
+Test Run By jahier on Tue Jun 27 14:30:37
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic2 tests ===
@@ -621,6 +621,9 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c stopwatch.lus {}
PASS: ./lus2lic {-2c struct0.lus -n struct0}
PASS: sh struct0.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c struct0.lus {}
+PASS: ./lus2lic {-2c struct_equality.lus -n struct_equality}
+PASS: sh struct_equality.sh
+FAIL: Try to compare lus2lic -exec and -2c: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c struct_equality.lus {}
PASS: ./lus2lic {-2c struct_with.lus -n struct_with}
PASS: sh struct_with.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c struct_with.lus {}
@@ -741,7 +744,7 @@ PASS: sh zzz2.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c zzz2.lus {}
==> lus2lic3.sum <==
-Test Run By jahier on Fri Jun 23 10:30:40
+Test Run By jahier on Tue Jun 27 14:31:50
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic3 tests ===
@@ -1249,7 +1252,7 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {}
==> lus2lic4.sum <==
-Test Run By jahier on Fri Jun 23 10:32:56
+Test Run By jahier on Tue Jun 27 14:34:05
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic4 tests ===
@@ -1558,6 +1561,9 @@ PASS: ./lus2lic {-o struct0.lic struct0.lus}
PASS: ./lus2lic {-ec -o struct0.ec struct0.lus}
PASS: ./myec2c {-o struct0.c struct0.ec}
PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node struct0.lus {}
+PASS: ./lus2lic {-o struct_equality.lic struct_equality.lus}
+PASS: ./lus2lic {-ec -o struct_equality.ec struct_equality.lus}
+FAIL: Try ec2c on the result: ./myec2c {-o struct_equality.c struct_equality.ec}
PASS: ./lus2lic {-o struct_with.lic struct_with.lus}
PASS: ./lus2lic {-ec -o struct_with.ec struct_with.lus}
PASS: ./myec2c {-o struct_with.c struct_with.ec}
@@ -1748,8 +1754,8 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
=== lus2lic2 Summary ===
-# of expected passes 327
-# of unexpected failures 1
+# of expected passes 329
+# of unexpected failures 2
==> lus2lic3.sum <==
=== lus2lic3 Summary ===
@@ -1762,18 +1768,18 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
=== lus2lic4 Summary ===
-# of expected passes 465
-# of unexpected failures 6
+# of expected passes 467
+# of unexpected failures 7
===============================
-# Total number of failures: 23
+# Total number of failures: 25
lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 0 seconds
lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 52 seconds
-lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 71 seconds
-lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 136 seconds
-lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 65 seconds
+lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 72 seconds
+lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 135 seconds
+lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 64 seconds
* Ref time:
-0.04user 0.03system 5:25.43elapsed 0%CPU (0avgtext+0avgdata 5624maxresident)k
-160inputs+0outputs (0major+6173minor)pagefaults 0swaps
+0.05user 0.02system 5:30.19elapsed 0%CPU (0avgtext+0avgdata 5548maxresident)k
+64inputs+0outputs (0major+6187minor)pagefaults 0swaps
* Quick time (-j 4):
-0.04user 0.04system 2:18.88elapsed 0%CPU (0avgtext+0avgdata 5620maxresident)k
-96inputs+0outputs (0major+6165minor)pagefaults 0swaps
+0.05user 0.02system 2:39.50elapsed 0%CPU (0avgtext+0avgdata 5672maxresident)k
+128inputs+0outputs (0major+6172minor)pagefaults 0swaps
diff --git a/test/should_work/array_equals.lus b/test/should_work/array_equals.lus
index 96cfcdf3..f788fa72 100644
--- a/test/should_work/array_equals.lus
+++ b/test/should_work/array_equals.lus
@@ -2,5 +2,9 @@
node array_equals(x,y:bool^2) returns (res:bool);
let
res = (x=y);
+tel
+node array_not_equals(x,y:bool^2) returns (res:bool);
+let
+ res = (x<>y);
tel
-- end of some_node
\ No newline at end of file
diff --git a/test/should_work/struct_equality.lus b/test/should_work/struct_equality.lus
new file mode 100644
index 00000000..660b636f
--- /dev/null
+++ b/test/should_work/struct_equality.lus
@@ -0,0 +1,10 @@
+type complex = struct {
+ re : real = 42.0;
+ im : real = 42.0;
+};
+
+node struct_equality(a,b : complex) returns (res:bool);
+let
+ res = a=b;
+tel
+ -- end of struct_equality
\ No newline at end of file
diff --git a/utils/compare_exec_and_2c b/utils/compare_exec_and_2c
index 7dc92dd8..27256278 100755
--- a/utils/compare_exec_and_2c
+++ b/utils/compare_exec_and_2c
@@ -51,7 +51,7 @@ PRECISION=4
if
lurette -l 10 -o xxx.rif \
-sut "./$node.exec" \
- -env "lutin $env -n $env_node -p $PRECISION" \
+ -env "lutin $env -n $env_node -p $PRECISION -seed 42" \
-oracle "lus2lic $_oracle -n $oracle $OPT";
# lurettetop_exe -p $PRECISION -rp "sut:socket:127.0.0.1:$PORT" -rp "env:lutin:$env:-p:$PRECISION" -rp "oracle:v6:$_oracle:$oracle:$OPT" \
# -go -l 10 -ns2c --stop-on-oracle-error;
--
GitLab