Commit 99ee9b44 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Bertrand fixed a bug in polka where overflow errors were silently

returning wrongs values.  The problem was due to the use of caml
integer, that were not always big enough (on 32 bits arch). Bertrand
fixed by usings the Nums ocaml lib.
parent 8e032dba
......@@ -58,13 +58,13 @@ rung: polkarung
polkatopg: polka.cma libpolkag_caml_debug.a ../C/libpolkag.a
$(OCAMLMKTOP) $(MLFLAGS) -o $@ -custom $^ -cclib "-L$(CAMLIDL_PREFIX) -lcamlidl -L$(GMP_PREFIX)/lib -lgmp"
$(OCAMLMKTOP) $(MLFLAGS) -o $@ -custom nums.cma $^ -cclib "-L$(CAMLIDL_PREFIX) -lcamlidl -L$(GMP_PREFIX)/lib -lgmp"
polkatopi: polka.cma libpolkai_caml_debug.a ../C/libpolkai.a
$(OCAMLMKTOP) $(MLFLAGS) -o $@ -custom $^ -cclib "-L$(CAMLIDL_PREFIX) -lcamlidl -L$(GMP_PREFIX)/lib -lgmp"
$(OCAMLMKTOP) $(MLFLAGS) -o $@ -custom nums.cma $^ -cclib "-L$(CAMLIDL_PREFIX) -lcamlidl -L$(GMP_PREFIX)/lib -lgmp"
polkatopl: polka.cma libpolkal_caml_debug.a ../C/libpolkal.a
$(OCAMLMKTOP) $(MLFLAGS) -o $@ -custom $^ -cclib "-L$(CAMLIDL_PREFIX) -lcamlidl -L$(GMP_PREFIX)/lib -lgmp"
$(OCAMLMKTOP) $(MLFLAGS) -o $@ -custom nums.cma $^ -cclib "-L$(CAMLIDL_PREFIX) -lcamlidl -L$(GMP_PREFIX)/lib -lgmp"
......
......@@ -135,6 +135,8 @@ boolean matrix_is_row_dummy_constraint(matrix__t mat, int row)
/* \section{Input/Output functions} %======================================== */
quote(MLI," \n\
val get_big_int : t -> int -> int -> Big_int.big_int
val set_big_int : t -> int -> int -> Big_int.big_int -> unit
val print : Format.formatter -> t -> unit \n\
val print_constraints : (int -> string) -> Format.formatter -> t -> unit \n\
val print_frames : (int -> string) -> Format.formatter -> t -> unit \n\
......@@ -143,6 +145,13 @@ val of_lframes : (string -> int) -> int -> string list -> t \n\
")
quote(ML," \n\
let get_big_int mat i j = \n\
try Big_int.big_int_of_int (get mat i j) \n\
with Polka.Overflow(s) -> Big_int.big_int_of_string s \n\
let set_big_int mat i j v = \n\
if Big_int.is_int_big_int v \n\
then set mat i j (Big_int.int_of_big_int v) \n\
else set_str10 mat i j (Big_int.string_of_big_int v) \n\
let print formatter mat = \n\
let nbrows = nbrows mat in \n\
Format.fprintf formatter \"@[<v>\"; \n\
......@@ -161,7 +170,7 @@ let print_constraints assoc formatter mat = \n\
let lchaines = ref [] in \n\
for i = nbrows-1 downto 0 do \n\
lchaines := (Polka.to_constraint assoc \n\
(fun j -> get mat i j) \n\
(fun j -> get_big_int mat i j) \n\
nbcolumns) :: !lchaines \n\
done; \n\
Polka.print_list formatter \"{@[<hov>\" \",@,\" \"@]}\" \n\
......@@ -179,7 +188,7 @@ let print_frames assoc formatter mat = \n\
let lchaines = ref [] in \n\
for i = nbrows-1 downto 0 do \n\
lchaines := (Polka.to_frame assoc \n\
(fun j -> get mat i j) \n\
(fun j -> get_big_int mat i j) \n\
nbcolumns) :: !lchaines \n\
done; \n\
Polka.print_list formatter \"{@[<hov>\" \",@,\" \"@]}\" \n\
......
......@@ -45,48 +45,51 @@ type gen = Vertex | Ray | Line
let denominator_of_list list =
let rec parcours res = function
| [] -> res
| (n,d,v)::suite -> parcours (res*d) suite
| (n,d,v)::suite -> parcours (Big_int.mult_big_int res d) suite
in
parcours 1 list
parcours Big_int.unit_big_int list
(* %========================================================================= *)
(* \section{Output functions, from vectors to string} *)
(* %========================================================================= *)
let to_constraint assoc get size =
let munit = Big_int.minus_big_int Big_int.unit_big_int in
let gauche = ref ""
and droite = ref ""
and sens_normal = ref true in
for i = !dec to size-1 do
let coeff = get i and nom = assoc (i - !dec) in
if coeff>0 then begin
let sgn = Big_int.sign_big_int coeff in
if sgn>0 then begin
gauche :=
(if !gauche = "" then !gauche else !gauche ^"+") ^
(if coeff = 1 then "" else string_of_int coeff) ^ nom
(if Big_int.eq_big_int coeff Big_int.unit_big_int then "" else Big_int.string_of_big_int coeff) ^ nom
end
else if coeff<0 then begin
else if sgn<0 then begin
if !gauche = "" then sens_normal := false;
droite :=
(if !droite = "" then !droite else (!droite)^"+") ^
(if coeff = (-1) then "" else string_of_int (-coeff)) ^ nom
(if Big_int.eq_big_int coeff munit then "" else Big_int.string_of_big_int (Big_int.minus_big_int coeff)) ^ nom
end
done;
let cst = get 1 in
let sgn = Big_int.sign_big_int cst in
if cst > 0 then
gauche := (if !gauche = "" then !gauche else !gauche ^"+") ^ (string_of_int cst)
else if cst < 0 then
droite := (if !droite = "" then !droite else (!droite)^"+") ^ (string_of_int (-cst));
if sgn > 0 then
gauche := (if !gauche = "" then !gauche else !gauche ^"+") ^ (Big_int.string_of_big_int cst)
else if sgn < 0 then
droite := (if !droite = "" then !droite else (!droite)^"+") ^ (Big_int.string_of_big_int (Big_int.minus_big_int cst));
if !gauche="" && !droite="" then (* aucun coefficient non nul, a part (peut-etre) $\epsilon$ *)
if !strict then
let epsilon = get 2 in
if epsilon = 1 then
if Big_int.eq_big_int epsilon Big_int.unit_big_int then
"$>=0"
else if epsilon=0 then
else if Big_int.eq_big_int epsilon Big_int.zero_big_int then
"0"
else
let msg = Format.sprintf "Vector._to_constraint: anomaly, constraint %d$ >= 0 !" epsilon in
let msg = Format.sprintf "Vector._to_constraint: anomaly, constraint %s$ >= 0 !" (Big_int.string_of_big_int epsilon) in
failwith msg
else
"0"
......@@ -94,13 +97,18 @@ let to_constraint assoc get size =
if !gauche="" then gauche := "0"
else if !droite="" then droite := "0";
let signe =
if get 0 = 0 then "="
else if !strict && (get 2)<0 then
let c0 = get 0 in
if Big_int.eq_big_int c0 Big_int.zero_big_int then "="
else begin
let c2 = get 2 in
let sgn2 = Big_int.sign_big_int c2 in
if !strict && sgn2<0 then
if !sens_normal then ">" else "<"
else if !strict && (get 2)>0 then
else if !strict && sgn2>0 then
if !sens_normal then ">" else "<"
else
if !sens_normal then ">=" else "<="
end
in
if !sens_normal then
!gauche ^ signe ^ !droite
......@@ -112,23 +120,25 @@ let to_frame assoc get size =
let chaine = ref "" in
if !strict then begin
let epsilon = get 2 in
if epsilon > 0 then
chaine := (if epsilon=1 then "" else (string_of_int epsilon)) ^ "$" ^ !chaine
else if epsilon < 0 then
let sgn = Big_int.sign_big_int epsilon in
if sgn > 0 then
chaine := (if Big_int.eq_big_int epsilon Big_int.unit_big_int then "" else (Big_int.string_of_big_int epsilon)) ^ "$" ^ !chaine
else if sgn < 0 then
failwith "Vector._to_constraint: anomaly, vertex with \\epsilon < 0 !"
end;
for i = !dec to size-1 do
let coeff = get i and nom = assoc (i - !dec) in
let ajout =
if coeff>0 then
let sgn = Big_int.sign_big_int coeff in
if sgn>0 then
(^)
(if !chaine="" then "" else "+")
(if coeff=1 then nom else (string_of_int coeff)^nom)
else if coeff<0 then
let coeff = -coeff in
(if Big_int.eq_big_int coeff Big_int.unit_big_int then nom else (Big_int.string_of_big_int coeff)^nom)
else if sgn<0 then
let coeff = Big_int.minus_big_int coeff in
(^)
"-"
(if coeff=1 then nom else (string_of_int coeff)^nom)
(if Big_int.eq_big_int coeff Big_int.unit_big_int then nom else (Big_int.string_of_big_int coeff)^nom)
else
""
in
......@@ -137,9 +147,9 @@ let to_frame assoc get size =
let x0 = get 0
and x1 = get 1
in
if x0=0 || x1=0 then begin
if Big_int.eq_big_int x1 Big_int.zero_big_int then begin
(* line or ray *)
if x0=0 then
if Big_int.eq_big_int x0 Big_int.zero_big_int then
(* line *)
"L:" ^ !chaine
else
......@@ -149,9 +159,9 @@ let to_frame assoc get size =
(* vertex *)
if !chaine="" then
chaine := "0"
else if x1<>1 then
chaine := "(" ^ !chaine ^ ")/" ^ (string_of_int x1);
if !strict && (get 2)<>0 then
else if not (Big_int.eq_big_int x1 Big_int.unit_big_int) then
chaine := "(" ^ !chaine ^ ")/" ^ (Big_int.string_of_big_int x1);
if !strict && not (Big_int.eq_big_int (get 2) Big_int.zero_big_int) then
"Vs:" ^ !chaine
else
"V:" ^ !chaine
......@@ -164,26 +174,29 @@ let to_expr assoc get size =
let chaine = ref "" in
for i = !dec to size-1 do
let coeff = get i and nom = assoc (i - !dec) in
if coeff<>0 then
let sgn = Big_int.sign_big_int coeff in
let coeff = Big_int.abs_big_int coeff in
if sgn<>0 then
chaine :=
!chaine ^
(if coeff < 0 then "-" else (if !chaine="" then "" else "+")) ^
(if coeff = 1 then "" else string_of_int (abs coeff)) ^
nom
(if sgn < 0 then "-" else (if !chaine="" then "" else "+")) ^
(if Big_int.eq_big_int coeff Big_int.unit_big_int then "" else Big_int.string_of_big_int coeff) ^
nom
done;
let cst = get 1 in
if cst<>0 then
let sgn = Big_int.sign_big_int cst in
if sgn<>0 then
chaine :=
!chaine ^
(if cst < 0 then "-" else (if !chaine="" then "" else "+")) ^
(string_of_int (abs cst))
(if sgn < 0 then "-" else (if !chaine="" then "" else "+")) ^
(Big_int.string_of_big_int (Big_int.abs_big_int cst))
;
if !chaine="" then chaine := "0";
let denom = get 0 in
if denom = 1 then
if Big_int.eq_big_int denom Big_int.unit_big_int then
!chaine
else
"(" ^ !chaine ^ ")/" ^ (string_of_int denom)
"(" ^ !chaine ^ ")/" ^ (Big_int.string_of_big_int denom)
let print_list fmt
(deb:(unit,Format.formatter,unit) format)
......
......@@ -17,12 +17,11 @@ external set_gc : int -> unit = "camlidl_polka_set_gc"
external set_widening_affine : unit -> unit = "camlidl_polka_set_widening_affine"
external set_widening_linear : unit -> unit = "camlidl_polka_set_widening_linear"
val denominator_of_list : (Big_int.big_int * Big_int.big_int * string) list -> Big_int.big_int
val denominator_of_list : (int * int * string) list -> int
val to_constraint : (int -> string) -> (int -> int) -> int -> string
val to_frame : (int -> string) -> (int -> int) -> int -> string
val to_expr : (int -> string) -> (int -> int) -> int -> string
val to_constraint : (int -> string) -> (int -> Big_int.big_int) -> int -> string
val to_frame : (int -> string) -> (int -> Big_int.big_int) -> int -> string
val to_expr : (int -> string) -> (int -> Big_int.big_int) -> int -> string
val print_list :
......
open Format
let name_of_rank = ref (Array.make 0 "")
......
......@@ -22,12 +22,12 @@ static inline void int_set_pkint(long* pres, pkint_t x, bool clear)
(void)pkint_get_str10(str, x);
value v = caml_copy_string(str);
free(str);
if (clear) pkint_clear(x);
if (clear){ pkint_clear(x); }
caml_raise_with_arg(*caml_named_value("camlidl_polka_overflow"),v);
}
else {
*pres = pkint_get_si(x);
if (clear) pkint_clear(x);
if (clear){ pkint_clear(x); }
}
}
......
......@@ -6,12 +6,7 @@
open Polka_parser
open Lexing
exception Error of int * int
let local_int_of_string str =
try int_of_string str
with _ ->
failwith ("Error in Polka lexer: can not convert " ^ str ^ " into an int.\n")
}
}
rule lex = parse
eof { TK_EOF }
......@@ -34,7 +29,7 @@ rule lex = parse
| "=" { TK_EG }
(* Identificateurs *)
| (['0'-'9'])+ { TK_NUM(local_int_of_string (lexeme lexbuf)) }
| (['0'-'9'])+ { TK_NUM(Big_int.big_int_of_string (lexeme lexbuf)) }
| ['A'-'Z' 'a'-'z' '_']
( ['_' 'A'-'Z' 'a'-'z' '0'-'9'] ) *
( ['\''] ) *
......
......@@ -6,7 +6,7 @@
(* This function allows to negate a vector. *)
let rec opp = function
| [] -> []
| (n,d,v)::suite -> (-n,d,v) :: (opp suite)
| (n,d,v)::suite -> (Big_int.minus_big_int n,d,v) :: (opp suite)
%}
/* \section{Lexems} %======================================================== */
......@@ -19,19 +19,19 @@ let rec opp = function
%token TK_SUPEG TK_INFEG TK_SUP TK_INF TK_EG
%token <int> TK_NUM
%token <Big_int.big_int> TK_NUM
%token <string> TK_VAR
%nonassoc TK_SUP TK_SUPEG TK_INF TK_INFEG TK_EG
%left TK_PLUS
%left TK_PLUS
%right TK_MOINS
%left TK_DIV
%start constrain frame expression
%type <Polka.cons * (int * int * string) list> constrain
%type <Polka.gen * (int * int * string) list> frame
%type <(int * int * string) list> expression
%type <Polka.cons * (Big_int.big_int * Big_int.big_int * string) list> constrain
%type <Polka.gen * (Big_int.big_int * Big_int.big_int * string) list> frame
%type <(Big_int.big_int * Big_int.big_int * string) list> expression
%%
......@@ -53,17 +53,16 @@ expression:
expr TK_EOF { $1 }
expr:
expr TK_PLUS term { $1@[$3] }
| expr TK_MOINS term { let (n,d,v) = $3 in $1@[(-n,d,v)] }
| expr TK_MOINS term { let (n,d,v) = $3 in $1@[(Big_int.minus_big_int n,d,v)] }
| TK_PLUS term { [$2] }
| TK_MOINS term { let (n,d,v) = $2 in [(-n,d,v)] }
| TK_MOINS term { let (n,d,v) = $2 in [(Big_int.minus_big_int n,d,v)] }
| term { [$1] }
term:
TK_VAR { (1,1,$1) }
TK_VAR { (Big_int.unit_big_int,Big_int.unit_big_int,$1) }
| coeff TK_VAR { let (n,d) = $1 in (n,d,$2) }
| coeff { let (n,d) = $1 in (n,d,"") }
coeff:
TK_NUM TK_DIV TK_NUM { ($1,$3) }
| TK_NUM { ($1,1) }
| TK_NUM { ($1,Big_int.unit_big_int) }
......@@ -176,6 +176,8 @@ boolean vector_is_dummy_constraint(vector__t vec)
/* \section{Input/Output functions} %======================================== */
quote(MLI," \n\
val get_big_int : t -> int -> Big_int.big_int \n\
val set_big_int : t -> int -> Big_int.big_int -> unit \n\
val to_constraint: (int -> string) -> t -> string \n\
val to_frame: (int -> string) -> t -> string \n\
val to_expr: (int -> string) -> t -> string \n\
......@@ -190,12 +192,19 @@ val of_expr: (string -> int) -> int -> string -> t \n\
")
quote(ML," \n\
let get_big_int vec i = \n\
try Big_int.big_int_of_int (get vec i) \n\
with Polka.Overflow(s) -> Big_int.big_int_of_string s \n\
let set_big_int vec i v = \n\
if Big_int.is_int_big_int v \n\
then set vec i (Big_int.int_of_big_int v) \n\
else set_str10 vec i (Big_int.string_of_big_int v) \n\
let to_constraint assoc vec = \n\
Polka.to_constraint assoc (get vec) (length vec) \n\
Polka.to_constraint assoc (get_big_int vec) (length vec) \n\
let to_frame assoc vec = \n\
Polka.to_frame assoc (get vec) (length vec) \n\
Polka.to_frame assoc (get_big_int vec) (length vec) \n\
let to_expr assoc vec = \n\
Polka.to_expr assoc (get vec) (length vec) \n\
Polka.to_expr assoc (get_big_int vec) (length vec) \n\
\n\
let print formatter vec = \n\
let length = length vec in \n\
......@@ -248,8 +257,13 @@ let of_constraint assoc dim str = \n\
while !l<>[] do \n\
let (n,d,v) = List.hd !l in \n\
let rank = (if v=\"\" then 1 else !Polka.dec + (assoc v)) in \n\
let coeff = get vec rank in \n\
set vec rank (coeff + n*(denominator/d)); \n\
let coeff = get_big_int vec rank in \n\
set_big_int vec rank \n\
(Big_int.add_big_int \n\
coeff \n\
(Big_int.mult_big_int \n\
n \n\
(Big_int.div_big_int denominator d))); \n\
l := List.tl !l \n\
done; \n\
norm vec; \n\
......@@ -276,14 +290,19 @@ let of_frame assoc dim str = \n\
let denominator = Polka.denominator_of_list list in \n\
let vec = make (!Polka.dec + dim) in \n\
set vec 0 (if gen = Polka.Line then 0 else 1); \n\
set vec 1 (if gen = Polka.Vertex then denominator else 0); \n\
set_big_int vec 1 (if gen = Polka.Vertex then denominator else Big_int.zero_big_int); \n\
let l = ref list in \n\
while !l<>[] do \n\
let (n,d,v) = List.hd !l in \n\
if v=\"\" && n<>0 then failwith (\"Constant has no sense in generator \"^str); \n\
if v=\"\" && (Big_int.sign_big_int n)<>0 then failwith (\"Constant has no sense in generator \"^str); \n\
let rank = !Polka.dec + (assoc v) in \n\
let coeff = get vec rank in \n\
set vec rank (coeff + n*(denominator/d)); \n\
let coeff = get_big_int vec rank in \n\
set_big_int vec rank \n\
(Big_int.add_big_int \n\
coeff \n\
(Big_int.mult_big_int \n\
n \n\
(Big_int.div_big_int denominator d))); \n\
l := List.tl !l \n\
done; \n\
norm vec; \n\
......@@ -309,13 +328,18 @@ let of_expr assoc dim str = \n\
in \n\
let denominator = Polka.denominator_of_list list in \n\
let vec = make (!Polka.dec + dim) in \n\
set vec 0 denominator; \n\
set_big_int vec 0 denominator; \n\
let l = ref list in \n\
while !l<>[] do \n\
let (n,d,v) = List.hd !l in \n\
let rank = (if v=\"\" then 1 else !Polka.dec + (assoc v)) in \n\
let coeff = get vec rank in \n\
set vec rank (coeff + n*(denominator/d)); \n\
let coeff = get_big_int vec rank in \n\
set_big_int vec rank \n\
(Big_int.add_big_int \n\
coeff \n\
(Big_int.mult_big_int \n\
n \n\
(Big_int.div_big_int denominator d))); \n\
l := List.tl !l \n\
done; \n\
norm_expr vec; \n\
......
Supports Markdown
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