Frama-C eklenti geliştirmesi: Özdeğerlik analizi sonucu OCaml tam sayıları

Question

Bu iki iletiyi okudum: Getting result of value analysis ve Getting the values of statement. Bu iki gönderi, baskısı'un değer analizinin değerleriyle ilgili nasıl paha biçilemez bilgiler sağlar.

Ancak, benim görev değer değişkeninde saklanan tamsayılar ayıklamak ve ardından tamsayılar (sadece tamsayı değerleri ile endişeli olurum) ile bazı matematik yapmamı gerektiriyor. Örneğin, bazı değişkenler için değer analizi sonucu {1, 2} ise, sonucu bir tamsayılar listesi olarak almak istiyorum: [1, 2]. Bu şekilde onunla matematik yapabilirim. Sonuç bir aralık içeriyorsa, bunun üstesinden gelmek için bir tür tanımlayabilirim. Örneğin, değer değişkeninin

type point_or_interval = 
| Point of int 
| Interval of int * int 

tipi belgelerinde type t = Cvalue.V.t olarak tanımlanır. Bu modülü kaynakta bulamadım, bu yüzden değeri nasıl kullanacağımı ve ihtiyacım olan bilgiyi nasıl çıkaracağımı bilmiyorum. Bunu nasıl yapmalıyım? Bir kod resmi takdir edilecektir!

Düzenleme: Aşağıdaki kodu çalıştılar. Bu kod, Getting result of value analysis'dan, pretty_vi işlevindeki bazı değişikliklerle birlikte verbatim kopyalanır. Test giriş programımda çalışmıyor - Locations.Location_Bytes.find_lonely_key işlevi Not_found istisnasını yükseltti. Giriş programım da eklenmiştir.

open Cil_types 

(* Prints the value associated to variable [vi] before [stmt]. *) 
let pretty_vi fmt stmt vi = 
    let kinstr = Kstmt stmt in (* make a kinstr from a stmt *) 
    let lval = (Var vi, NoOffset) in (* make an lval from a varinfo *) 
    let loc = (* make a location from a kinstr + an lval *) 
    !Db.Value.lval_to_loc kinstr ~with_alarms:CilE.warn_none_mode lval 
    in  
    Db.Value.fold_state_callstack 
    (fun state() -> 
     (* for each state in the callstack *) 
     let value = Db.Value.find state loc in (* obtain value for location *) 
     let base, offset = Locations.Location_Bytes.find_lonely_key value in 
     (match offset with 
     | Ival.Set _ ->() 
     | Ival.Float _ ->() 
     | Ival.Top (_, _, _, _)->()); 
     Format.fprintf fmt "%a -> %a@." Printer.pp_varinfo vi 
     Db.Value.pretty value (* print mapping *) 
    )() ~after:false kinstr 

(* Prints the state at statement [stmt] for each local variable in [kf], 
    and for each global variable. *) 
let pretty_local_and_global_vars kf fmt stmt = 
    let locals = Kernel_function.get_locals kf in 
    List.iter (fun vi -> pretty_vi fmt stmt vi) locals (*; 
    Globals.Vars.iter (fun vi _ -> pretty_vi fmt stmt vi) *) 

(* Visits each statement in [kf] and prints the result of Value before the 
    statement. *) 
class stmt_val_visitor kf = 
    object (self) 
    inherit Visitor.frama_c_inplace 
    method! vstmt_aux stmt = 
     (match stmt.skind with 
     | Instr _ -> 
     Format.printf "state for all variables before stmt: %a@.%a@." 
      Printer.pp_stmt stmt (pretty_local_and_global_vars kf) stmt 
     | _ ->()); 
     Cil.DoChildren 
    end 

(* usage: frama-c file.c -load-script print_vals.ml *) 
let() = 
    Db.Main.extend (fun() -> 
     Format.printf "computing value...@."; 
     !Db.Value.compute(); 
     let fun_name = "main" in 
     Format.printf "visiting function: %s@." fun_name; 
     let kf_vis = new stmt_val_visitor in 
     let kf = Globals.Functions.find_by_name fun_name in 
     let fundec = Kernel_function.get_definition kf in 
     ignore (Visitor.visitFramacFunction (kf_vis kf) fundec); 
     Format.printf "done!@.") 

Test girişi programı:

#include <stdio.h> 

int main() { 
    int a = 1; 
    return 0; 
} 

bu kodla problemi nedir? Değer eşlemesi neden bulunamadı?

Answer 1

Genel açıklama: Merlin'u destekleyen bir düzenleyici kullanıyorsanız, bunu kullanmanızı kesinlikle öneriyorum. Hangi modül modüllerinin tanımlandığını, hangi türlerin eş anlamlı olduğunu ve otomatik tamamlama aracıyla birleştiğini bulmayı kolaylaştırır Merlin, dönüşüm işlevlerini çok daha kolay bulmanızı sağlar.

Özellikle, Merlin, (örneğin, bir gösterici değil, dönüştürülebilen değerini alan) Eğer Cvalue.V.project_ival : V.t -> Ival.t bir Ival.t bir V.t dönüştürür öğrenmek yardımcı olmalıdır.

Ival.t

temsil sofistike bir aralık benzeri bir değerdir:

• kayan nokta değerleri bitişik bir aralık (Ival.Float);
• küçük bir tam sayı kümesi (Ival.Set);
• ya da bir gerçek tamsayı aralığı (isme rağmen Ival.Top), uyum bilgisi ve isteğe bağlı sınırlarla, örn. [9..--]1%4, {x ∈ ℕ | x ≥ 9 ∧ x mod 4 = 1}'u temsil eder.

Fonksiyon Ival.min_and_max : Ival.t -> Integer.t option * Integer.t option aksi Some min vardır (eksi sonsuz) bir alt sınır arasında olması durumunda veya maybe_minNone olan bir çift (maybe_min, maybe_max), (bir kayan nokta aralığı içermeyen aralığını varsayılarak) bir Ival.t ve döner alır ve maybe max için simetrik olarak. Her ikisi de Ival.Set ve Ival.Top ile çalışır.

Integer.t'un makine tamsayıları değil, rastgele kesinlikli tamsayıların bir uygulaması olduğunu unutmayın.