Skip to content

Commit

Permalink
Comparaison des flottants à epsilon près (interpréteur + backend C). (#…
Browse files Browse the repository at this point in the history
  • Loading branch information
denismerigoux authored Jan 24, 2024
2 parents 8e98f0a + b2340da commit 08ce9cd
Show file tree
Hide file tree
Showing 15 changed files with 150 additions and 157 deletions.
3 changes: 0 additions & 3 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,7 @@ else
TEST_FILTER_FLAG=
endif

TEST_ERROR_MARGIN?=0.

MLANG_INTERPRETER_OPTS=\
--test_error_margin=$(TEST_ERROR_MARGIN) \
--mpp_file=$(MPP_FILE) \
--mpp_function=$(MPP_FUNCTION)

Expand Down
4 changes: 1 addition & 3 deletions Makefile.config.template
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,6 @@
# Interpreter instrumentation
# ---------------------------

# TEST_ERROR_MARGIN=0.

# CODE_COVERAGE=1

##################################################
Expand Down Expand Up @@ -67,4 +65,4 @@
##################################################
# Exports
##################################################
# Export here variables you need in recursive make calls
# Export here variables you need in recursive make calls
8 changes: 0 additions & 8 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -171,14 +171,6 @@ To check that Mlang passes all the randomized tests, simply invoke

make tests

Some tests might fail using non-default precision settings, even if the error
message shows no difference between the expected value and the computed value.
This is because we control a difference of 0 between the computed and the
expected, but when doing computations with a higher precision, a difference
lower than the smallest representable float value might appear. To pass the test,
we have provided the command line option `--test_error_margin=0.0000001` to
let you define how much error margin you want to tolerate when running tests.

## Documentation

The OCaml code is self-documented using `ocamldoc` style. You can generate the HTML
Expand Down
41 changes: 12 additions & 29 deletions examples/dgfip_c/ml_primitif/static/const.h
Original file line number Diff line number Diff line change
Expand Up @@ -79,45 +79,28 @@ struct S_discord
};

#ifdef FLG_MULTITHREAD

extern void add_erreur(T_irdata *irdata, T_erreur *erreur, char *code);
extern void free_erreur();

extern double my_ceil(double); /* ceil(a - 0.000001); */
extern double my_floor(double); /* floor(a + 0.000001); */
extern double my_arr(double); /* floor(v1 + v2 + 0.5) */

#else

extern void add_erreur(T_erreur *erreur, char *code);
extern void free_erreur();

#define my_ceil(a) (ceil((a) - 0.000001))

#ifdef FLG_OPTIM_MIN_MAX

#define my_floor(a) (floor_g((a) + 0.000001))
/*#define my_arr(a) (floor_g((a) + 0.50005)) *//* Ancienne version (2021) */
#define my_arr(a) (((a) < 0.0) ? ceil_g((a) - .50005) : floor_g((a) + .50005))

#else

#define my_floor(a) (floor((a) + 0.000001))
#define my_arr(a) ((double)(long long)(((a) < 0.0) ? ((a) - .50005) : ((a) + .50005)))

#endif /* FLG_OPTIM_MIN_MAX */

#endif /* FLG_MULTITHREAD */

#define fabs(a) (((a) < 0.0) ? -(a) : (a))
#define min(a,b) (((a) <= (b)) ? (a) : (b))
#define max(a,b) (((a) >= (b)) ? (a) : (b))
#define divd(a,b) (((b) != 0.0) ? (a / b) : 0.0)

#ifdef FLG_OPTIM_MIN_MAX

#define fabs(a) (((a) < 0.0) ? -(a) : (a))

#endif /* FLG_OPTIM_MIN_MAX */
#define EPSILON 0.000001
#define GT_E(a,b) ((a) > (b) + EPSILON)
#define LT_E(a,b) ((a) + EPSILON < (b))
#define GE_E(a,b) ((a) > (b) - EPSILON)
#define LE_E(a,b) ((a) - EPSILON < (b))
#define EQ_E(a,b) (fabs((a) - (b)) < EPSILON)
#define NEQ_E(a,b) (fabs((a) - (b)) >= EPSILON)
#define my_floor(a) (floor_g((a) + EPSILON))
#define my_ceil(a) (ceil_g((a) - EPSILON));
#define my_arr(a) (((a) < 0) ? ceil_g((a) - EPSILON - 0.5) : floor_g((a) + EPSILON + 0.5))
#define divd(a,b) (NEQ_E((b),0.0) ? (a / b) : 0.0)

