From e7e1e2ed84c33e58103fcc0fc977b3e97adb8a58 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 18 Sep 2024 10:46:22 +0200
Subject: [PATCH] [wp] plug the MemBytes model
---
src/plugins/wp/Factory.ml | 19 ++++++++++++++++++-
src/plugins/wp/Factory.mli | 2 +-
src/plugins/wp/gui/GuiPanel.ml | 6 +++++-
src/plugins/wp/wp.ml | 1 +
4 files changed, 25 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 488ce673bc4..f173e8b2e0b 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva
+type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva | Bytes
type mvar = Raw | Var | Ref | Caveat
type setup = {
@@ -68,6 +68,7 @@ let descr_mheap d = function
| Hoare -> main d "hoare"
| Typed p -> main d "typed" ; descr_mtyped d p
| Eva -> main d "eva"
+ | Bytes -> main d "bytes"
let descr_mvar d = function
| Var -> ()
@@ -205,6 +206,8 @@ module Model_Hoare_Raw = Register(MemVar.Raw)(MemEmpty)
module Model_Hoare_Ref = Register(Ref)(MemEmpty)
module Model_Typed_Var = Register(Var)(MemTyped)
module Model_Typed_Ref = Register(Ref)(MemTyped)
+module Model_Bytes_Var = Register(Var)(MemBytes)
+module Model_Bytes_Ref = Register(Ref)(MemBytes)
module Model_Caveat = Register(Caveat)(MemTyped)
module MemVal = MemVal.Make(MemVal.Eva)
@@ -218,12 +221,20 @@ struct
end
module Comp_MemZeroAlias = MakeCompiler(MemZeroAlias)
+
module Comp_Hoare_Raw = MakeCompiler(Model_Hoare_Raw)
module Comp_Hoare_Ref = MakeCompiler(Model_Hoare_Ref)
+
module Comp_MemTyped = MakeCompiler(MemTyped)
module Comp_Typed_Var = MakeCompiler(Model_Typed_Var)
module Comp_Typed_Ref = MakeCompiler(Model_Typed_Ref)
+
module Comp_Caveat = MakeCompiler(Model_Caveat)
+
+module Comp_MemBytes = MakeCompiler(MemBytes)
+module Comp_Bytes_Var = MakeCompiler(Model_Bytes_Var)
+module Comp_Bytes_Ref = MakeCompiler(Model_Bytes_Ref)
+
module Comp_MemVal = MakeCompiler(MemVal)
@@ -237,6 +248,10 @@ let compiler mheap mvar : (module Sigs.Compiler) =
| Typed _ , Var -> (module Comp_Typed_Var)
| Typed _ , Ref -> (module Comp_Typed_Ref)
| Eva, _ -> (module Comp_MemVal)
+ | Bytes, Raw -> (module Comp_MemBytes)
+ | Bytes, Var -> (module Comp_Bytes_Var)
+ | Bytes, Ref -> (module Comp_Bytes_Ref)
+
(* -------------------------------------------------------------------------- *)
(* --- Tuning --- *)
@@ -246,6 +261,7 @@ let configure_mheap = function
| Hoare -> MemEmpty.configure ()
| ZeroAlias -> MemZeroAlias.configure ()
| Eva -> MemVal.configure ()
+ | Bytes -> MemBytes.configure ()
| Typed p ->
let rollback_memtyped = MemTyped.configure () in
let orig_memtyped_pointer = Context.push MemTyped.pointer p in
@@ -330,6 +346,7 @@ let update_config ~warning m s = function
| "CAST" -> { s with mheap = Typed MemTyped.Unsafe }
| "NOCAST" -> { s with mheap = Typed MemTyped.NoCast }
| "EVA" -> { s with mheap = Eva }
+ | "BYTES" -> { s with mheap = Bytes }
| "CAVEAT" -> { s with mvar = Caveat }
| "RAW" -> { s with mvar = Raw }
| "REF" -> { s with mvar = Ref }
diff --git a/src/plugins/wp/Factory.mli b/src/plugins/wp/Factory.mli
index dc9e29707e3..1b9ac3843c2 100644
--- a/src/plugins/wp/Factory.mli
+++ b/src/plugins/wp/Factory.mli
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva
+type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva | Bytes
type mvar = Raw | Var | Ref | Caveat
type setup = {
diff --git a/src/plugins/wp/gui/GuiPanel.ml b/src/plugins/wp/gui/GuiPanel.ml
index 8292028a5c6..fb7171d4252 100644
--- a/src/plugins/wp/gui/GuiPanel.ml
+++ b/src/plugins/wp/gui/GuiPanel.ml
@@ -99,7 +99,7 @@ let run_and_prove
(* --- Model Panel --- *)
(* ------------------------------------------------------------------------ *)
-type memory = TREE | HOARE | TYPED | EVA
+type memory = TREE | HOARE | TYPED | EVA | BYTES
class model_selector (main : Design.main_window_extension_points) =
let dialog = new Wpane.dialog
@@ -107,6 +107,7 @@ class model_selector (main : Design.main_window_extension_points) =
let memory = new Widget.group HOARE in
let r_hoare = memory#add_radio ~label:"Hoare Memory Model" ~value:HOARE () in
let r_typed = memory#add_radio ~label:"Typed Memory Model" ~value:TYPED () in
+ let r_bytes = memory#add_radio ~label:"Bytes Memory Model" ~value:BYTES () in
let r_eva = memory#add_radio ~label:"Eva Memory Model" ~value:EVA () in
let c_casts = new Widget.checkbox ~label:"Unsafe casts" () in
let c_byref = new Widget.checkbox ~label:"Reference Arguments" () in
@@ -120,6 +121,7 @@ class model_selector (main : Design.main_window_extension_points) =
begin
dialog#add_row r_hoare#coerce ;
dialog#add_row r_typed#coerce ;
+ dialog#add_row r_bytes#coerce ;
dialog#add_row r_eva#coerce ;
dialog#add_row c_casts#coerce ;
dialog#add_row c_byref#coerce ;
@@ -148,6 +150,7 @@ class model_selector (main : Design.main_window_extension_points) =
| Hoare -> memory#set HOARE
| Typed m -> memory#set TYPED ; c_casts#set (m = MemTyped.Unsafe)
| Eva -> memory#set EVA
+ | Bytes -> memory#set BYTES
) ;
c_byref#set (s.mvar = Ref) ;
c_ctxt#set (s.mvar = Caveat) ;
@@ -162,6 +165,7 @@ class model_selector (main : Design.main_window_extension_points) =
| TYPED -> Typed
(if c_casts#get then MemTyped.Unsafe else MemTyped.Fits)
| EVA -> Eva
+ | BYTES -> Bytes
in {
mheap = m ;
mvar = if c_ctxt#get then Caveat else if c_byref#get then Ref else Var ;
diff --git a/src/plugins/wp/wp.ml b/src/plugins/wp/wp.ml
index c10ae35f535..89dfaae71cb 100644
--- a/src/plugins/wp/wp.ml
+++ b/src/plugins/wp/wp.ml
@@ -95,6 +95,7 @@ module MemDebug = MemDebug
module MemEmpty = MemEmpty
module MemLoader = MemLoader
module MemMemory = MemMemory
+module MemBytes = MemBytes
module MemTyped = MemTyped
module MemVal = MemVal
module MemVar = MemVar
--
GitLab