core/Term: smart, protecting constructors for integer constants

examples/use_api.ml

@@ -127,8 +127,8 @@ An arithmetic goal: 2+2 = 4
 
 *)
 
-let two : Term.term = Term.t_const (Term.ConstInt (Term.IConstDecimal "2"))
-let four : Term.term = Term.t_const (Term.ConstInt (Term.IConstDecimal "4"))
+let two : Term.term = Term.t_const (Term.ConstInt (Term.int_const_decimal "2"))
+let four : Term.term = Term.t_const (Term.ConstInt (Term.int_const_decimal "4"))
 let int_theory : Theory.theory =
   Env.find_theory env ["int"] "Int"
 let plus_symbol : Term.lsymbol =
@@ -156,7 +156,7 @@ let () = printf "@[On task 3, alt-ergo answers %a@."
   Call_provers.print_prover_result result3
 
 (* quantifiers: let's build "forall x:int. x*x >= 0" *)
-let zero : Term.term = Term.t_const (Term.ConstInt (Term.IConstDecimal "0"))
+let zero : Term.term = Term.t_const (Term.ConstInt (Term.int_const_decimal "0"))
 let mult_symbol : Term.lsymbol =
   Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
 let ge_symbol : Term.lsymbol =
@@ -217,9 +217,9 @@ let d =
   }
   in
   let body =
-    let c6 = Term.t_const (Term.ConstInt (Term.IConstDecimal "6")) in
-    let c7 = Term.t_const (Term.ConstInt (Term.IConstDecimal "7")) in
-    let c42 = Term.t_const (Term.ConstInt (Term.IConstDecimal "42")) in
+    let c6 = Term.t_const (Term.ConstInt (Term.int_const_decimal "6")) in
+    let c7 = Term.t_const (Term.ConstInt (Term.int_const_decimal "7")) in
+    let c42 = Term.t_const (Term.ConstInt (Term.int_const_decimal "42")) in
     let p = 
       Term.t_equ (Term.t_app_infer mul_int [c6;c7]) c42
     in

src/core/pretty.ml

@@ -518,6 +518,8 @@ let () = Exn_printer.register
       fprintf fmt "Variable %a is used twice" print_vsty vs
   | Term.UncoveredVar vs ->
       fprintf fmt "Variable %a uncovered in \"or\"-pattern" print_vsty vs
+  | Term.InvalidConstantLiteral(n,s) ->
+      fprintf fmt "Invalid constant literal in base %d: '%s'" n s
   | Term.FunctionSymbolExpected ls ->
       fprintf fmt "Not a function symbol: %a" print_ls ls
   | Term.PredicateSymbolExpected ls ->

src/core/term.ml

@@ -257,6 +257,37 @@ type integer_constant =
   | IConstOctal of string
   | IConstBinary of string
 
+exception InvalidConstantLiteral of int * string
+let invalid_constant_literal n s = raise (InvalidConstantLiteral(n,s))
+
+let check_integer_literal n f s =
+  let l = String.length s in
+  if l = 0 then invalid_constant_literal n s;
+  for i=0 to l-1 do
+    if not (f s.[i]) then invalid_constant_literal n s;
+  done
+
+let int_const_decimal s =
+  check_integer_literal 10 
+    (function '0'..'9' -> true | _ -> false) s;
+  IConstDecimal s
+
+let int_const_hexa s =
+  check_integer_literal 16
+    (function '0'..'9' | 'A'..'F' | 'a'..'f' -> true | _ -> false) s;
+  IConstHexa s
+
+let int_const_octal s =
+  check_integer_literal 8
+    (function '0'..'7' -> true | _ -> false) s;
+  IConstOctal s
+
+let int_const_binary s =
+  check_integer_literal 8
+    (function '0'..'1' -> true | _ -> false) s;
+  IConstBinary s
+
+
 type real_constant =
   | RConstDecimal of string * string * string option (* int / frac / exp *)
   | RConstHexa of string * string * string

src/core/term.mli

@@ -62,6 +62,7 @@ exception UncoveredVar of vsymbol
 exception BadArity of lsymbol * int * int
 exception FunctionSymbolExpected of lsymbol
 exception PredicateSymbolExpected of lsymbol
+exception InvalidConstantLiteral of int * string
 
 (** {2 Patterns} *)
 
@@ -109,13 +110,18 @@ type binop =
   | Timplies
   | Tiff
 
-type integer_constant =
+type integer_constant = private
   | IConstDecimal of string
   | IConstHexa of string
   | IConstOctal of string
   | IConstBinary of string
 
-type real_constant =
+val int_const_decimal : string -> integer_constant
+val int_const_hexa : string -> integer_constant
+val int_const_octal : string -> integer_constant
+val int_const_binary : string -> integer_constant
+
+type real_constant = 
   | RConstDecimal of string * string * string option (* int / frac / exp *)
   | RConstHexa of string * string * string
 

src/parser/lexer.mll

@@ -184,13 +184,13 @@ rule token = parse
   | uident as id
       { UIDENT id }
   | ['0'-'9'] ['0'-'9' '_']* as s
-      { INTEGER (IConstDecimal (remove_underscores s)) }
+      { INTEGER (int_const_decimal (remove_underscores s)) }
   | '0' ['x' 'X'] (['0'-'9' 'A'-'F' 'a'-'f']['0'-'9' 'A'-'F' 'a'-'f' '_']* as s)
-      { INTEGER (IConstHexa (remove_underscores s)) }
+      { INTEGER (int_const_hexa (remove_underscores s)) }
   | '0' ['o' 'O'] (['0'-'7'] ['0'-'7' '_']* as s)
-      { INTEGER (IConstOctal (remove_underscores s)) }
+      { INTEGER (int_const_octal (remove_underscores s)) }
   | '0' ['b' 'B'] (['0'-'1'] ['0'-'1' '_']* as s)
-      { INTEGER (IConstBinary (remove_underscores s)) }
+      { INTEGER (int_const_binary (remove_underscores s)) }
   | (digit+ as i) ("" as f) ['e' 'E'] (['-' '+']? digit+ as e)
   | (digit+ as i) '.' (digit* as f) (['e' 'E'] (['-' '+']? digit+ as e))?
   | (digit* as i) '.' (digit+ as f) (['e' 'E'] (['-' '+']? digit+ as e))?

src/transform/eliminate_algebraic.ml

@@ -231,7 +231,7 @@ let add_indexer (state,task) ts ty csl =
     let pr = create_prsymbol (id_derive id cs.ls_name) in
     let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in
     let hd = fs_app cs (List.rev_map t_var vl) (Opt.get cs.ls_value) in
-    let ix = t_const (ConstInt (IConstDecimal(string_of_int !index))) in
+    let ix = t_const (ConstInt (int_const_decimal (string_of_int !index))) in
     let ax = t_equ (fs_app mt_ls [hd] ty_int) ix in
     let ax = t_forall_close (List.rev vl) [[hd]] ax in
     add_prop_decl tsk Paxiom pr ax