extern double floor_g(double);
extern double ceil_g(double);
Expand Down
2 changes: 2 additions & 0 deletions examples/dgfip_c/ml_primitif/static/enchain_static.c.inc
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ static void add_erreur_code(T_erreur *erreur, const char *code)

#ifdef FLG_MULTITHREAD

/*
double my_floor(double a)
{
return floor(a + 0.000001);
Expand All @@ -54,6 +55,7 @@ double my_arr(double a)
v2 = floor((a - v1) * 100000. + 0.5) / 100000.;
return floor(v1 + v2 + 0.5);
}
*/

static void init_erreur(T_irdata *irdata)
{
Expand Down
49 changes: 38 additions & 11 deletions src/mlang/backend_compilers/decoupledExpr.ml
Original file line number Diff line number Diff line change
Expand Up @@ -301,21 +301,27 @@ let comp op (e1 : constr) (e2 : constr) (stacks : local_stacks)
(ctx : local_vars) : t =
let stacks', lv1, e1 = push_with_kind stacks ctx Val e1 in
let _, lv2, e2 = push_with_kind stacks' ctx Val e2 in
let comp o =
let comp (o : Mast.comp_op) =
match (e1, e2) with
| Dlit f1, Dlit f2 -> if o f1 f2 then Dtrue else Dfalse
| Dlit f1, Dlit f2 ->
if
Bir_interpreter.FloatDefInterp.compare_numbers o
(Bir_number.RegularFloatNumber.of_float f1)
(Bir_number.RegularFloatNumber.of_float f2)
then Dtrue
else Dfalse
| Dvar v1, Dvar v2 ->
if String.equal op "==" && v1 = v2 then Dtrue else Dbinop (op, e1, e2)
| _ -> Dbinop (op, e1, e2)
in
let e =
match op with
| "==" -> comp ( = )
| "!=" -> comp ( <> )
| "<=" -> comp ( <= )
| "<" -> comp ( < )
| ">=" -> comp ( >= )
| ">" -> comp ( > )
| "==" -> comp Mast.Eq
| "!=" -> comp Mast.Neq
| "<=" -> comp Mast.Lte
| "<" -> comp Mast.Lt
| ">=" -> comp Mast.Gte
| ">" -> comp Mast.Gt
| _ -> assert false
in
(e, Def, lv2 @ lv1)
Expand Down Expand Up @@ -442,9 +448,30 @@ let rec format_dexpr (dgfip_flags : Dgfip_options.flags)
Format.fprintf fmt "@[<hov 2>(%a@ || %a@])" format_dexpr de1 format_dexpr
de2
| Dunop (op, de) -> Format.fprintf fmt "@[<hov 2>(%s%a@])" op format_dexpr de
| Dbinop (op, de1, de2) ->
Format.fprintf fmt "@[<hov 2>(%a@ %s %a@])" format_dexpr de1 op
format_dexpr de2
| Dbinop (op, de1, de2) -> begin
match op with
| ">" ->
Format.fprintf fmt "@[<hov 2>(GT_E((%a),(%a))@])" format_dexpr de1
format_dexpr de2
| "<" ->
Format.fprintf fmt "@[<hov 2>(LT_E((%a),(%a))@])" format_dexpr de1
format_dexpr de2
| ">=" ->
Format.fprintf fmt "@[<hov 2>(GE_E((%a),(%a))@])" format_dexpr de1
format_dexpr de2
| "<=" ->
Format.fprintf fmt "@[<hov 2>(LE_E((%a),(%a))@])" format_dexpr de1
format_dexpr de2
| "==" ->
Format.fprintf fmt "@[<hov 2>(EQ_E((%a),(%a))@])" format_dexpr de1
format_dexpr de2
| "!=" ->
Format.fprintf fmt "@[<hov 2>(NEQ_E((%a),(%a))@])" format_dexpr de1
format_dexpr de2
| _ ->
Format.fprintf fmt "@[<hov 2>((%a)@ %s (%a)@])" format_dexpr de1 op
format_dexpr de2
end
| Dfun (funname, des) ->
Format.fprintf fmt "@[<hov 2>%s(%a@])" funname
(Format.pp_print_list
Expand Down
1 change: 1 addition & 0 deletions src/mlang/backend_compilers/dgfip_gen_files.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1147,6 +1147,7 @@ let gen_conf_h fmt flags vars =
FLG_TRACE_IRDATA\n"; *)
if flags.flg_debug then Format.fprintf fmt "#define FLG_DEBUG\n";
Format.fprintf fmt "#define NB_DEBUG_C %d\n" flags.nb_debug_c;
Format.fprintf fmt "#define EPSILON %f\n" !Cli.comparison_error_margin;

let nb_saisie = count vars (Input None) in
let nb_calculee = count vars (Computed (Some Computed)) in
Expand Down
28 changes: 15 additions & 13 deletions src/mlang/backend_ir/bir_interpreter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,8 @@ module type S = sig

val raise_runtime_as_structured : run_error -> ctx -> Mir.program -> 'a

val compare_numbers : Mast.comp_op -> custom_float -> custom_float -> bool

val evaluate_expr : ctx -> Mir.program -> Bir.expression Pos.marked -> value

val evaluate_program : Bir.program -> ctx -> int -> ctx
Expand Down Expand Up @@ -394,6 +396,16 @@ struct
else if N.(idx <. N.zero ()) then Number (N.zero ())
else values.(Int64.to_int (N.to_int idx))

let compare_numbers op i1 i2 =
let epsilon = N.of_float !Cli.comparison_error_margin in
match op with
| Mast.Gt -> N.(i1 >. i2 +. epsilon)
| Mast.Gte -> N.(i1 >. i2 -. epsilon)
| Mast.Lt -> N.(i1 +. epsilon <. i2)
| Mast.Lte -> N.(i1 -. epsilon <. i2)
| Mast.Eq -> N.(N.abs (i1 -. i2) <. epsilon)
| Mast.Neq -> N.(N.abs (i1 -. i2) >=. epsilon)

let rec evaluate_expr (ctx : ctx) (p : Mir.program)
(e : Bir.expression Pos.marked) : value =
let out =
Expand All @@ -403,24 +415,14 @@ struct
let new_e1 = evaluate_expr ctx p e1 in
let new_e2 = evaluate_expr ctx p e2 in
match (Pos.unmark op, new_e1, new_e2) with
| Mast.Gt, Number i1, Number i2 ->
Number N.(real_of_bool (i1 >. i2))
| Mast.Gt, _, Undefined | Mast.Gt, Undefined, _ -> Undefined
| Mast.Gte, Number i1, Number i2 ->
Number N.(real_of_bool (i1 >=. i2))
| Mast.Gte, _, Undefined | Mast.Gte, Undefined, _ -> Undefined
| Mast.Lt, Number i1, Number i2 ->
Number N.(real_of_bool (i1 <. i2))
| Mast.Lt, _, Undefined | Mast.Lt, Undefined, _ -> Undefined
| Mast.Lte, Number i1, Number i2 ->
Number N.(real_of_bool (i1 <=. i2))
| Mast.Lte, _, Undefined | Mast.Lte, Undefined, _ -> Undefined
| Mast.Eq, Number i1, Number i2 ->
Number N.(real_of_bool (i1 =. i2))
| Mast.Eq, _, Undefined | Mast.Eq, Undefined, _ -> Undefined
| Mast.Neq, Number i1, Number i2 ->
Number N.(real_of_bool (not (i1 =. i2)))
| Mast.Neq, _, Undefined | Mast.Neq, Undefined, _ -> Undefined)
| Mast.Neq, _, Undefined | Mast.Neq, Undefined, _ -> Undefined
| op, Number i1, Number i2 ->
Number (real_of_bool (compare_numbers op i1 i2)))
| Binop (op, e1, e2) -> (
let new_e1 = evaluate_expr ctx p e1 in
let new_e2 = evaluate_expr ctx p e2 in
Expand Down
31 changes: 19 additions & 12 deletions src/mlang/backend_ir/bir_interpreter.mli
Original file line number Diff line number Diff line change
Expand Up @@ -125,12 +125,17 @@ module type S = sig
val raise_runtime_as_structured : run_error -> ctx -> Mir.program -> 'a
(** Raises a runtime error with a formatted error message and context *)

val compare_numbers : Mast.comp_op -> custom_float -> custom_float -> bool
(** Returns the comparison between two numbers in the rounding and precision
context of the interpreter. *)

val evaluate_expr : ctx -> Mir.program -> Bir.expression Pos.marked -> value

val evaluate_program : Bir.program -> ctx -> int -> ctx
end

module FloatDefInterp : S
module FloatDefInterp :
S with type custom_float = Bir_number.RegularFloatNumber.t
(** The different interpreters, which combine a representation of numbers and
rounding operations. The first part of the name corresponds to the
representation of numbers, and is one of the following:
Expand All @@ -149,33 +154,35 @@ module FloatDefInterp : S
- Multi: use the rouding operations of the PC/multi-thread context
- Mf: use the rounding operations of the mainframe context *)

module FloatMultInterp : S
module FloatMultInterp :
S with type custom_float = Bir_number.RegularFloatNumber.t

module FloatMfInterp : S
module FloatMfInterp :
S with type custom_float = Bir_number.RegularFloatNumber.t

module MPFRDefInterp : S
module MPFRDefInterp : S with type custom_float = Bir_number.MPFRNumber.t

module MPFRMultInterp : S
module MPFRMultInterp : S with type custom_float = Bir_number.MPFRNumber.t

module MPFRMfInterp : S
module MPFRMfInterp : S with type custom_float = Bir_number.MPFRNumber.t

module BigIntDefInterp : S

module BigIntMultInterp : S

module BigIntMfInterp : S

module IntvDefInterp : S
module IntvDefInterp : S with type custom_float = Bir_number.IntervalNumber.t

module IntvMultInterp : S
module IntvMultInterp : S with type custom_float = Bir_number.IntervalNumber.t

module IntvMfInterp : S
module IntvMfInterp : S with type custom_float = Bir_number.IntervalNumber.t

module RatDefInterp : S
module RatDefInterp : S with type custom_float = Bir_number.RationalNumber.t

module RatMultInterp : S
module RatMultInterp : S with type custom_float = Bir_number.RationalNumber.t

module RatMfInterp : S
module RatMfInterp : S with type custom_float = Bir_number.RationalNumber.t

(** {1 Generic interpretation API}*)

Expand Down
22 changes: 16 additions & 6 deletions src/mlang/backend_ir/bir_roundops.ml
Original file line number Diff line number Diff line change
Expand Up @@ -29,22 +29,29 @@ module DefaultRoundOps (N : Bir_number.NumberInterface) :
RoundOpsInterface with type t = N.t = struct
type t = N.t

let truncatef (x : N.t) : N.t = N.floor N.(x +. N.of_float 0.000001)
let truncatef (x : N.t) : N.t =
N.floor N.(x +. N.of_float !Cli.comparison_error_margin)

(* Careful : rounding in M is done with this arbitrary behavior. We can't use
copysign here because [x < zero] is critical to have the correct behavior
on -0 *)
let roundf (x : N.t) =
N.of_int
(N.to_int
N.(x +. N.of_float (if N.(x < zero ()) then -0.50005 else 0.50005)))
N.(
x
+. N.of_float
(if N.(x < zero ()) then
Float.sub (-0.5) !Cli.comparison_error_margin
else Float.add 0.5 !Cli.comparison_error_margin)))
end

