İmzasız tamsayı taşmasına dayanan kod kanıtları mı?

Question

Bazı verimsizlikten kaçınmak için modüler aritmetiğe dayanan aşağıdaki gibi kodun doğruluğunu kanıtlamaya nasıl yaklaşmalıyım?

#include <stdint.h> 

uint32_t my_add(uint32_t a, uint32_t b) { 
    uint32_t r = a + b; 
    if (r < a) 
     return UINT32_MAX; 
    return r; 
} 

eğer doğru anlamak ben, RP'nin "int" modeliyle denedi, ancak ettik o modeli PO'lara mantıksal tamsayılar anlamlandırmasını C kodunun değil biçimsel modeller yapılandırır. Örneğin, WP ve RTE eklentileri hala "int" modeli kullanılırken yukarıdaki imzasız ekleme için taşma savı PO'larını gerektirir ve enjekte eder.

Böyle durumlarda, bir deyim veya temel blok için mantıksal bir model öngören ek açıklamalar ekleyebilirim, bu yüzden Frama-C'ye belirli bir derleyicinin gerçekten bir ifadeyi nasıl yorumladığını söyleyebilirim? Öyleyse, imzasız sarmalayıcı, derleyici tanımlı davranışlar, standart olmayan davranışlar (satır içi assy?), Vb. Gibi tanımlanmış ama çoğu kez kusurlu indükleyici davranışlar gibi diğer doğrulama tekniklerini kullanabilirim. çevreleyen kod. Bazı özelliklerin kendileri için özellikleri elde edemedikleri zaman tuttukları bazı statik analizcileri bilgilendirmek için kullanılan "assert düzeltme" ye benzer (ama daha güçlü) bir resim çiziyorum.

Alt-ergo 95.1 ile referans için Frama-C Fluorine-20130601 ile çalışıyorum.

Answer 1

Ben Frama-C Florlu-20130601 son sürümünü kullanmak için bir yol bulmuş olduğunu görmekten

ile çalışıyorum.

Jessie vardır:

#pragma JessieIntegerModel(modulo) 

yukarıdaki Pragma o düşünün yapar İşte

tamamen sorunuza cevap yok rağmen, bir StackOverflow yorumunu sığmayan, bu bilgilerin bazıları rasgele parçalarıdır tüm taşmalar (hem tanımlanmamış imzalılar hem de tanımlanmış imzasızlar) etrafa sarılır (2'nin tamamlayıcı aritmetiğinde imzalı taşmalarla aynı). Oluşturulan kanıt yükümlülükleri çok daha zordur çünkü her yerde ek modulo işlemleri içerirler. Otomatik teorem geliştiricilerinden, genellikle yalnızca Basitleştir, onlarla bir şeyler yapabilir. Florlu yılında

, RTE varsayılan olarak + b hakkında uyarmak değildir:

$ frama-c -rte t.c -then -print 
[kernel] preprocessing with "gcc -C -E -I. t.c" 
[rte] annotating function my_add 
/* Generated by Frama-C */ 
typedef unsigned int uint32_t; 
uint32_t my_add(uint32_t a, uint32_t b) 
{ 
    uint32_t __retres; 
    uint32_t r; 
    r = a + b; 
    if (r < a) { 
    __retres = 4294967295U; 
    goto return_label; 
    } 
    __retres = r; 
    return_label: return __retres; 
} 

RTE seçeneğiyle -warn-unsigned-overflow bulunan imzasız ek hakkında uyarmak için yapılabilir

:

$ frama-c -warn-unsigned-overflow -rte t.c -then -print 
[kernel] preprocessing with "gcc -C -E -I. t.c" 
[rte] annotating function my_add 
/* Generated by Frama-C */ 
typedef unsigned int uint32_t; 
uint32_t my_add(uint32_t a, uint32_t b) 
{ 
    uint32_t __retres; 
    uint32_t r; 
    /*@ assert rte: unsigned_overflow: 0 ≤ a+b; */ 
    /*@ assert rte: unsigned_overflow: a+b ≤ 4294967295; */ 
    r = a + b; 
    … 

Ama bu kesinlikle var İstediğin şeyin tersine, bunu neden yaptığını anlamıyorum.

Answer 2

Kullandığınız komut satırını tam olarak vermediniz. Sanırım bu frama-c -wp -wp-rte file.c -pp-annot. Bu durumda, gerçekten, RTE'nin yaydığı tüm iddialar üretilir. Bununla birlikte, daha iyi bir kontrole sahip olabilirsiniz, frama-c'ye ilk olarak yalnızca ilgilendiğiniz RTE kategorilerini üretmesi talimatı verin (iki çeşit seçenek tarafından kontrol edildiğine dikkat edin: frama-c -rte-help ve -warn-{signed,unsigned}-{overflow,downcast} tanımlanmış olanlar kernel'de) ve sonuçta wp'yi başlatın.

/*@ 
    behavior no_overflow: 
    assumes a + b <= UINT32_MAX; 
    ensures \result == a+b; 
    behavior saturate: 
    assumes a+b > UINT32_MAX; 
    ensures \result == UINT32_MAX; 
*/ 
uint32_t my_add(uint32_t a,uint32_t b);