Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- Subject: [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- From: mohamed.iguernelala at ocamlpro.com (Mohamed Iguernelala)
- Date: Tue, 04 Nov 2014 08:04:45 +0100
- In-reply-to: <CAAS2fgRTEAODJ78tg7m77oDEyK4XG0E0GHLRkrqm7tRNFwY3bg@mail.gmail.com>
- References: <CAAS2fgRTEAODJ78tg7m77oDEyK4XG0E0GHLRkrqm7tRNFwY3bg@mail.gmail.com>
Hi,
I looked into one of the unproved VCs
("secp256k1_fe_mul_inner_assert_rte_unsigned_overflow_38" attached),
and I think that it is not valid.
The VC is of the form:
goal overflow_38:
"some context" ->
x_9 <= 67108863 ->
x_10 <= 1073741823 ->
x_9 * x_10 <= 4294967295
So, you are trying to show that "x_9 * x_10 <= 4294967295" always holds
under the given context (i.e. for every
possible values for x_9 and x_10). But this is not true when taking, for
instance, x_9 = 67108863 and x_10 = 1073741823.
Mohamed.
--
Senior R&D Engineer, OCamlPro
Research Associate, VALS team, LRI.
http://www.iguer.info
Le 04/11/2014 00:14, Gregory Maxwell a ?crit :
> Greetings, I haven't used frama-c in some time, it's changed quite a
> bit (and I've likely forgotten even more...) and I'm having a hard
> time making progress with it at all this time around.
>
> I'm working on libsecp256k1 a free software cryptographic signature
> library which will be used by the reference Bitcoin software;
> verifying that optimized implementations are exactly correct is
> critical for this application
>
> I'm trying to prove some simple theorems about some inner kernels used
> for field arithmetic.
>
> To start with, I need to first prove that the code is overflow free,
> under assumptions. (I don't just need to do this to make WP happy, its
> required for correctness of the code.
>
> Here is a reduced testcase that I'm trying:
>
> $ cat a.c
> #include <stdint.h>
> /*@ requires \valid(a + (0..9));
> requires \valid(b + (0..9));
> requires (a[0] < 1073741824);
> requires (a[1] < 1073741824);
> requires (a[2] < 1073741824);
> requires (a[3] < 1073741824);
> requires (a[4] < 1073741824);
> requires (a[5] < 1073741824);
> requires (a[6] < 1073741824);
> requires (a[7] < 1073741824);
> requires (a[8] < 1073741824);
> requires (a[9] < 67108864);
> requires (b[0] < 1073741824);
> requires (b[1] < 1073741824);
> requires (b[2] < 1073741824);
> requires (b[3] < 1073741824);
> requires (b[4] < 1073741824);
> requires (b[5] < 1073741824);
> requires (b[6] < 1073741824);
> requires (b[7] < 1073741824);
> requires (b[8] < 1073741824);
> requires (b[9] < 67108864);
> */
> void static inline secp256k1_fe_mul_inner(const uint32_t *a, const
> uint32_t *b, uint32_t *r) {
> uint64_t d;
> d = (uint64_t)a[0] * b[9]
> + (uint64_t)a[1] * b[8]
> + (uint64_t)a[2] * b[7]
> + (uint64_t)a[3] * b[6]
> + (uint64_t)a[4] * b[5]
> + (uint64_t)a[5] * b[4]
> + (uint64_t)a[6] * b[3]
> + (uint64_t)a[7] * b[2]
> + (uint64_t)a[8] * b[1]
> + (uint64_t)a[9] * b[0];
> }
>
> I invoke frama-c with:
>
> frama-c -main secp256k1_fe_mul_inner -lib-entry -wp -wp-timeout 300
> -wp-par 1 -wp-rte a.c
>
> And get some successful proof for memory access, followed by alt-ergo
> returning unknown on the overflow checks:
> [...]
> [wp] [Alt-Ergo] Goal
> typed_secp256k1_fe_mul_inner_assert_rte_mem_access_20 : Valid
> (Qed:1ms) (93ms) (74)
> [wp] [Alt-Ergo] Goal
> typed_secp256k1_fe_mul_inner_assert_rte_unsigned_overflow : Unknown
> (Qed:4ms) (4s)
> [wp] [Alt-Ergo] Goal
> typed_secp256k1_fe_mul_inner_assert_rte_unsigned_overflow_2 : Unknown
> (Qed:5ms) (4s)
>
> This is obviously free of overflows, since 1073741824*1073741824*8 +
> 1073741824*67108864*2 < 2^64
>
> (but the non-reduced code, is less trivial
> http://0bin.net/paste/tTR7910ESfwij7Ib#pZwnZkivigEp+73f4D4yWQpXMaEWCmVFTb4XxE6vRUN
> ... which is why I'm starting with just proving overflows since the
> hand verifiable correctness proof in the comments assumes no
> overflow).
>
> I'm using alt-ergo 0.95.1 and frama-c Neon-20140301
>
> Any suggestions?
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
-------------- next part --------------
(**************************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(* File modified by CEA (Commissariat ? l'?nergie atomique et aux *)
(* ?nergies alternatives). *)
(* *)
(**************************************************************************)
(* this is a prelude for Alt-Ergo*)
(* this is a prelude for Alt-Ergo integer arithmetic *)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(**************************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(* File modified by CEA (Commissariat ? l'?nergie atomique et aux *)
(* ?nergies alternatives). *)
(* *)
(**************************************************************************)
(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
logic abs_int : int -> int
axiom abs_def : (forall x:int. ((0 <= x) -> (abs_int(x) = x)))
axiom abs_def1 : (forall x:int. ((not (0 <= x)) -> (abs_int(x) = (-x))))
axiom Abs_le :
(forall x:int. forall y:int. ((abs_int(x) <= y) -> ((-y) <= x)))
axiom Abs_le1 : (forall x:int. forall y:int. ((abs_int(x) <= y) -> (x <= y)))
axiom Abs_le2 :
(forall x:int. forall y:int. ((((-y) <= x) and (x <= y)) ->
(abs_int(x) <= y)))
axiom Abs_pos : (forall x:int. (0 <= abs_int(x)))
(**************************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(* File modified by CEA (Commissariat ? l'?nergie atomique et aux *)
(* ?nergies alternatives). *)
(* *)
(**************************************************************************)
(* this is a prelude for Alt-Ergo*)
logic safe_comp_div: int, int -> int
axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y
logic safe_comp_mod: int, int -> int
axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory int_Abs_ must be appended to this file*)
axiom Div_bound :
(forall x:int. forall y:int. (((0 <= x) and (0 < y)) ->
(0 <= safe_comp_div(x,y))))
axiom Div_bound1 :
(forall x:int. forall y:int. (((0 <= x) and (0 < y)) ->
(safe_comp_div(x,y) <= x)))
axiom Div_1 : (forall x:int. (safe_comp_div(x,1) = x))
axiom Mod_1 : (forall x:int. (safe_comp_mod(x,1) = 0))
axiom Div_inf :
(forall x:int. forall y:int. (((0 <= x) and (x < y)) ->
(safe_comp_div(x,y) = 0)))
axiom Mod_inf :
(forall x:int. forall y:int. (((0 <= x) and (x < y)) ->
(safe_comp_mod(x,y) = x)))
axiom Div_mult :
(forall x:int. forall y:int. forall z:int [safe_comp_div(((x * y) + z),x)].
(((0 < x) and ((0 <= y) and (0 <= z))) ->
(safe_comp_div(((x * y) + z),x) = (y + safe_comp_div(z,x)))))
axiom Mod_mult :
(forall x:int. forall y:int. forall z:int [safe_comp_mod(((x * y) + z),x)].
(((0 < x) and ((0 <= y) and (0 <= z))) ->
(safe_comp_mod(((x * y) + z),x) = safe_comp_mod(z,x))))
(**************************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(* File modified by CEA (Commissariat ? l'?nergie atomique et aux *)
(* ?nergies alternatives). *)
(* *)
(**************************************************************************)
(* this is a prelude for Alt-Ergo*)
(* this is a prelude for Alt-Ergo real arithmetic *)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
axiom add_div :
(forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
(((x + y) / z) = ((x / z) + (y / z)))))
axiom sub_div :
(forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
(((x - y) / z) = ((x / z) - (y / z)))))
axiom neg_div :
(forall x:real. forall y:real. ((not (y = 0.0)) ->
(((-x) / y) = (-(x / y)))))
axiom assoc_mul_div :
(forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
(((x * y) / z) = (x * (y / z)))))
axiom assoc_div_mul :
(forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
(not (z = 0.0))) -> (((x / y) / z) = (x / (y * z)))))
axiom assoc_div_div :
(forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
(not (z = 0.0))) -> ((x / (y / z)) = ((x * z) / y))))
(**************************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(* File modified by CEA (Commissariat ? l'?nergie atomique et aux *)
(* ?nergies alternatives). *)
(* *)
(**************************************************************************)
(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
(**************************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(* File modified by CEA (Commissariat ? l'?nergie atomique et aux *)
(* ?nergies alternatives). *)
(* *)
(**************************************************************************)
(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
logic from_int : int -> real
axiom Zero : (from_int(0) = 0.0)
axiom One : (from_int(1) = 1.0)
axiom Add :
(forall x:int. forall y:int.
(from_int((x + y)) = (from_int(x) + from_int(y))))
axiom Sub :
(forall x:int. forall y:int.
(from_int((x - y)) = (from_int(x) - from_int(y))))
axiom Mul :
(forall x:int. forall y:int.
(from_int((x * y)) = (from_int(x) * from_int(y))))
axiom Neg : (forall x:int. (from_int((-x)) = (-from_int(x))))
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2014 *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory bool_Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory int_Abs_ must be appended to this file*)
(** The theory int_ComputerDivision_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
(** The theory real_RealInfix_ must be appended to this file*)
(** The theory real_FromInt_ must be appended to this file*)
logic ite : bool, 'a, 'a -> 'a
axiom ite1 :
(forall p:bool. forall x:'a. forall y:'a [ite(p, x, y)]. (((p = true) and
(ite(p, x, y) = x)) or ((p = false) and (ite(p, x, y) = y))))
logic eqb : 'a, 'a -> bool
axiom eqb1 : (forall x:'a. forall y:'a. ((eqb(x, y) = true) -> (x = y)))
axiom eqb2 : (forall x:'a. forall y:'a. ((x = y) -> (eqb(x, y) = true)))
logic neqb : 'a, 'a -> bool
axiom neqb1 :
(forall x:'a. forall y:'a. ((neqb(x, y) = true) -> (not (x = y))))
axiom neqb2 :
(forall x:'a. forall y:'a. ((not (x = y)) -> (neqb(x, y) = true)))
logic zlt : int, int -> bool
logic zleq : int, int -> bool
axiom zlt1 : (forall x:int. forall y:int. ((zlt(x, y) = true) -> (x < y)))
axiom zlt2 : (forall x:int. forall y:int. ((x < y) -> (zlt(x, y) = true)))
axiom zleq1 : (forall x:int. forall y:int. ((zleq(x, y) = true) -> (x <= y)))
axiom zleq2 : (forall x:int. forall y:int. ((x <= y) -> (zleq(x, y) = true)))
logic rlt : real, real -> bool
logic rleq : real, real -> bool
axiom rlt1 : (forall x:real. forall y:real. ((rlt(x, y) = true) -> (x < y)))
axiom rlt2 : (forall x:real. forall y:real. ((x < y) -> (rlt(x, y) = true)))
axiom rleq1 :
(forall x:real. forall y:real. ((rleq(x, y) = true) -> (x <= y)))
axiom rleq2 :
(forall x:real. forall y:real. ((x <= y) -> (rleq(x, y) = true)))
logic truncate : real -> int
function real_of_int(x: int) : real = from_int(x)
axiom truncate_of_int : (forall x:int. (truncate(real_of_int(x)) = x))
axiom c_euclidian :
(forall n:int. forall d:int [safe_comp_div(n,d), safe_comp_mod(n,d)].
((not (d = 0)) -> (n = ((safe_comp_div(n,d) * d) + safe_comp_mod(n,d)))))
axiom cdiv_cases :
(forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((0 < d) ->
(safe_comp_div(n,d) = (n / d)))))
axiom cdiv_cases1 :
(forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((0 < d) ->
(safe_comp_div(n,d) = (-((-n) / d))))))
axiom cdiv_cases2 :
(forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((d < 0) ->
(safe_comp_div(n,d) = (-(n / (-d)))))))
axiom cdiv_cases3 :
(forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((d < 0) ->
(safe_comp_div(n,d) = ((-n) / (-d))))))
axiom cmod_cases :
(forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 < d) ->
(safe_comp_mod(n,d) = (n % d)))))
axiom cmod_cases1 :
(forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 < d) ->
(safe_comp_mod(n,d) = (-((-n) % d))))))
axiom cmod_cases2 :
(forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d < 0) ->
(safe_comp_mod(n,d) = (n % (-d))))))
axiom cmod_cases3 :
(forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d < 0) ->
(safe_comp_mod(n,d) = (-((-n) % (-d)))))))
axiom cmod_remainder :
(forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 < d) ->
(0 <= safe_comp_mod(n,d)))))
axiom cmod_remainder1 :
(forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 < d) ->
(safe_comp_mod(n,d) < d))))
axiom cmod_remainder2 :
(forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 < d) ->
((-d) < safe_comp_mod(n,d)))))
axiom cmod_remainder3 :
(forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 < d) ->
(safe_comp_mod(n,d) <= 0))))
axiom cmod_remainder4 :
(forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d < 0) ->
(0 <= safe_comp_mod(n,d)))))
axiom cmod_remainder5 :
(forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d < 0) ->
(safe_comp_mod(n,d) < (-d)))))
axiom cmod_remainder6 :
(forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d < 0) ->
(d < safe_comp_mod(n,d)))))
axiom cmod_remainder7 :
(forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d < 0) ->
(safe_comp_mod(n,d) <= 0))))
axiom cdiv_neutral :
(forall a:int [safe_comp_div(a,1)]. (safe_comp_div(a,1) = a))
axiom cdiv_inv :
(forall a:int [safe_comp_div(a,a)]. ((not (a = 0)) ->
(safe_comp_div(a,a) = 1)))
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2014 *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory bool_Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory map_Map_ must be appended to this file*)
type addr = { base : int; offset : int
}
logic addr_le : addr, addr -> prop
logic addr_lt : addr, addr -> prop
logic addr_le_bool : addr, addr -> bool
logic addr_lt_bool : addr, addr -> bool
axiom addr_le_def :
(forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
(addr_le(p, q) -> ((p).offset <= (q).offset))))
axiom addr_le_def1 :
(forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
(((p).offset <= (q).offset) -> addr_le(p, q))))
axiom addr_lt_def :
(forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) ->
(addr_lt(p, q) -> ((p).offset < (q).offset))))
axiom addr_lt_def1 :
(forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) ->
(((p).offset < (q).offset) -> addr_lt(p, q))))
axiom addr_le_bool_def :
(forall p:addr. forall q:addr [addr_le_bool(p, q)]. (addr_le(p, q) ->
(addr_le_bool(p, q) = true)))
axiom addr_le_bool_def1 :
(forall p:addr. forall q:addr [addr_le_bool(p, q)]. ((addr_le_bool(p,
q) = true) -> addr_le(p, q)))
axiom addr_lt_bool_def :
(forall p:addr. forall q:addr [addr_lt_bool(p, q)]. (addr_lt(p, q) ->
(addr_lt_bool(p, q) = true)))
axiom addr_lt_bool_def1 :
(forall p:addr. forall q:addr [addr_lt_bool(p, q)]. ((addr_lt_bool(p,
q) = true) -> addr_lt(p, q)))
function null() : addr = { base = 0; offset = 0 }
function global(b: int) : addr = { base = b; offset = 0 }
function shift(p: addr, k: int) : addr = { base = (p).base; offset =
((p).offset + k) }
predicate included(p: addr, a: int, q: addr, b: int) = ((0 < a) ->
((0 <= b) and (((p).base = (q).base) and (((q).offset <= (p).offset) and
(((p).offset + a) <= ((q).offset + b))))))
predicate separated(p: addr, a: int, q: addr, b: int) = ((a <= 0) or
((b <= 0) or ((not ((p).base = (q).base)) or
((((q).offset + b) <= (p).offset) or (((p).offset + a) <= (q).offset)))))
predicate eqmem(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr,
a1: int) =
(forall q:addr [(m1[p])| (m2[q])]. (included(q, 1, p, a1) ->
((m1[q]) = (m2[q]))))
predicate havoc(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr,
a1: int) =
(forall q:addr [(m1[p])| (m2[q])]. (separated(q, 1, p, a1) ->
((m1[q]) = (m2[q]))))
predicate valid_rd(m: (int,int) farray, p: addr, n: int) = ((0 < n) ->
((0 <= (p).offset) and (((p).offset + n) <= (m[(p).base]))))
predicate valid_rw(m: (int,int) farray, p: addr, n: int) = ((0 < n) ->
((0 < (p).base) and ((0 <= (p).offset) and
(((p).offset + n) <= (m[(p).base])))))
axiom valid_rw_rd :
(forall m:(int,int) farray.
(forall p:addr. (forall n:int. (valid_rw(m, p, n) -> valid_rd(m, p, n)))))
axiom valid_string :
(forall m:(int,int) farray.
(forall p:addr. (((p).base < 0) -> (((0 <= (p).offset) and
((p).offset < (m[(p).base]))) -> valid_rd(m, p, 1)))))
axiom valid_string1 :
(forall m:(int,int) farray.
(forall p:addr. (((p).base < 0) -> (((0 <= (p).offset) and
((p).offset < (m[(p).base]))) -> (not valid_rw(m, p, 1))))))
axiom separated_1 :
(forall p:addr. forall q:addr.
(forall a:int. forall b:int. forall i:int. forall j:int [separated(p, a, q,
b), { base = (p).base; offset = i }, { base = (q).base; offset = j }].
(separated(p, a, q, b) -> ((((p).offset <= i) and
(i < ((p).offset + a))) -> ((((q).offset <= j) and
(j < ((q).offset + b))) -> (not ({ base = (p).base; offset = i } = {
base = (q).base; offset = j })))))))
logic region : int -> int
logic linked : (int,int) farray -> prop
logic sconst : (addr,int) farray -> prop
predicate framed(m: (addr,addr) farray) =
(forall p:addr [(m[p])]. (region(((m[p])).base) <= 0))
axiom separated_included :
(forall p:addr. forall q:addr.
(forall a:int. forall b:int [separated(p, a, q, b), included(p, a, q, b)].
((0 < a) -> ((0 < b) -> (separated(p, a, q, b) -> (not included(p, a, q,
b)))))))
axiom included_trans :
(forall p:addr. forall q:addr. forall r:addr.
(forall a:int. forall b:int. forall c:int [included(p, a, q, b),
included(q, b, r, c)]. (included(p, a, q, b) -> (included(q, b, r, c) ->
included(p, a, r, c)))))
axiom separated_trans :
(forall p:addr. forall q:addr. forall r:addr.
(forall a:int. forall b:int. forall c:int [included(p, a, q, b),
separated(q, b, r, c)]. (included(p, a, q, b) -> (separated(q, b, r, c) ->
separated(p, a, r, c)))))
axiom separated_sym :
(forall p:addr. forall q:addr.
(forall a:int. forall b:int [separated(p, a, q, b)]. (separated(p, a, q,
b) -> separated(q, b, p, a))))
axiom separated_sym1 :
(forall p:addr. forall q:addr.
(forall a:int. forall b:int [separated(p, a, q, b)]. (separated(q, b, p,
a) -> separated(p, a, q, b))))
axiom eqmem_included :
(forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
(forall p:addr. forall q:addr.
(forall a1:int. forall b:int [eqmem(m1, m2, p, a1), eqmem(m1, m2, q, b)].
(included(p, a1, q, b) -> (eqmem(m1, m2, q, b) -> eqmem(m1, m2, p, a1))))))
axiom eqmem_sym :
(forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
(forall p:addr.
(forall a1:int. (eqmem(m1, m2, p, a1) -> eqmem(m2, m1, p, a1)))))
axiom havoc_sym :
(forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
(forall p:addr.
(forall a1:int. (havoc(m1, m2, p, a1) -> havoc(m2, m1, p, a1)))))
logic cast : addr -> int
axiom cast_injective :
(forall p:addr. forall q:addr [cast(p), cast(q)]. ((cast(p) = cast(q)) ->
(p = q)))
logic hardware : int -> int
axiom hardnull : (hardware(0) = 0)
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2014 *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory bool_Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
logic is_uint8 : int -> prop
axiom is_uint8_def : (forall x:int [is_uint8(x)]. (is_uint8(x) -> (0 <= x)))
axiom is_uint8_def1 :
(forall x:int [is_uint8(x)]. (is_uint8(x) -> (x < 256)))
axiom is_uint8_def2 :
(forall x:int [is_uint8(x)]. (((0 <= x) and (x < 256)) -> is_uint8(x)))
logic is_sint8 : int -> prop
axiom is_sint8_def :
(forall x:int [is_sint8(x)]. (is_sint8(x) -> ((-128) <= x)))
axiom is_sint8_def1 :
(forall x:int [is_sint8(x)]. (is_sint8(x) -> (x < 128)))
axiom is_sint8_def2 :
(forall x:int [is_sint8(x)]. ((((-128) <= x) and (x < 128)) ->
is_sint8(x)))
logic is_uint16 : int -> prop
axiom is_uint16_def :
(forall x:int [is_uint16(x)]. (is_uint16(x) -> (0 <= x)))
axiom is_uint16_def1 :
(forall x:int [is_uint16(x)]. (is_uint16(x) -> (x < 65536)))
axiom is_uint16_def2 :
(forall x:int [is_uint16(x)]. (((0 <= x) and (x < 65536)) ->
is_uint16(x)))
predicate is_sint16(x: int) = (((-32768) <= x) and (x < 32768))
logic is_uint32 : int -> prop
axiom is_uint32_def :
(forall x:int [is_uint32(x)]. (is_uint32(x) -> (0 <= x)))
axiom is_uint32_def1 :
(forall x:int [is_uint32(x)]. (is_uint32(x) -> (x < 4294967296)))
axiom is_uint32_def2 :
(forall x:int [is_uint32(x)]. (((0 <= x) and (x < 4294967296)) ->
is_uint32(x)))
logic is_sint32 : int -> prop
axiom is_sint32_def :
(forall x:int [is_sint32(x)]. (is_sint32(x) -> ((-2147483648) <= x)))
axiom is_sint32_def1 :
(forall x:int [is_sint32(x)]. (is_sint32(x) -> (x < 2147483648)))
axiom is_sint32_def2 :
(forall x:int [is_sint32(x)]. ((((-2147483648) <= x) and
(x < 2147483648)) -> is_sint32(x)))
logic is_uint64 : int -> prop
axiom is_uint64_def :
(forall x:int [is_uint64(x)]. (is_uint64(x) -> (0 <= x)))
axiom is_uint64_def1 :
(forall x:int [is_uint64(x)]. (is_uint64(x) ->
(x < 18446744073709551616)))
axiom is_uint64_def2 :
(forall x:int [is_uint64(x)]. (((0 <= x) and
(x < 18446744073709551616)) -> is_uint64(x)))
logic is_sint64 : int -> prop
axiom is_sint64_def :
(forall x:int [is_sint64(x)]. (is_sint64(x) ->
((-9223372036854775808) <= x)))
axiom is_sint64_def1 :
(forall x:int [is_sint64(x)]. (is_sint64(x) -> (x < 9223372036854775808)))
axiom is_sint64_def2 :
(forall x:int [is_sint64(x)]. ((((-9223372036854775808) <= x) and
(x < 9223372036854775808)) -> is_sint64(x)))
logic to_uint8 : int -> int
logic to_sint8 : int -> int
logic to_uint16 : int -> int
logic to_sint16 : int -> int
logic to_uint32 : int -> int
logic to_sint32 : int -> int
logic to_uint64 : int -> int
logic to_sint64 : int -> int
axiom is_to_uint8 :
(forall x:int [is_uint8(to_uint8(x))]. is_uint8(to_uint8(x)))
axiom is_to_sint8 :
(forall x:int [is_sint8(to_sint8(x))]. is_sint8(to_sint8(x)))
axiom is_to_uint16 :
(forall x:int [is_uint16(to_uint16(x))]. is_uint16(to_uint16(x)))
axiom is_to_sint16 :
(forall x:int [is_sint16(to_sint16(x))]. is_sint16(to_sint16(x)))
axiom is_to_uint32 :
(forall x:int [is_uint32(to_uint32(x))]. is_uint32(to_uint32(x)))
axiom is_to_sint32 :
(forall x:int [is_sint32(to_sint32(x))]. is_sint32(to_sint32(x)))
axiom is_to_uint64 :
(forall x:int [is_uint64(to_uint64(x))]. is_uint64(to_uint64(x)))
axiom is_to_sint64 :
(forall x:int [is_sint64(to_sint64(x))]. is_sint64(to_sint64(x)))
axiom id_uint8 :
(forall x:int [to_uint8(x)]. (((0 <= x) and (x < 256)) ->
(to_uint8(x) = x)))
axiom id_sint8 :
(forall x:int [to_sint8(x)]. ((((-128) <= x) and (x < 128)) ->
(to_sint8(x) = x)))
axiom id_uint16 :
(forall x:int [to_uint16(x)]. (((0 <= x) and (x < 65536)) ->
(to_uint16(x) = x)))
axiom id_sint16 :
(forall x:int [to_sint16(x)]. ((((-32768) <= x) and (x < 32768)) ->
(to_sint16(x) = x)))
axiom id_uint32 :
(forall x:int [to_uint32(x)]. (((0 <= x) and (x < 4294967296)) ->
(to_uint32(x) = x)))
axiom id_sint32 :
(forall x:int [to_sint32(x)]. ((((-2147483648) <= x) and
(x < 2147483648)) -> (to_sint32(x) = x)))
axiom id_uint64 :
(forall x:int [to_uint64(x)]. (((0 <= x) and
(x < 18446744073709551616)) -> (to_uint64(x) = x)))
axiom id_sint64 :
(forall x:int [to_sint64(x)]. ((((-9223372036854775808) <= x) and
(x < 9223372036854775808)) -> (to_sint64(x) = x)))
logic lnot : int -> int
logic ac land : int, int -> int
logic ac lxor : int, int -> int
logic ac lor : int, int -> int
logic lsl : int, int -> int
logic lsr : int, int -> int
logic bit_testb : int, int -> bool
logic bit_test : int, int -> prop
(* ---------------------------------------------------------- *)
(* --- Assertion 'rte,unsigned_overflow' (file a.c, line 37) --- *)
(* ---------------------------------------------------------- *)
goal secp256k1_fe_mul_inner_assert_rte_unsigned_overflow_38:
forall Malloc_0 : int farray.
forall Mint_0 : (addr,int) farray.
forall a_0,b_0 : addr.
let a_1 = shift(a_0, 0) : addr in
let x_0 = Mint_0[a_1] : int in
let x_1 = Mint_0[shift(a_0, 1)] : int in
let x_2 = Mint_0[shift(a_0, 2)] : int in
let x_3 = Mint_0[shift(a_0, 3)] : int in
let x_4 = Mint_0[shift(a_0, 4)] : int in
let x_5 = Mint_0[shift(a_0, 5)] : int in
let x_6 = Mint_0[shift(a_0, 6)] : int in
let x_7 = Mint_0[shift(a_0, 7)] : int in
let x_8 = Mint_0[shift(a_0, 8)] : int in
let x_9 = Mint_0[shift(a_0, 9)] : int in
let a_2 = shift(b_0, 0) : addr in
let x_10 = Mint_0[a_2] : int in
let x_11 = Mint_0[shift(b_0, 1)] : int in
let x_12 = Mint_0[shift(b_0, 2)] : int in
let x_13 = Mint_0[shift(b_0, 3)] : int in
let x_14 = Mint_0[shift(b_0, 4)] : int in
let x_15 = Mint_0[shift(b_0, 5)] : int in
let x_16 = Mint_0[shift(b_0, 6)] : int in
let x_17 = Mint_0[shift(b_0, 7)] : int in
let x_18 = Mint_0[shift(b_0, 8)] : int in
let x_19 = Mint_0[shift(b_0, 9)] : int in
linked(Malloc_0) ->
(x_0 <= 1073741823) ->
(x_1 <= 1073741823) ->
(x_2 <= 1073741823) ->
(x_3 <= 1073741823) ->
(x_4 <= 1073741823) ->
(x_5 <= 1073741823) ->
(x_6 <= 1073741823) ->
(x_7 <= 1073741823) ->
(x_8 <= 1073741823) ->
(x_9 <= 67108863) ->
(x_10 <= 1073741823) ->
(x_11 <= 1073741823) ->
(x_12 <= 1073741823) ->
(x_13 <= 1073741823) ->
(x_14 <= 1073741823) ->
(x_15 <= 1073741823) ->
(x_16 <= 1073741823) ->
(x_17 <= 1073741823) ->
(x_18 <= 1073741823) ->
(x_19 <= 67108863) ->
is_uint32(x_0) ->
is_uint32(x_1) ->
is_uint32(x_2) ->
is_uint32(x_3) ->
is_uint32(x_4) ->
is_uint32(x_5) ->
is_uint32(x_6) ->
is_uint32(x_7) ->
is_uint32(x_8) ->
is_uint32(x_9) ->
is_uint32(x_10) ->
is_uint32(x_11) ->
is_uint32(x_12) ->
is_uint32(x_13) ->
is_uint32(x_14) ->
is_uint32(x_15) ->
is_uint32(x_16) ->
is_uint32(x_17) ->
is_uint32(x_18) ->
is_uint32(x_19) ->
valid_rw(Malloc_0, a_1, 10) ->
valid_rw(Malloc_0, a_2, 10) ->
((x_9 * x_10) <= 4294967295)
- Follow-Ups:
- [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- From: gmaxwell at gmail.com (Gregory Maxwell)
- [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- References:
- [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- From: gmaxwell at gmail.com (Gregory Maxwell)
- [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- Prev by Date: [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- Next by Date: [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- Previous by thread: [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- Next by thread: [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- Index(es):