module MultiRoundOps (N : Bir_number.NumberInterface) :
RoundOpsInterface with type t = N.t = struct
type t = N.t

let truncatef (x : N.t) : N.t = N.floor N.(x +. N.of_float 0.000001)
let truncatef (x : N.t) : N.t =
N.floor N.(x +. N.of_float !Cli.comparison_error_margin)

let roundf (x : N.t) =
let n_0_5 = N.of_float 0.5 in
Expand All @@ -66,12 +73,15 @@ end)
let ceil_g (x : N.t) : N.t =
if N.abs x <= N.of_int !L.max_long then N.ceil x else x

let truncatef (x : N.t) : N.t = floor_g N.(x +. N.of_float 0.000001)
let truncatef (x : N.t) : N.t =
floor_g N.(x +. N.of_float !Cli.comparison_error_margin)

(* Careful : rounding in M is done with this arbitrary behavior. We can't use
copysign here because [x < zero] is critical to have the correct behavior
on -0 *)
let roundf (x : N.t) =
if N.(x < zero ()) then ceil_g N.(x -. N.of_float 0.50005)
else floor_g N.(x +. N.of_float 0.50005)
if N.(x < zero ()) then
ceil_g N.(x -. N.of_float (Float.add 0.5 !Cli.comparison_error_margin))
else
floor_g N.(x +. N.of_float (Float.add 0.5 !Cli.comparison_error_margin))
end
Loading

0 comments on commit 08ce9cd

Please sign in to comment.