diff --git a/Makefile b/Makefile
index 8b2e0e805f772f40f62a3b545f3dafa032047b6e..add6a8e330e945f5b3de056c421b576856484cb4 100644
--- a/Makefile
+++ b/Makefile
@@ -936,6 +936,19 @@ PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(VALUE_TYPES))
$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
+#########
+# Reduc #
+#########
+PLUGIN_ENABLE:=$(ENABLE_REDUC)
+PLUGIN_DYNAMIC:=$(DYNAMIC_REDUC)
+PLUGIN_NAME:=Reduc
+PLUGIN_DISTRIBUTED:=yes
+PLUGIN_DIR:=src/plugins/reduc
+PLUGIN_CMO:=reduc_options misc value2acsl collect hyp register
+PLUGIN_DEPENDENCIES:=Value
+
+$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
+
##################
# Occurrence #
##################
diff --git a/src/plugins/reduc/Reduc.mli b/src/plugins/reduc/Reduc.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/reduc/collect.ml b/src/plugins/reduc/collect.ml
new file mode 100644
index 0000000000000000000000000000000000000000..fab5f06acf173b34b6b8319ca7e5373d1fc40cfc
--- /dev/null
+++ b/src/plugins/reduc/collect.ml
@@ -0,0 +1,183 @@
+open Cil_types
+open Cil_datatype
+
+module Options = Reduc_options
+
+exception Alarm_reached
+
+let dkey = Options.register_category "collect"
+let debug = Options.debug ~dkey
+
+type 'a alarm_component = Emitter.t ->
+ kernel_function ->
+ stmt ->
+ rank:int -> Alarms.alarm -> code_annotation -> 'a -> 'a
+
+type varh = VarAll
+type annoth = AnnotAll | AnnotInout
+
+type env = {
+ rel_varh: varh;
+ rel_annoth: annoth;
+ rel_stmts: Stmt.Set.t;
+ rel_vars: LvalStructEq.Set.t Stmt.Map.t;
+}
+
+let empty_env varh annoth = {
+ rel_varh = varh;
+ rel_annoth = annoth;
+ rel_stmts = Stmt.Set.empty;
+ rel_vars = Stmt.Map.empty;
+}
+
+let env_with_stmt env stmt =
+ { env with rel_stmts = Stmt.Set.add stmt env.rel_stmts }
+
+let env_with_stmt_vars env stmt lvs =
+ let vars =
+ try
+ Stmt.Map.find stmt env.rel_vars
+ with Not_found -> LvalStructEq.Set.empty in
+ let new_vars = LvalStructEq.Set.(union vars (of_list lvs)) in
+ { env with rel_vars = Stmt.Map.add stmt new_vars env.rel_vars }
+
+(* ************************************************************************ *)
+(** Alarms to relevant locations *)
+(* ************************************************************************ *)
+
+class stmts_vis
+ (alarm_stmt : stmt)
+ (env: env ref) = object(_)
+ inherit Cil.nopCilVisitor
+
+ method! vstmt stmt =
+ env := env_with_stmt !env stmt;
+ if Stmt.equal stmt alarm_stmt then begin
+ raise Alarm_reached
+ end;
+ Cil.DoChildren
+end
+
+let rec collect_off typ =
+ match typ with
+ | TInt _ | TFloat _ -> [ NoOffset ]
+ | TComp ({cfields = flds}, _, _) ->
+ List.fold_left collect_fields [] flds
+ | TArray (arrtyp, e_opt, _, _) ->
+ debug "Array of length %a" (Pretty_utils.pp_opt Printer.pp_exp) e_opt;
+ begin try collect_array arrtyp [] (Cil.lenOfArray64 e_opt)
+ with Cil.LenOfArray -> [] end
+ | TVoid _ | TFun _ | TPtr _ | TEnum _ | TNamed _ | TBuiltin_va_list _ -> []
+
+and collect_fields acc fld =
+ let offs = collect_off fld.ftype in
+ List.map (fun off -> Field (fld, off)) offs @ acc
+
+and collect_array typ acc = function
+ | x when Integer.is_zero x -> acc
+ | x ->
+ let offs = collect_off typ in
+ let exp = Cil.kinteger64 ~loc:Location.unknown x in
+ let acc' = acc @ List.map (fun off -> Index(exp ,off)) offs in
+ collect_array typ acc' (Integer.add x Integer.minus_one)
+
+let collect_varinfo acc x =
+ let offs = collect_off x.vtype in
+ List.map (fun off -> (Var x, off)) offs @ acc
+
+class inout_vis
+ (alarm_stmt : stmt)
+ (kf : Kernel_function.t)
+ (env : env ref) = object(self)
+ inherit stmts_vis alarm_stmt env as super
+
+ val mutable vars = []
+
+ method !vfunc _ =
+ vars <- Kernel_function.((get_locals kf) @ (get_formals kf));
+ Cil.DoChildren
+
+ method private is_first_stmt stmt =
+ try Stmt.equal stmt (Kernel_function.find_first_stmt kf)
+ with Kernel_function.No_Statement -> assert false
+
+ method !vstmt stmt =
+ let out = !Db.Outputs.statement stmt in
+ let filter_out vi =
+ let open Locations in
+ let zone = enumerate_bits (loc_of_varinfo vi) in
+ Zone.intersects out zone
+ in
+ let effect =
+ if self#is_first_stmt stmt then vars
+ else List.filter filter_out vars
+ in
+ let vars = List.fold_left collect_varinfo [] effect in
+ env := env_with_stmt_vars !env stmt vars;
+ super#vstmt stmt
+end
+
+let get_relevant_stmts kf stmt env =
+ let do_visit ref_env = match !ref_env.rel_annoth with
+ | AnnotAll -> Cil.visitCilFunction (new stmts_vis stmt ref_env)
+ | AnnotInout ->
+ Cil.visitCilFunction (new inout_vis stmt kf ref_env :> Cil.cilVisitor)
+ in
+ let renv = ref env in
+ try
+ let fundec = Kernel_function.get_definition kf in
+ ignore (do_visit renv fundec);
+ !renv
+ with Alarm_reached ->
+ !renv
+
+let get_relevant _emit kf stmt ~rank:_ _a _annot env =
+ get_relevant_stmts kf stmt env
+
+let should_annotate_stmt env stmt =
+ Stmt.Set.mem stmt env.rel_stmts
+
+(* ************************************************************************ *)
+(** Relevant locations to relevant variables *)
+(* ************************************************************************ *)
+
+class relevant_stmt_vars_visitor
+ (vars: LvalStructEq.Set.t ref) = object(_)
+ inherit Cil.nopCilVisitor
+
+ method! vstmt stmt =
+ match stmt.skind with
+ | Goto _ | UnspecifiedSequence _ -> Cil.SkipChildren
+ | _ -> Cil.DoChildren
+
+ method! vblock _ = Cil.SkipChildren
+
+ method !vexpr e =
+ begin match e.enode with
+ | Lval lv | AddrOf lv | StartOf lv ->
+ vars := LvalStructEq.Set.add lv !vars
+ | _ -> ()
+ end;
+ Cil.DoChildren
+end
+
+let get_relevant_all_vars_stmt kf stmt =
+ let do_visit ref_vars =
+ Cil.visitCilStmt (new relevant_stmt_vars_visitor ref_vars)
+ in
+ let ref_vars = ref LvalStructEq.Set.empty in
+ ignore (do_visit ref_vars stmt);
+ let locals = Kernel_function.get_locals kf in
+ let formals = Kernel_function.get_formals kf in
+ let vars = List.map Cil.var (locals @ formals) in
+ vars @ LvalStructEq.Set.elements !ref_vars
+
+let get_relevant_inout_vars_stmt env stmt =
+ try
+ let vars = Stmt.Map.find stmt env.rel_vars in
+ LvalStructEq.Set.elements vars
+ with Not_found -> assert false
+
+let get_relevant_vars_stmt env kf stmt = match env.rel_annoth with
+ | AnnotAll -> get_relevant_all_vars_stmt kf stmt
+ | AnnotInout -> get_relevant_inout_vars_stmt env stmt
diff --git a/src/plugins/reduc/collect.mli b/src/plugins/reduc/collect.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ea81bde8186ba0926a1eccbe2ff3ad98274b936e
--- /dev/null
+++ b/src/plugins/reduc/collect.mli
@@ -0,0 +1,18 @@
+open Cil_types
+
+type 'a alarm_component = Emitter.t ->
+ kernel_function ->
+ stmt ->
+ rank:int -> Alarms.alarm -> code_annotation -> 'a -> 'a
+
+type env
+
+type varh = VarAll
+type annoth = AnnotAll | AnnotInout
+
+val empty_env: varh -> annoth -> env
+
+val get_relevant: env alarm_component (* Set(loc) * Set(exp) ? *)
+
+val should_annotate_stmt: env -> stmt -> bool
+val get_relevant_vars_stmt: env -> kernel_function -> stmt -> lval list
diff --git a/src/plugins/reduc/hyp.ml b/src/plugins/reduc/hyp.ml
new file mode 100644
index 0000000000000000000000000000000000000000..cb17a0d5271f0cd65a87364237e11e081e48e0f2
--- /dev/null
+++ b/src/plugins/reduc/hyp.ml
@@ -0,0 +1,32 @@
+let pred_opt_from_expr_state state e =
+ try
+ Value2acsl.lval_to_predicate state e
+ with
+ | Cvalue.V.Not_based_on_null ->
+ Misc.not_implemented ~what:"Value not based on null";
+ None
+ | Misc.Not_implemented what ->
+ Misc.not_implemented ~what;
+ None
+
+class hypotheses_visitor (env: Collect.env) = object(self)
+ inherit Visitor.generic_frama_c_visitor (Visitor_behavior.inplace ())
+
+ method! vstmt_aux stmt =
+ let kf = Extlib.the (self#current_kf) in
+ let state = Db.Value.get_stmt_state stmt in
+ if Collect.should_annotate_stmt env stmt then begin
+ let vars = Collect.get_relevant_vars_stmt env kf stmt in
+ List.iter
+ (fun e ->
+ let p_opt = pred_opt_from_expr_state state e in
+ Extlib.may (Misc.assert_and_validate ~kf stmt) p_opt)
+ vars
+ end;
+ Cil.DoChildren
+end
+
+
+let generate_hypotheses env =
+ let visitor = new hypotheses_visitor env in
+ Cil.visitCilFileSameGlobals (visitor :> Cil.cilVisitor) (Ast.get ())
diff --git a/src/plugins/reduc/hyp.mli b/src/plugins/reduc/hyp.mli
new file mode 100644
index 0000000000000000000000000000000000000000..74c77bf394e2f62982915fe2f4f5d129d4b18a7b
--- /dev/null
+++ b/src/plugins/reduc/hyp.mli
@@ -0,0 +1 @@
+val generate_hypotheses: Collect.env -> unit
diff --git a/src/plugins/reduc/misc.ml b/src/plugins/reduc/misc.ml
new file mode 100644
index 0000000000000000000000000000000000000000..061e0f5d614dd0a965f820819cfa35ec40bd9728
--- /dev/null
+++ b/src/plugins/reduc/misc.ml
@@ -0,0 +1,31 @@
+open Cil_types
+
+module Options = Reduc_options
+
+
+exception Not_implemented of string
+
+let not_implemented ~what =
+ Options.warning "Not implemented: `%s'. Ignoring." what
+
+
+let emitter =
+ Emitter.create
+ "Reduc"
+ [ Emitter.Code_annot; Emitter.Property_status ]
+ ~correctness:[]
+ ~tuning:[]
+
+(* ******************************************************)
+(* Annotations and function contracts helpers *)
+(* ******************************************************)
+let validate_ip ip =
+ Property_status.emit emitter ~hyps:[] ip Property_status.True
+
+let assert_and_validate ~kf stmt p =
+ let p = { tp_only_check = false; tp_statement = p } in
+ let annot = Logic_const.new_code_annotation (AAssert([], p)) in
+ Annotations.add_code_annot emitter ~kf stmt annot ;
+ List.iter
+ validate_ip
+ (Property.ip_of_code_annot kf stmt annot)
diff --git a/src/plugins/reduc/misc.mli b/src/plugins/reduc/misc.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f63d293994b8d218074eea541d97a0bca2a25911
--- /dev/null
+++ b/src/plugins/reduc/misc.mli
@@ -0,0 +1,12 @@
+open Cil_types
+
+exception Not_implemented of string
+val not_implemented: what:string -> unit
+
+(* [emitter] of the reduc plugin. *)
+val emitter: Emitter.t
+
+(* ******************************************************)
+(* Annotations and function contracts helpers *)
+(* ******************************************************)
+val assert_and_validate: kf:Kernel_function.t -> stmt -> predicate -> unit
diff --git a/src/plugins/reduc/reduc_options.ml b/src/plugins/reduc/reduc_options.ml
new file mode 100644
index 0000000000000000000000000000000000000000..381cf7512f8ed872d1262b246e6f957d12092b95
--- /dev/null
+++ b/src/plugins/reduc/reduc_options.ml
@@ -0,0 +1,32 @@
+include Plugin.Register
+ (struct
+ let name = "Reduction"
+ let shortname = "reduc"
+ let help = "Generate ACSL annotations from Value Analysis informations"
+ end)
+
+module Reduc =
+ Bool
+ (struct
+ let option_name = "-reduc"
+ let help = "Use reduc"
+ let default = false
+ end)
+
+module GenAnnot =
+ String
+ (struct
+ let option_name = "-reduc-gen-annot"
+ let arg_name = "gen-annot-heuristic"
+ let help = "Heuristic to generate annotations from Value"
+ let default = "inout"
+ end)
+
+module GenVars =
+ String
+ (struct
+ let option_name = "-reduc-gen-vars"
+ let arg_name = "gen-vars-heuristic"
+ let help = "Heuristic to generate annotations for variables"
+ let default = "all"
+ end)
diff --git a/src/plugins/reduc/reduc_options.mli b/src/plugins/reduc/reduc_options.mli
new file mode 100644
index 0000000000000000000000000000000000000000..c1020ae3560193f10dd0b82e174de8972e82ae3b
--- /dev/null
+++ b/src/plugins/reduc/reduc_options.mli
@@ -0,0 +1,6 @@
+include Plugin.General_services
+
+module Reduc: Parameter_sig.Bool
+
+module GenAnnot: Parameter_sig.String
+module GenVars: Parameter_sig.String
diff --git a/src/plugins/reduc/register.ml b/src/plugins/reduc/register.ml
new file mode 100644
index 0000000000000000000000000000000000000000..a6a6d9edd2eb0b0cb1545365de8afc1b45a1a209
--- /dev/null
+++ b/src/plugins/reduc/register.ml
@@ -0,0 +1,22 @@
+module Options = Reduc_options
+
+let command_line () =
+ let varh = match Options.GenVars.get () with
+ | "all" -> Collect.VarAll
+ | _ -> Options.fatal "Not a valid variable heuristic" in
+ let annoth = match Options.GenAnnot.get () with
+ | "all" -> Collect.AnnotAll
+ | "inout" -> Collect.AnnotInout
+ | _ -> Options.fatal "Not a valid annotation heuristic"
+ in
+ varh, annoth
+
+let main () =
+ if (Options.Reduc.get ()) then begin
+ let varh, annoth = command_line () in
+ let env = Alarms.fold Collect.get_relevant (Collect.empty_env varh annoth) in
+ Hyp.generate_hypotheses env;
+ ()
+ end
+
+let () = Db.Main.extend main
diff --git a/src/plugins/reduc/value2acsl.ml b/src/plugins/reduc/value2acsl.ml
new file mode 100644
index 0000000000000000000000000000000000000000..637948a5c148a65ba244fda98045cf47ce748cc4
--- /dev/null
+++ b/src/plugins/reduc/value2acsl.ml
@@ -0,0 +1,157 @@
+open Cil_datatype
+open Cil_types
+
+open Misc
+
+module AI = Abstract_interp
+
+module Options = Reduc_options
+
+let not_yet ~what =
+ Options.warning "Not yet: %s" what
+
+(* [int_to_predicate ~loc lop te i] create a predicate where [te] [lop] [i]. *)
+let int_to_predicate ~loc ~lop te (i: Integer.t) =
+ let ti = Logic_const.tint i in
+ Logic_const.prel ~loc (lop, te, ti)
+
+(* [float_to_predicate ~loc lop te f] create a predicate where [te] [lop] [f]. *)
+let float_to_predicate ~loc ~lop t f =
+ let tf = Logic_const.treal ~loc f in
+ Logic_const.prel ~loc (lop, t, tf)
+
+(* [interval_to_predicate_opt ~loc te min max] may create an interval
+ predicate where [min] <= [te] <= [max]. *)
+let interval_to_predicate_opt ~loc te min max =
+ let min_predicate =
+ int_to_predicate ~loc ~lop:Rge te
+ and max_predicate =
+ int_to_predicate ~loc ~lop:Rle te
+ in
+ Extlib.merge_opt
+ (fun _ pmin pmax -> Logic_const.pand ~loc (pmin, pmax))
+ ()
+ (Extlib.opt_map min_predicate min)
+ (Extlib.opt_map max_predicate max)
+
+(* [congruence_to_predicate_opt ~loc te rem modulo] may create a congruence
+ predicate where [te] mod [modulo] equals [rem] *)
+let congruence_to_predicate_opt ~loc te rem modulo =
+ if Integer.(equal modulo one) then None
+ else
+ let tmodulo = Logic_const.tint ~loc modulo in
+ let tbinop = TBinOp(Mod, te, tmodulo) in
+ (* since 0 <= rem < mod *)
+ let tmodop = Logic_const.term ~loc tbinop (Linteger) in
+ let p = int_to_predicate ~loc ~lop:Req tmodop rem in
+ Some p
+
+let fval_to_predicate ~loc t f =
+ match Ival.min_and_max_float f with
+ | None, false -> assert false
+ | _, true -> Logic_const.pfalse (* todo *)
+ | Some (fmn, fmx), _ ->
+ let mn = Fval.F.to_float fmn in
+ let mx = Fval.F.to_float fmx in
+ let pmn = float_to_predicate ~loc ~lop:Rge t mn in
+ let pmx = float_to_predicate ~loc ~lop:Rle t mx in
+ Logic_const.pand ~loc (pmn, pmx)
+
+(* [ival_to_predicate_opt ~loc t ival] may create a predicate from different
+ domains contained in [ival]. *)
+let ival_to_predicate_opt ~loc t ival =
+ if Ival.is_float ival
+ then Some (fval_to_predicate ~loc t ival)
+ else
+ match Ival.project_small_set ival with
+ | Some is ->
+ let ps = List.map (int_to_predicate ~loc ~lop:Req t) is in
+ let pors = Logic_const.pors ps in
+ Some pors
+ | None ->
+ match Ival.min_max_r_mod ival with
+ | (None, None, _, modulo) when AI.Int.is_one modulo ->(*Top*) None
+ | (min, max, rem, modulo) ->
+ let pint = interval_to_predicate_opt ~loc t min max in
+ let pcon = congruence_to_predicate_opt ~loc t rem modulo in
+ Extlib.merge_opt
+ (fun _ pint pcon -> Logic_const.pand ~loc (pint, pcon))
+ ()
+ pint
+ pcon
+
+
+(* [valid_to_predicate_opt ~loc t valid] may create validity predicate *only*
+ for valid locations. *)
+let valid_to_predicate_opt ~loc t valid =
+ let here_lbl = BuiltinLabel Here in
+ match valid with
+ | Base.Empty -> None
+ | Base.Known (bmn, bmx) | Base.Unknown (bmn, Some bmx, _) ->
+ let tbmn = Cil.lconstant ~loc bmn in
+ let tbmx = Cil.lconstant ~loc bmx in
+ let p = Logic_const.pvalid_range ~loc (here_lbl, t, tbmn, tbmx) in
+ Some p
+ | Base.Unknown (_, _, _) -> None
+ | Base.Variable { Base.min_alloc = bmn } when Integer.(equal bmn minus_one) ->
+ not_yet "Invalid Base.Variable above max_alloc";
+ None
+ | Base.Variable { Base.min_alloc = bmn; Base.max_alloc = bmx } ->
+ not_yet "Invalid Base.Variable above max_alloc";
+ let tbmn = Cil.lconstant ~loc bmn in
+ let tbmx = Cil.lconstant ~loc bmx in
+ let p = Logic_const.pvalid_range ~loc (here_lbl, t, tbmn, tbmx) in
+ Some p
+ | Base.Invalid ->
+ not_yet "Invalid Base";
+ None
+
+let base_to_predicate ~loc t (b: Base.t) =
+ match b with
+ | Base.Var (_vi, valid) | Base.Allocated (_vi, _, valid) ->
+ valid_to_predicate_opt ~loc t valid
+ | Base.CLogic_Var (_lvi, _typ, _) -> raise (Not_implemented "Base.CLogic_Var")
+ | Base.Null -> assert false (*by projecting ival*)
+ | Base.String _ -> raise (Not_implemented "Base.String")
+
+
+let base_offset_to_predicate ~loc t b o =
+ if Ival.equal Ival.zero o then
+ base_to_predicate ~loc t b
+ else begin
+ not_yet ~what:"Base w/ offsets";
+ None
+ end
+
+let _base_offsets_to_predicate ~loc t (m: Cvalue.V.M.t) =
+ let aux b o (acc: predicate list) =
+ let p_opt = base_offset_to_predicate ~loc t b o in
+ (Extlib.list_of_opt p_opt) @ acc
+ in
+ match Cvalue.V.M.fold aux m [] with
+ | [] -> None
+ | ps -> Some (Logic_const.pands ps)
+
+let value_to_predicate_opt ?(loc=Location.unknown) t v =
+ let open Cvalue.V in
+ match v with
+ | Top _ -> None
+ | Map _m ->
+ try
+ let ival = project_ival v in
+ ival_to_predicate_opt ~loc t ival
+ with
+ | Not_based_on_null -> (* base_offsets_to_predicate ~loc t m *) None
+
+let exp_to_predicate ?(loc=Location.unknown) state e =
+ let value = !Db.Value.eval_expr ~with_alarms:CilE.warn_none_mode state e in
+ let te = Logic_utils.expr_to_term ~coerce:false e in
+ value_to_predicate_opt ~loc te value
+
+let lval_to_predicate ?(loc=Location.unknown) state lv =
+ let value = snd(!Db.Value.eval_lval
+ ~with_alarms:CilE.warn_none_mode None state lv)
+ in
+ let e = Cil.new_exp ~loc (Lval lv) in
+ let te = Logic_utils.expr_to_term ~coerce:false e in
+ value_to_predicate_opt ~loc te value
diff --git a/src/plugins/reduc/value2acsl.mli b/src/plugins/reduc/value2acsl.mli
new file mode 100644
index 0000000000000000000000000000000000000000..1ef1e2f4b8987dd89a5d8ffabefaa95fcf9b2b6e
--- /dev/null
+++ b/src/plugins/reduc/value2acsl.mli
@@ -0,0 +1,9 @@
+open Cil_types
+
+(* [value_to_predicate_opt loc t value] may create a predicate given a [value]
+ about some [term].
+ @return None if no such predicate can be created. *)
+val value_to_predicate_opt: ?loc:location -> term -> Cvalue.V.t -> predicate option
+
+val lval_to_predicate: ?loc:location -> Cvalue.Model.t -> lval -> predicate option
+val exp_to_predicate: ?loc:location -> Cvalue.Model.t -> exp -> predicate option
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 8fea80af863b6d2c7203f5b57d4e5937d3167322..85a6754ed0cb91f70198a84e98babadc599ead3b 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer
+type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer | Value
type mvar = Raw | Var | Ref | Caveat
type setup = {
@@ -68,6 +68,7 @@ let descr_mheap d = function
| ZeroAlias -> main d "zeroalias"
| Hoare -> main d "hoare"
| Typed p -> main d "typed" ; descr_mtyped d p
+ | Value -> main d "value"
let descr_mvar d = function
| Var -> ()
@@ -247,6 +248,7 @@ 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_MemValue = MakeCompiler(MemValue)
let compiler mheap mvar : (module Sigs.Compiler) =
@@ -259,6 +261,7 @@ let compiler mheap mvar : (module Sigs.Compiler) =
| Typed _ , Raw -> (module Comp_MemTyped)
| Typed _ , Var -> (module Comp_Typed_Var)
| Typed _ , Ref -> (module Comp_Typed_Ref)
+ | Value, _ -> (module Comp_MemValue)
(* -------------------------------------------------------------------------- *)
(* --- Tuning --- *)
@@ -276,6 +279,7 @@ let configure_mheap = function
Context.pop MemTyped.pointer orig_memtyped_pointer
in
rollback
+ | Value -> MemValue.configure ()
let configure_driver setup driver () =
let rollback_mheap = configure_mheap setup.mheap in
diff --git a/src/plugins/wp/Factory.mli b/src/plugins/wp/Factory.mli
index 913d151300efeb21ff7da03a4f26e85693225926..d83156b90222fc88ff459e1ed050b6b301c00391 100644
--- a/src/plugins/wp/Factory.mli
+++ b/src/plugins/wp/Factory.mli
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer
+type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer | Value
type mvar = Raw | Var | Ref | Caveat
type setup = {
diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index b24a0ca165b0113a6afb5761142d6c86f4eb22f2..42a18b86e5bfa604ec4b28bc06d31a33898e24a7 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/src/plugins/wp/GuiPanel.ml
@@ -139,7 +139,8 @@ class model_selector (main : Design.main_window_extension_points) =
| ZeroAlias -> memory#set TREE
| Region -> memory#set REGION
| Hoare -> memory#set HOARE
- | Typed m -> memory#set TYPED ; c_casts#set (m = MemTyped.Unsafe)) ;
+ | Typed m -> memory#set TYPED ; c_casts#set (m = MemTyped.Unsafe)
+ | Value -> ()) ;
c_byref#set (s.mvar = Ref) ;
c_ctxt#set (s.mvar = Caveat) ;
c_cint#set (s.cint = Cint.Machine) ;
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 2ab8ab0e65898a650b80a0e9f5b4db42800298ba..c662db3ead0e3afaf813507f870fc08aa5fa37d9 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -80,7 +80,7 @@ PLUGIN_CMO:= \
LogicSemantics LogicAssigns \
Sigma MemLoader \
MemEmpty MemZeroAlias MemVar \
- MemMemory MemTyped MemRegion \
+ MemMemory MemTyped MemValue MemRegion \
wpReached wpRTE wpAnnot \
CfgCompiler StmtSemantics \
VCS script proof wpo wpReport \
@@ -242,7 +242,7 @@ WP_API_BASE= \
Plang.mli Pcfg.mli Pcond.mli \
CodeSemantics.mli \
LogicCompiler.mli LogicSemantics.mli \
- Sigma.mli MemVar.mli MemTyped.mli \
+ Sigma.mli MemVar.mli MemTyped.mli MemValue.mli \
CfgCompiler.mli StmtSemantics.mli \
Factory.mli driver.mli VCS.mli Tactical.mli Strategy.mli Auto.mli \
VC.mli wpo.mli ProverTask.mli prover.mli
diff --git a/src/plugins/wp/MemValue.ml b/src/plugins/wp/MemValue.ml
new file mode 100644
index 0000000000000000000000000000000000000000..4e7a77a0073e53f7cfdbb77a2342ccd29f667572
--- /dev/null
+++ b/src/plugins/wp/MemValue.ml
@@ -0,0 +1,796 @@
+(**************************************************************************)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2016 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Value Memory Model --- *)
+(* -------------------------------------------------------------------------- *)
+
+open Cil_types
+open Cil_datatype
+open Ctypes
+open Lang
+open Lang.F
+open Sigs
+open Definitions
+
+module L = Qed.Logic
+
+let dkey = Wp_parameters.register_category "value" (* Debugging key *)
+let debug fmt = Wp_parameters.debug ~dkey fmt
+let not_yet fmt = Wp_parameters.not_yet_implemented fmt
+let not_yet_base = not_yet "Base %a. Only Null and Var implemented." Base.pretty
+let not_yet_obj = fun obj -> not_yet "Logic type %a." Ctypes.pp_object obj
+
+let dkey = Wp_parameters.register_category "value+flow"
+let debug_flow fmt = Wp_parameters.debug ~dkey fmt
+
+(* let dkey = Wp_parameters.register_category "value+eva"
+ * let debug_eva fmt = Wp_parameters.debug ~dkey fmt *)
+
+let datatype = "MemValue"
+
+let t_addr = MemMemory.t_addr
+
+(* -------------------------------------------------------------------------- *)
+(* --- Utilities --- *)
+(* -------------------------------------------------------------------------- *)
+
+let a_null = MemMemory.a_null (* { base = 0; offset = 0 } *)
+let a_base = MemMemory.a_base (* p -> p.offset *)
+let a_offset = MemMemory.a_offset (* p -> p.base *)
+let a_global = MemMemory.a_global (* b -> { base = b; offset = 0 } *)
+let a_shift = MemMemory.a_shift (* p k -> { p with offset = p.offset + k } *)
+let a_addr = MemMemory.a_addr (* b k -> { base = b; offset = k } *)
+
+let cluster_dummy () = Definitions.cluster ~id:"Value" ~title:"MemValue" ()
+
+(* Wp utilities *)
+module Cstring =
+struct
+ include Cstring
+
+ let str_cil ~eid cstr =
+ let enode = match cstr with
+ | C_str str -> Const (CStr str)
+ | W_str wstr -> Const (CWStr wstr)
+ in {
+ eid = eid;
+ enode = enode;
+ eloc = Location.unknown;
+ }
+end
+
+(*
+let flow f l = (* TODO: USE ONE DAY *)
+ let aux b acc =
+ let cond = F.e_eq (a_base l.loc_t) (F.e_int (Base.id b)) in
+ F.e_if cond (f l b) acc
+ in
+ V.fold_bases aux l.loc_v (F.e_false)
+ *)
+
+(* Value utilities *)
+module V = Cvalue.V
+(* module V_Or_Uninitialized = Cvalue.V_Or_Uninitialized *)
+(* module V_Offsetmap = Cvalue.V_Offsetmap *)
+
+module Base =
+struct
+ include Base
+
+ let bitsize_from_validity = function
+ | Invalid -> Integer.zero
+ | Empty -> Integer.zero
+ | Known (_, m)
+ | Unknown (_, _, m) -> Integer.succ m
+ | Variable { max_allocable } -> Integer.succ max_allocable
+
+ let size_from_validity b =
+ Integer.(e_div (bitsize_from_validity b) eight)
+end
+
+module VState =
+struct
+ module M = Cvalue.Model
+ let current : M.t ref = ref M.bottom
+ let _update () =
+ try
+ match WpContext.get_scope () with
+ | Global -> assert false
+ | Kf kf ->
+ current := M.bottom;
+ let vis = object
+ inherit Cil.nopCilVisitor
+ method !vstmt s =
+ current := M.join (Db.Value.get_stmt_state s) !current;
+ Cil.DoChildren
+ end in
+ ignore (Cil.visitCilFunction vis (Kernel_function.get_definition kf))
+ with | Invalid_argument _ | Kernel_function.No_Definition
+ -> assert false (* since kf exists and has a definition *)
+end
+
+module Value :
+sig
+ type t
+ type state = Cvalue.Model.t
+
+ val top : t
+
+ val null : t
+ val literal : eid:int -> Cstring.cst -> int * t
+ val cvar : state -> varinfo -> t
+
+ val field : t -> fieldinfo -> t
+ val shift : t -> c_object -> term -> t
+ val base_addr : t -> t
+ val load : state -> t -> c_object -> t
+
+ val bases : t -> Base.t list
+
+ val pretty : Format.formatter -> t -> unit
+ val compare : t -> t -> int
+end =
+struct
+ type t = Cvalue.V.t
+ type state = Cvalue.Model.t
+
+ let with_alarms = CilE.warn_none_mode
+ let eval_expr state e = !Db.Value.eval_expr ~with_alarms state e
+
+ let top = V.top
+
+ let null = V.inject Base.null Ival.zero
+
+ let literal ~eid cstr =
+ let b = Base.of_string_exp (Cstring.str_cil ~eid cstr) in
+ Base.id b, V.inject b Ival.zero
+
+ let cvar : state -> varinfo -> t = fun state vi ->
+ eval_expr state (Cil.mkAddrOfVi vi)
+
+ let field : t -> fieldinfo -> t = fun v f ->
+ let bsize = 8 * Ctypes.field_offset f |> Integer.of_int in
+ let offs = Ival.inject_singleton bsize in
+ Cvalue.V.shift offs v
+
+ let shift : t -> c_object -> term -> t = fun v obj t ->
+ let bsize = 8 * Ctypes.sizeof_object obj |> Integer.of_int in
+ let offs = match F.repr t with
+ | L.Kint z -> Ival.inject_singleton (Integer.mul bsize z)
+ | _ -> Ival.top in
+ Cvalue.V.shift offs v
+
+ let base_addr : t -> t = function
+ | V.Top _ -> V.top (* TODO: For now, just send Top *)
+ | V.Map m ->
+ let v = ref V.bottom in
+ V.M.iter (fun b _ -> v := V.add b Ival.zero !v) m;
+ !v
+
+ let load : state -> t -> c_object -> t = fun state v obj ->
+ let bsize = 8 * Ctypes.sizeof_object obj in
+ let bits = Locations.loc_bytes_to_loc_bits v in
+ let int_base = bsize |> Integer.of_int |> Int_Base.inject in
+ let vloc = Locations.make_loc bits int_base in
+ Cvalue.Model.find state vloc
+
+ let bases : t -> Base.t list = fun v ->
+ try
+ V.fold_bases
+ (fun b acc -> b :: acc)
+ v []
+ with Abstract_interp.Error_Top -> []
+
+ let pretty = V.pretty
+ let compare = V.compare
+end
+
+
+(* -------------------------------------------------------------------------- *)
+(* --- Model --- *)
+(* -------------------------------------------------------------------------- *)
+
+
+(* -------------------------------------------------------------------------- *)
+(* --- Model Parameters --- *)
+(* -------------------------------------------------------------------------- *)
+
+let configure () =
+ if not (Db.Value.is_computed ()) then
+ Warning.error ~source:"Value Model"
+ "A previous Value analysis is needed by this memory model.";
+ let orig_pointer = Context.push Lang.pointer (fun _ -> t_addr) in
+ let rollback () =
+ Context.pop Lang.pointer orig_pointer;
+ in
+ rollback
+
+
+(* -------------------------------------------------------------------------- *)
+(* --- Chunk --- *)
+(* -------------------------------------------------------------------------- *)
+
+type chunk =
+ | M_int
+ | M_char
+ | M_float
+ | M_base of Base.t
+
+module Chunk =
+struct
+ type t = chunk
+ let self = "MemValue.Chunk"
+ let hash = function
+ | M_int -> 1
+ | M_char -> 2
+ | M_float -> 3
+ | M_base b -> 5 * Base.hash b
+ let equal c1 c2 = match c1, c2 with
+ | M_base b1, M_base b2 -> Base.equal b1 b2
+ | _ -> c1 = c2
+ let compare c1 c2 = match c1, c2 with
+ | M_base b1, M_base b2 -> Base.compare b1 b2
+ | _ -> Stdlib.compare c1 c2
+ let pretty fmt c = match c with
+ | M_int -> Format.pp_print_string fmt "Mint"
+ | M_char -> Format.pp_print_string fmt "Mchar"
+ | M_float -> Format.pp_print_string fmt "Mfloat"
+ | M_base b -> Base.pretty fmt b
+ let tau_of_chunk = function
+ | M_int | M_char -> L.Array (t_addr, L.Int)
+ | M_float -> L.Array (t_addr, L.Real)
+ | M_base _ -> L.Array (L.Int, t_addr)
+ let basename_of_chunk c = match c with
+ | M_int -> "Mint"
+ | M_char -> "Mchar"
+ | M_float -> "Mfloat"
+ | M_base b -> match b with
+ | Base.Null -> "Mnull"
+ | Base.Var (vi, _) -> Format.sprintf "Mvar_%s" (LogicUsage.basename vi)
+ | Base.String (eid, _) -> Format.sprintf "MStr_%d" eid
+ | b -> not_yet_base b
+ let is_framed c = match c with
+ | M_int | M_char | M_float -> false
+ | M_base b ->
+ try
+ match WpContext.get_scope () with
+ | Global -> assert false
+ | Kf kf ->
+ Base.is_formal_or_local b (Kernel_function.get_definition kf)
+ with Invalid_argument _ | Kernel_function.No_Definition ->
+ assert false (* by context *)
+end
+
+module RegisterBase = WpContext.Static
+ (struct
+ let name = "MemValue.RegisterBase"
+ type key = term (* of type int *)
+ type data = Base.t
+ include F
+ let pretty = F.pp_term
+ end)
+
+let count = ref 0
+
+module TermV = WpContext.Generator(Value)
+ (struct
+ let name = "MemValue.TermV"
+ type key = Value.t
+ type data = term (* of type addr *)
+
+ let _base_id prefix v (base : term) =
+ let name = prefix ^ "_id_lemma" in
+ let equal b = F.p_equal base (F.e_int (Base.id b)) in
+ let rec lemma = function
+ | [] -> assert false
+ | [ b ] -> equal b
+ | b :: bs -> F.p_or (equal b) (lemma bs)
+ in
+ match Value.bases v with
+ | [] -> ()
+ | bs ->
+ Definitions.define_lemma {
+ l_kind = `Axiom;
+ l_name = name; l_types = 0; l_triggers = []; l_forall = [];
+ l_lemma = lemma bs;
+ l_cluster = cluster_dummy ();
+ }
+
+ let compile_base _v =
+ incr count;
+ let prefix =
+ Format.sprintf "Base_%d" !count in
+ let var = Lang.freshvar ~basename:prefix Qed.Logic.Int in
+ let base = e_var var in
+ (* base_id prefix v base; *)
+ base
+
+ let compile_offset _ =
+ let prefix =
+ Format.sprintf "Offs" in
+ let var = Lang.freshvar ~basename:prefix Qed.Logic.Int in
+ e_var var
+
+ let compile x = a_addr (compile_base x) (compile_offset x)
+ end)
+
+type loc = {
+ loc_v : Value.t;
+ loc_t : term; (* of type addr *)
+}
+
+module Heap = Qed.Collection.Make(Chunk)
+module Sigma = Sigma.Make(Chunk)(Heap)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Sigma --- *)
+(* -------------------------------------------------------------------------- *)
+
+type sigma = Sigma.t
+
+(* -------------------------------------------------------------------------- *)
+(* --- State Pretty Printer --- *)
+(* -------------------------------------------------------------------------- *)
+
+type state = chunk Tmap.t
+
+let state : sigma -> state = fun sigma ->
+ let s = ref Tmap.empty in
+ Sigma.iter (fun c x -> s := Tmap.add (e_var x) c !s) sigma; !s
+
+let imval c = Sigs.Mchunk (Pretty_utils.to_string Chunk.pretty c, KValue)
+
+let lookup_lv _c _e = assert false (* TODO *)
+
+let lookup s e = imval (Tmap.find e s)
+
+let apply f s =
+ let m = ref Tmap.empty in
+ Tmap.iter (fun e c -> m := Tmap.add (f e) c !m) s; !m
+
+let iter : (mval -> term -> unit) -> state -> unit = fun f s ->
+ Tmap.iter (fun v c -> f (imval c) v) s
+
+let heap domain state =
+ Tmap.fold (fun m c w ->
+ if Vars.intersect (F.vars m) domain
+ then Heap.Map.add c m w else w
+ ) state Heap.Map.empty
+
+let rec diff c v1 v2 =
+ if v1 == v2 then Bag.empty else
+ match F.repr v2 with
+ | L.Aset (m, k, v) ->
+ let lv = lookup_lv c k in
+ let upd = Mstore (lv, v) in
+ Bag.append (diff c v1 m) upd
+ | _ ->
+ Bag.empty
+
+let updates : (state sequence) -> Vars.t -> update Bag.t = fun seq domain ->
+ let pool = ref Bag.empty in
+ let pre = heap domain seq.pre in
+ let post = heap domain seq.post in
+ Heap.Map.iter2
+ (fun c v1 v2 ->
+ match v1, v2 with
+ | Some v1, Some v2 -> pool := Bag.concat (diff c v1 v2) !pool
+ | _ -> ()
+ ) pre post;
+ !pool
+
+(* -------------------------------------------------------------------------- *)
+(* --- Location --- *)
+(* -------------------------------------------------------------------------- *)
+
+let m_int i = if Ctypes.is_char i then M_char else M_int
+
+type segment = loc rloc
+
+let vars : loc -> Vars.t = fun l -> F.vars l.loc_t
+
+let occurs x l = Vars.mem x (vars l)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Pretty --- *)
+(* -------------------------------------------------------------------------- *)
+
+let pretty : Format.formatter -> loc -> unit = fun fmt l ->
+ Format.fprintf fmt "[v: %a; t: %a]"
+ Value.pretty l.loc_v F.pp_term l.loc_t
+
+(* -------------------------------------------------------------------------- *)
+(* --- Basic Constructors --- *)
+(* -------------------------------------------------------------------------- *)
+
+let null : loc = { (*QB: Correct *)
+ loc_v = Value.null;
+ loc_t = a_null;
+}
+
+let literal ~eid cstr = (*QB: Correct *)
+ let bid, v = Value.literal ~eid cstr in
+ {
+ loc_v = v;
+ loc_t = a_global (F.e_int bid);
+ }
+
+let cvar : varinfo -> loc = fun x ->
+ debug_flow "[cvar] %a" Varinfo.pretty x;
+ let state = !VState.current in
+ let v = Value.cvar state x in
+ {
+ loc_v = v;
+ loc_t = TermV.get v;
+ }
+
+(* -------------------------------------------------------------------------- *)
+(* --- Logic - Location conversion --- *)
+(* -------------------------------------------------------------------------- *)
+
+(* [pointer_loc t] convert a logic term [t] into an abstract location.
+ Currently, we only accept [t] of type [t_addr] and lose information about
+ the abstract value for this location. *)
+let pointer_loc : term -> loc = fun t ->
+ debug_flow "locof %a" F.pp_term t;
+ match F.typeof t with
+ | tau when tau = t_addr -> {
+ loc_v = Value.top;
+ loc_t = t
+ }
+ | _ -> assert false
+
+(* [pointer_val l] convert an abstract location [l] into a logic term. Since we
+ can't express abstract values into the logic, only the logic part of the
+ location is returned. *)
+let pointer_val : loc -> term = fun l ->
+ debug_flow "valof %a" pretty l;
+ l.loc_t
+
+(* -------------------------------------------------------------------------- *)
+(* --- Lifting --- *)
+(* -------------------------------------------------------------------------- *)
+
+let field : loc -> fieldinfo -> loc = fun l f ->
+ debug_flow "field";
+ let offs = Integer.of_int (Ctypes.field_offset f) in
+ {
+ loc_v = Value.field l.loc_v f;
+ loc_t = a_shift l.loc_t (F.e_bigint offs);
+ }
+
+let shift : loc -> c_object -> term -> loc = fun l obj t ->
+ debug_flow "shift %a" Ctypes.pp_object obj;
+ let size = Integer.of_int (Ctypes.sizeof_object obj) in
+ let offs = F.e_times size t in
+ {
+ loc_v = Value.shift l.loc_v obj t;
+ loc_t = a_shift l.loc_t offs;
+ }
+
+let base_addr : loc -> loc = fun l ->
+ debug_flow "base_addr";
+ {
+ loc_v = Value.base_addr l.loc_v;
+ loc_t = a_addr (a_base l.loc_t) F.e_zero
+ }
+
+let block_length : sigma -> c_object -> loc -> term = fun _s _obj l ->
+ let aux acc b =
+ F.e_if
+ (F.e_eq (F.e_int (Base.id b)) (a_base l.loc_t))
+ (F.e_bigint (Base.size_from_validity (Base.validity b)))
+ acc
+ in
+ List.fold_left aux F.e_false (Value.bases l.loc_v)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Casting --- *)
+(* -------------------------------------------------------------------------- *)
+
+let cast : c_object sequence -> loc -> loc = fun _obj l ->
+ debug_flow "cast";
+ l (* TODO: Check correctness *)
+
+let loc_of_int : c_object -> term -> loc = fun _obj t ->
+ debug "int: %a" F.pp_term t;
+ if F.is_zero t then null else
+ begin match F.repr t with
+ | L.Kint _ -> (* TODO: Not correct *)
+ let obj = Ctypes.(C_int (c_char ())) in
+ {
+ loc_v = Value.shift Value.null obj t;
+ loc_t = a_shift null.loc_t t;
+ }
+ | _ -> Warning.error ~source:"Value Model"
+ "Forbidden cast of int to pointer"
+ end
+
+let int_of_loc : c_int -> loc -> term = fun _ l ->
+ a_offset l.loc_t
+
+(* -------------------------------------------------------------------------- *)
+(* --- Memory Load --- *)
+(* -------------------------------------------------------------------------- *)
+
+let loadvalue : sigma -> c_object -> loc -> term = fun sigma _obj l ->
+ let ite acc b =
+ let cond = F.e_eq (a_base l.loc_t) (F.e_int (Base.id b)) in
+ let load = F.e_get (Sigma.value sigma (M_base b)) (a_offset l.loc_t) in
+ F.e_if cond load acc
+ in
+ try
+ List.fold_left ite F.e_false (Value.bases l.loc_v)
+ with Abstract_interp.Error_Top -> F.e_false
+
+let loadpointer : c_object -> loc -> loc = fun obj loc ->
+ let state = !VState.current in
+ let v = Value.load state loc.loc_v obj in
+ {
+ loc_v = v;
+ loc_t = TermV.get v;
+ }
+
+let load : sigma -> c_object -> loc -> loc value = fun sigma obj l -> match obj with
+ | C_int i ->
+ Val (F.e_get (Sigma.value sigma (m_int i)) l.loc_t)
+ | C_float _ ->
+ Val (F.e_get (Sigma.value sigma M_float) l.loc_t)
+ | C_pointer _ ->
+ Loc (loadpointer obj l)
+ | _ -> not_yet_obj obj
+
+(* Wrapper *)
+let load sigma obj l = match load sigma obj l with
+ | Val t as v ->
+ debug_flow "load (%a) %a = Val (%a)"
+ Ctypes.pp_object obj pretty l F.pp_term t;
+ v
+ | Loc l' as v ->
+ debug_flow "load (%a) %a = Loc (%a)"
+ Ctypes.pp_object obj pretty l pretty l';
+ v
+
+(* -------------------------------------------------------------------------- *)
+(* --- Memory Store --- *)
+(* -------------------------------------------------------------------------- *)
+
+let stored : sigma sequence -> c_object -> loc -> term -> equation list = fun seq _obj l e ->
+ let ite acc b =
+ let cond = F.p_equal (a_base l.loc_t) (F.e_int (Base.id b)) in
+ let store =
+ F.p_equal
+ (Sigma.value seq.post (M_base b))
+ (F.e_set (Sigma.value seq.pre (M_base b)) (a_offset l.loc_t) e)
+ in
+ F.p_if cond store acc
+ in
+ try
+ let p = List.fold_left ite F.p_false (Value.bases l.loc_v) in
+ [ Assert p ]
+ with Abstract_interp.Error_Top -> [ Assert F.p_false ]
+
+let updated s c l v =
+ let m1 = Sigma.value s.pre c in
+ let m2 = Sigma.value s.post c in
+ [ Set( m2, (F.e_set m1 l.loc_t v)) ]
+
+let stored : sigma sequence -> c_object -> loc -> term -> equation list = fun seq obj l e ->
+ debug_flow "store %a" Ctypes.pp_object obj;
+ match obj with
+ | C_int i -> updated seq (m_int i) l e
+ | C_float _ -> updated seq M_float l e
+ | C_pointer _ -> stored seq obj l e
+ | _ -> not_yet_obj obj
+
+let copied : sigma sequence -> c_object -> loc -> loc -> equation list = fun seq obj ll lr ->
+ debug_flow "copied";
+ stored seq obj ll (loadvalue seq.pre obj lr)
+
+let assigned : sigma sequence -> c_object -> loc sloc -> equation list = fun _ _ _ ->
+ debug_flow "assigned";
+ [ Assert F.p_true ]
+
+(* -------------------------------------------------------------------------- *)
+(* --- Pointer Comparison --- *)
+(* -------------------------------------------------------------------------- *)
+
+let is_null : loc -> pred = fun l ->
+ p_equal l.loc_t a_null
+
+let loc_delta l1 l2 =
+ match F.is_equal (a_base l1.loc_t) (a_base l2.loc_t) with
+ | L.Yes -> F.e_sub (a_offset l1.loc_t) (a_offset l2.loc_t)
+ | L.Maybe | L.No ->
+ Warning.error "Can only compare pointers with same base."
+
+let base_eq l1 l2 = F.p_equal (a_base l1.loc_t) (a_base l2.loc_t)
+let offset_cmp cmpop l1 l2 = cmpop (a_offset l1.loc_t) (a_offset l2.loc_t)
+
+let loc_diff : c_object -> loc -> loc -> term = fun _obj l1 l2 ->
+ debug_flow "loc_diff";
+ loc_delta l1 l2
+let loc_eq : loc -> loc -> pred = fun l1 l2 ->
+ debug_flow "loc_eq";
+ F.p_and (base_eq l1 l2) (offset_cmp F.p_equal l1 l2)
+let loc_lt : loc -> loc -> pred = fun l1 l2 ->
+ debug_flow "loc_lt";
+ F.p_lt (loc_delta l1 l2) F.e_zero
+let loc_leq : loc -> loc -> pred = fun l1 l2 ->
+ debug_flow "loc_leq";
+ F.p_leq (loc_delta l1 l2) F.e_zero
+let loc_neq : loc -> loc -> pred = fun l1 l2 ->
+ debug_flow "loc_neq";
+ F.p_neq (loc_delta l1 l2) F.e_zero
+
+(* -------------------------------------------------------------------------- *)
+(* --- Scope --- *)
+(* -------------------------------------------------------------------------- *)
+
+type alloc = ALLOC | FREE
+
+let alloc_sigma : sigma -> varinfo list -> sigma = fun sigma xs ->
+ let update sigma x =
+ let havoc_chunk s (c : Base.t) =
+ if Sigma.mem s (M_base c) then s
+ else Sigma.havoc_chunk s (M_base c)
+ in
+ let state = !VState.current in
+ let v = Value.cvar state x in
+ List.fold_left havoc_chunk sigma (Value.bases v)
+ in
+ List.fold_left update sigma xs
+
+let alloc_pred : sigma sequence -> varinfo list -> alloc -> pred list = fun _ _ _ -> [] (* TODO *)
+
+ let alloc sigma xs =
+ if xs = [] then sigma else alloc_sigma sigma xs
+
+let scope : sigma sequence -> scope -> varinfo list -> pred list = fun seq scope xs ->
+ match scope with
+ | Enter ->
+ alloc_pred seq xs ALLOC
+ | Leave ->
+ alloc_pred seq xs FREE
+
+let global : sigma -> term (*addr*) -> pred = fun _sigma p ->
+ match RegisterBase.get (a_base p) with
+ | None -> F.p_false
+ | Some c ->
+ F.p_bool (F.e_bool (Chunk.is_framed (M_base c)))
+
+(* -------------------------------------------------------------------------- *)
+(* --- Segments --- *)
+(* -------------------------------------------------------------------------- *)
+
+type range =
+ | LOC of term (*addr*) * term (*size*)
+ | RANGE of term (*base*) * Vset.set (*range offset*)
+
+let range = function
+ | Rloc (obj, l) ->
+ LOC (l.loc_t, F.e_int (Ctypes.sizeof_object obj))
+ | Rrange (l, obj, Some a, Some b) ->
+ let l' = shift l obj a in
+ let n = e_fact (Ctypes.sizeof_object obj) (F.e_range a b) in
+ LOC (l'.loc_t , n)
+ | Rrange (l,_obj,None,None) ->
+ RANGE (a_base l.loc_t, Vset.range None None)
+ | Rrange (l,obj,Some a,None) ->
+ let se = Ctypes.sizeof_object obj in
+ RANGE (a_base l.loc_t, Vset.range (Some (e_fact se a)) None)
+ | Rrange (l,obj,None,Some b) ->
+ let se = Ctypes.sizeof_object obj in
+ RANGE (a_base l.loc_t, Vset.range None (Some (e_fact se b)))
+
+let range_set = function
+ | LOC (l, n) ->
+ let a = a_offset l in
+ let b = e_add a n in
+ a_base l, Vset.range (Some a) (Some b)
+ | RANGE (base, set) -> base, set
+
+(* -------------------------------------------------------------------------- *)
+(* --- Validity --- *)
+(* -------------------------------------------------------------------------- *)
+
+let vset_from_validity = function
+ | Base.Empty -> Vset.empty
+ | Base.Invalid -> Vset.singleton F.e_zero
+ | Base.Known (min_valid, max_valid)
+
+ | Base.Unknown (min_valid, Some max_valid, _) ->
+ (* valid between min_valid .. max_valid inclusive *)
+ Vset.range (Some (F.e_bigint min_valid)) (Some (F.e_bigint max_valid))
+ | Base.Variable { Base.min_alloc = min_valid } ->
+ (* valid between 0 .. min_valid inclusive *)
+ Vset.range (Some F.e_zero) (Some (F.e_bigint min_valid))
+ | Base.Unknown (_, None, _) -> Vset.empty
+
+let r_valid acs r =
+ let for_writing = match acs with | RW | OBJ -> true | RD -> false in
+ let base, set = range_set r in
+ match RegisterBase.get base with
+ | None -> F.p_false (* For now. *)
+ | Some base ->
+ if for_writing && (Base.is_read_only base) then
+ F.p_false
+ else
+ Vset.subset set (vset_from_validity (Base.validity base))
+
+let valid : sigma -> acs -> segment -> pred = fun _s acs seg ->
+ r_valid acs (range seg)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Segment Inclusion --- *)
+(* -------------------------------------------------------------------------- *)
+
+let r_included r1 r2 = match r1, r2 with
+ (* | LOC (l1, n1), LOC (l2, n2) -> p_call p_included [l1;n1;l2;n2] *)
+ | _ ->
+ let base1, set1 = range_set r1 in
+ let base2, set2 = range_set r2 in
+ p_and (p_equal base1 base2) (Vset.subset set1 set2)
+
+let included : segment -> segment -> pred = fun s1 s2 ->
+ r_included (range s1) (range s2)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Segment Separation --- *)
+(* -------------------------------------------------------------------------- *)
+
+let r_separated r1 r2 = match r1, r2 with
+ (* | LOC (l1, n1), LOC (l2, n2) -> p_call p_separated [l1;n1;l2;n2] *)
+ | _ ->
+ let base1, set1 = range_set r1 in
+ let base2, set2 = range_set r1 in
+ p_imply (p_equal base1 base2) (Vset.disjoint set1 set2)
+
+let separated : segment -> segment -> pred = fun s1 s2 ->
+ r_separated (range s1) (range s2)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Domain --- *)
+(* -------------------------------------------------------------------------- *)
+
+let domain : c_object -> loc -> Sigma.domain = fun obj l -> match obj with
+ | C_int i -> Heap.Set.singleton (m_int i)
+ | C_float _ -> Heap.Set.singleton M_float
+ | C_pointer _ ->
+ begin try
+ List.fold_left (fun acc b -> Heap.Set.add (M_base b) acc)
+ Heap.Set.empty (Value.bases l.loc_v)
+ with Abstract_interp.Error_Top -> Heap.Set.empty end
+ | _ -> not_yet_obj obj
+
+(* -------------------------------------------------------------------------- *)
+
+
+let initialized _sigma _l = F.p_true (* todo *)
+let is_well_formed _ = F.p_true (* todo *)
+let base_offset _loc = assert false (** TODO *)
+type domain = Sigma.domain
+let no_binder = { bind = fun _ f v -> f v }
+let configure_ia _ = no_binder (* todo *)
+let hypotheses x = x (* todo *)
+let frame _sigma = [] (* todo *)
+let invalid = fun _ _ -> F.p_true (* TODO *)
diff --git a/src/plugins/wp/MemValue.mli b/src/plugins/wp/MemValue.mli
new file mode 100644
index 0000000000000000000000000000000000000000..7683b0e4c139fdeeb9c87f257cbfb0934a69fee5
--- /dev/null
+++ b/src/plugins/wp/MemValue.mli
@@ -0,0 +1,3 @@
+(* module Make(M : Memory.Model) : Memory.Model *)
+
+include Sigs.Model