Merge branch 'euclidean' into unstable

src/backends/C/c_backend_common.ml

@@ -108,16 +108,43 @@ let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
 let pp_machine_clear_name fmt id = fprintf fmt "%s_clear" id
 let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
 
-let pp_basic_lib_fun i pp_val fmt vl =
+let pp_mod pp_val v1 v2 fmt =
+  if !Options.integer_div_euclidean then
+    (* (a mod_C b) + (a < 0 ? abs(b) : 0) *)
+    Format.fprintf fmt "((%a %% %a) + (%a < 0?(abs(%a)):0))"
+      pp_val v1 pp_val v2
+      pp_val v1 pp_val v2
+  else (* Regular behavior: printing a % *)
+    Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
+
+let pp_div pp_val v1 v2 fmt =
+  if !Options.integer_div_euclidean then
+    (* (a - ((a mod_C b) + (a < 0 ? abs(b) : 0))) div_C b *)
+    Format.fprintf fmt "(%a - ((%a %% %a) + (%a < 0 ? abs(%a) : 0))) / %a"
+      pp_val v1 pp_val v1 pp_val v2
+      pp_val v1 pp_val v2 pp_val v2
+  else (* Regular behavior: printing a / *)
+    Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2
+  
+let pp_basic_lib_fun is_int i pp_val fmt vl =
   match i, vl with
   (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
   | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
   | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
   | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
   | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
-  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
+  | "mod", [v1; v2] ->
+     if is_int then
+       pp_mod pp_val v1 v2 fmt 
+     else
+       Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
   | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
   | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
+  | "/", [v1; v2] ->
+     if is_int then
+       pp_div pp_val v1 v2 fmt
+     else
+       Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2
   | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
   | _ -> (Format.eprintf "internal error: Basic_library.pp_c %s@." i; assert false)
 
@@ -134,7 +161,7 @@ let rec pp_c_dimension fmt dim =
      fprintf fmt "((%a)?%a:%a)"
        pp_c_dimension i pp_c_dimension t pp_c_dimension e
   | Dimension.Dappl (f, args) ->
-     fprintf fmt "%a" (pp_basic_lib_fun f pp_c_dimension) args
+     fprintf fmt "%a" (pp_basic_lib_fun (Basic_library.is_numeric_operator f) f pp_c_dimension) args
   | Dimension.Dlink dim' -> fprintf fmt "%a" pp_c_dimension dim'
   | Dimension.Dvar       -> fprintf fmt "_%s" (Utils.name_of_dimension dim.Dimension.dim_id)
   | Dimension.Dunivar    -> fprintf fmt "'%s" (Utils.name_of_dimension dim.Dimension.dim_id)
@@ -222,7 +249,7 @@ let rec pp_c_val self pp_var fmt v =
     if Types.is_array_type v.var_type && not (Types.is_real_type v.var_type && !Options.mpfr)
     then fprintf fmt "%a" pp_var v
     else fprintf fmt "%s->_reg.%a" self pp_var v
-  | Fun (n, vl)   -> pp_basic_lib_fun n (pp_c_val self pp_var) fmt vl
+  | Fun (n, vl)   -> pp_basic_lib_fun (Types.is_int_type v.value_type) n (pp_c_val self pp_var) fmt vl
 
 (* Access to the value of a variable:
    - if it's not a scalar output, then its name is enough

src/backends/C/c_backend_header.ml

@@ -55,7 +55,7 @@ let rec print_static_val pp_var fmt v =
   match v.value_desc with
   | Cst c         -> pp_c_const fmt c
   | LocalVar v    -> pp_var fmt v
-  | Fun (n, vl)   -> pp_basic_lib_fun n (print_static_val pp_var) fmt vl
+  | Fun (n, vl)   -> pp_basic_lib_fun (Types.is_int_type v.value_type) n (print_static_val pp_var) fmt vl
   | _             -> (Format.eprintf "Internal error: C_backend_header.print_static_val"; assert false)
 
 let print_constant_decl (m, attr, inst) pp_var fmt v =

src/backends/C/c_backend_src.ml

@@ -163,7 +163,7 @@ let rec pp_value_suffix self var_type loop_vars pp_value fmt value =
     | _           :: q, Power (v, n)  ->
        pp_value_suffix self var_type q pp_value fmt v
     | _               , Fun (n, vl)   ->
-       pp_basic_lib_fun n (pp_value_suffix self var_type loop_vars pp_value) fmt vl
+       pp_basic_lib_fun (Types.is_int_type value.value_type) n (pp_value_suffix self var_type loop_vars pp_value) fmt vl
     | _               , Access (v, i) ->
        let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in
        pp_value_suffix self var_type ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_value fmt v

src/backends/Horn/horn_backend_printers.ml

@@ -46,52 +46,6 @@ let rec pp_horn_const fmt c =
     | Const_tag t    -> pp_horn_tag fmt t
     | _              -> assert false
 
-(* PL comment 2017/01/03: Useless code, the function existed before in typing.ml *)
-(* let rec get_type_cst c = *)
-(*   match c with *)
-(*   | Const_int(n) -> new_ty Tint *)
-(*   | Const_real _ -> new_ty Treal *)
-(*   (\* | Const_float _ -> new_ty Treal *\) *)
-(*   | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), *)
-(* 				     get_type_cst (List.hd l))) *)
-(*   | Const_tag(tag) -> new_ty Tbool *)
-(*   | Const_string(str) ->  assert false(\* used only for annotations *\) *)
-(*   | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l)) *)
-
-(* PL comment 2017/01/03: the following function get_type seems useless to me: it looks like computing the type of a machine code expression v while v.value_type should contain this information. The code is kept for the moment in case I missed something *)
-
-(*
-let rec get_type v =
-  match v with
-  | Cst c -> Typing.type_const Location.dummy_loc c (* get_type_cst c*)
-  | Access(tab, index) -> begin
-      let rec remove_link ltype =
-        match (dynamic_type ltype).tdesc with
-        | Tlink t -> t
-        | _ -> ltype
-      in
-      match (dynamic_type (remove_link (get_type tab))).tdesc with
-      | Tarray(size, t) -> remove_link t
-      | Tvar -> Format.eprintf "Type of access is a variable... "; assert false
-      | Tunivar -> Format.eprintf "Type of access is a variable... "; assert false
-      | _ -> Format.eprintf "Type of access is not an array "; assert false
-                          end
-  | Power(v, n) -> assert false
-  | LocalVar v -> v.var_type
-  | StateVar v -> v.var_type
-  | Fun(n, vl) -> begin match n with
-                  | "+"
-                  | "-"
-                  | "*" -> get_type (List.hd vl)
-                  | _ -> Format.eprintf "Function undealt with : %s" n ;assert false
-                  end
-  | Array(l) -> new_ty (Tarray(Dimension.mkdim_int
-                                 (Location.dummy_loc)
-                                 (List.length l),
-                               get_type (List.hd l)))
-  | _ -> assert false
-*)
-
 (* Default value for each type, used when building arrays. Eg integer array
    [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
    for the type integer (arrays).
@@ -111,22 +65,42 @@ let rec pp_default_val fmt t =
   | Types.Ttuple(l) -> assert false
   |_ -> assert false
 
+let pp_mod pp_val v1 v2 fmt =
+  if Types.is_int_type v1.value_type &&  not !Options.integer_div_euclidean then
+    (* C semantics: converting it to Euclidian operators
+       (a mod_M b) - (a < 0 ? abs(b) : 0)            
+    *)
+    Format.fprintf fmt "(- (mod %a %a) (ite (< %a 0) (abs %a) 0))"
+      pp_val v1 pp_val v2 pp_val v1 pp_val v2
+  else
+    Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
+
+let pp_div pp_val v1 v2 fmt =
+  if Types.is_int_type v1.value_type &&  not !Options.integer_div_euclidean then
+    (* C semantics: converting it to Euclidian operators
+       (a - ((a mod_M b) - (a < 0 ? abs(b) : 0))) div_M b
+    *)
+    Format.fprintf fmt "(div (- %a (- (mod %a %a) (ite (< %a 0) (abs %a) 0))) %a)"
+      pp_val v1 pp_val v1 pp_val v2
+      pp_val v1 pp_val v2 pp_val v2
+  else
+    Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
+
 
 let pp_basic_lib_fun i pp_val fmt vl =
   match i, vl with
   | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
-
   | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
   | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
   | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
   | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
   | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
   | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
-  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
   | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
   | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
   | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
-  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
+  | "mod", [v1; v2] -> pp_mod pp_val v1 v2 fmt
+  | "/", [v1; v2] -> pp_div pp_val v1 v2 fmt
   | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
   | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
 (*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2

src/options.ml

@@ -35,6 +35,10 @@ let mpfr = ref false
 let mpfr_prec = ref 100
 let print_dec_types = ref false
 
+(* Option to select the expected behavior of integer division: Euclidian or
+   C. Default C !!! *)
+let integer_div_euclidean = ref false
+  
 let traces = ref false
 let horn_cex = ref false
 let horn_query = ref true

src/options_management.ml

@@ -97,33 +97,35 @@ let common_options =
   ]
 
 let lustrec_options =
-   common_options @
-  [ 
-    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
-    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
-    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
-    "-mpfr", Arg.Int set_mpfr, "replaces FP numbers by the MPFR library multiple precision numbers with a precision of \x1b[4mprec\x1b[0m bits <default: keep FP numbers>";
-    "-lusi", Arg.Set lusi, "only generates a .lusi interface source file from a Lustre source <default: no generation>";
-    "-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
-    "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
-    "-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
-    (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
-    "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
-    "-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
-    "-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
-    "-horn-query", Arg.Unit (fun () -> set_backend "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
-    "-horn-sfunction", Arg.Set_string sfunction, "Gets the endpoint predicate of the \x1b[4msfunction\x1b[0m";
-    "-print-reuse", Arg.Set print_reuse, "prints variable reuse policy";
-    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
-   "-emf", Arg.Unit (fun () -> set_backend "emf"), "generates EMF output, to be used by CocoSim";
-   "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
-    "-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
-    "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
-    
-    "-c++" , Arg.Set        cpp      , "c++ backend";
-    "-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")";
-    "-real", Arg.String set_real_type, "specifies the real type (default=\"double\" without mpfr option)";
-    "-real-print-prec", Arg.Set_int print_prec_double, "specifies the number of digits to be printed for real values (default=15)";
+  common_options @
+    [ 
+      "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
+      "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
+      "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
+      "-mpfr", Arg.Int set_mpfr, "replaces FP numbers by the MPFR library multiple precision numbers with a precision of \x1b[4mprec\x1b[0m bits <default: keep FP numbers>";
+      "-lusi", Arg.Set lusi, "only generates a .lusi interface source file from a Lustre source <default: no generation>";
+      "-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
+      "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
+      "-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
+      (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
+      "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
+      "-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
+      "-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
+      "-horn-query", Arg.Unit (fun () -> set_backend "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
+      "-horn-sfunction", Arg.Set_string sfunction, "Gets the endpoint predicate of the \x1b[4msfunction\x1b[0m";
+      "-print-reuse", Arg.Set print_reuse, "prints variable reuse policy";
+      "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
+      "-emf", Arg.Unit (fun () -> set_backend "emf"), "generates EMF output, to be used by CocoSim";
+      "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
+      "-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
+      "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
+      
+      "-c++" , Arg.Set        cpp      , "c++ backend";
+      "-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")";
+      "-real", Arg.String set_real_type, "specifies the real type (default=\"double\" without mpfr option)";
+      "-real-print-prec", Arg.Set_int print_prec_double, "specifies the number of digits to be printed for real values (default=15)";
+      "-int_div_euclidean", Arg.Set integer_div_euclidean, "interprets integer division as Euclidean (default : C division semantics)";
+      "-int_div_C", Arg.Clear integer_div_euclidean, "interprets integer division as C division (default)";
 
     "-mauve", Arg.String (fun node -> mauve := node; cpp := true; static_mem := false), "generates the mauve code";
 ]