-
Patrick Baudin authoredPatrick Baudin authored
Pcond.ml 16.48 KiB
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2022 *)
(* 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). *)
(* *)
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
module F = Lang.F
module Env = Plang.Env
open F
let dkey_state = Wp_parameters.register_category "state"
type env = Plang.Env.t
let rec alloc_hyp pool f seq =
let open Conditions in
if not (Vars.subset (Conditions.vars_hyp seq) (Plang.alloc_domain pool))
then
Conditions.iter
(fun step ->
if not (Vars.subset step.vars (Plang.alloc_domain pool)) then
match step.condition with
| State _ ->
Plang.alloc_xs pool f step.vars
| Have p | When p | Type p | Init p | Core p ->
Plang.alloc_p pool f p
| Branch(p,sa,sb) ->
Plang.alloc_p pool f p ;
alloc_hyp pool f sa ;
alloc_hyp pool f sb ;
| Either cases -> List.iter (alloc_hyp pool f) cases
) seq
let alloc_seq pool f (hs,g) =
begin
Plang.alloc_p pool f g ; (* Mark goal first *)
alloc_hyp pool f hs ;
end
(* -------------------------------------------------------------------------- *)
(* --- State Printer --- *)
(* -------------------------------------------------------------------------- *)
type context = NoWhere | InAddr | AtLabel of Pcfg.label
class state =
object(self)
inherit Plang.engine as super
inherit Pcfg.engine
val mutable env = Pcfg.create ()
val mutable context = NoWhere
val mutable domain = Vars.empty
method clear =
begin
env <- Pcfg.create () ;
context <- NoWhere ;
domain <- Vars.empty ;
end
method set_sequence seq =
begin
env <- Pcfg.register seq ;
context <- NoWhere ;
domain <- Conditions.vars_hyp seq ;
end
method domain = domain
method set_domain vars = domain <- vars
method label_at ~id = Pcfg.at env ~id
method private at : 'a. ?lbl:Pcfg.label ->
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit =
begin fun ?lbl pp fmt w ->
match context , lbl with
| NoWhere , None ->
context <- InAddr ;
Format.fprintf fmt "« %a »" pp w ;
context <- NoWhere ;
| NoWhere , Some l ->
context <- AtLabel l ;
Format.fprintf fmt "« %a »%a" pp w self#pp_at l ;
context <- NoWhere ;
| InAddr , None -> pp fmt w
| AtLabel _ , None -> pp fmt w
| AtLabel l0 , Some l when l == l0 -> pp fmt w
| (InAddr | AtLabel _) as here , Some l ->
context <- AtLabel l ;
Format.fprintf fmt "( %a )%a" pp w self#pp_at l ;
context <- here ;
end
method private atflow : 'a. ?lbl:Pcfg.label ->
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit =
begin fun ?lbl pp fmt w ->
match context , lbl with
| NoWhere , None ->
context <- InAddr ;
pp fmt w ;
context <- NoWhere ;
| InAddr , None -> pp fmt w
| AtLabel _ , None -> pp fmt w
| AtLabel l0 , Some l when l == l0 -> pp fmt w
| (InAddr | AtLabel _ | NoWhere) as here , Some l ->
context <- AtLabel l ;
Format.fprintf fmt "%a%a" pp w self#pp_at l ;
context <- here ;
end
method pp_at fmt lbl = Format.fprintf fmt "@@%a" self#pp_label lbl
val mutable force = false
method! pp_var fmt x = Format.pp_print_char fmt '`' ; Format.pp_print_string fmt x
method! pp_repr fmt e =
if force then (force <- false ; super#pp_repr fmt e) else
begin
match Pcfg.find env e with
| Pcfg.Term -> super#pp_repr fmt e
| Pcfg.Addr lv ->
if self#is_atomic_lv lv then self#atflow self#pp_addr fmt lv
else self#at self#pp_addr fmt lv
| Pcfg.Lval(lv,lbl) ->
if self#is_atomic_lv lv
then self#atflow ~lbl self#pp_lval fmt lv
else self#at ~lbl self#pp_lval fmt lv
| Pcfg.Init(lv,lbl) ->
if self#is_atomic_lv lv
then self#atflow ~lbl self#pp_init fmt lv
else self#at ~lbl self#pp_init fmt lv
| Pcfg.Chunk(m,lbl) ->
self#atflow ~lbl self#pp_chunk fmt m
end
method pp_value fmt e = force <- true ; super#pp_sort fmt e
method! pp_sort fmt e = context <- NoWhere ; super#pp_sort fmt e
method! pp_term fmt e = context <- NoWhere ; super#pp_term fmt e
method! pp_pred fmt p = context <- NoWhere ; super#pp_pred fmt p
method! subterms f e =
if not (Pcfg.subterms env f e) then super#subterms f e
method updates seq = Pcfg.updates env seq domain
method pp_update lbl fmt = function Sigs.Mstore(lv,v) ->
let stack = context in
context <- AtLabel lbl ;
Format.fprintf fmt "@[<hov 2>%a =@ %a;@]"
self#pp_lval lv self#pp_value v ;
context <- stack ;
end
(* -------------------------------------------------------------------------- *)
(* --- Sequent Printer --- *)
(* -------------------------------------------------------------------------- *)
open Conditions
let mark_step m step =
(* sub-sequences are marked recursively marked later *)
match step.condition with
| When p | Type p | Have p | Init p | Core p
| Branch(p,_,_) -> F.mark_p m p
| Either _ | State _ -> ()
let spaced pp fmt a = Format.pp_print_space fmt () ; pp fmt a
let append pp fmt a = pp fmt a ; Format.pp_print_space fmt ()
let pp_open_block pp fmt a left =
Format.fprintf fmt "@[<hv 0>@[<hv 2>%a %s" pp a left
let pp_close_block fmt right =
Format.fprintf fmt "@]@ %s@]" right
class engine (lang : #Plang.engine) =
object(self)
(* -------------------------------------------------------------------------- *)
(* --- Horizontal Printers --- *)
(* -------------------------------------------------------------------------- *)
method pp_clause fmt s = Format.fprintf fmt "@{<wp:clause>%s@}" s
method pp_stmt fmt s = Format.fprintf fmt "@{<wp:stmt>%s@}" s
method pp_name = Format.pp_print_string
method pp_core = lang#pp_sort
method pp_comment fmt s =
Format.fprintf fmt "@[<hov 0>@{<wp:comment>(* %s *)@}@]" s
method pp_property fmt p =
Format.fprintf fmt "@[<hov 0>@{<wp:property>(* %a *)@}@]"
Description.pp_local p
method pp_warning fmt w =
let open Warning in Format.fprintf fmt "@[<hov 0>@{<wp:warning>Warning@}[%s]: %s@ (%s).@]"
w.source w.reason w.effect
method pp_definition fmt x e =
Format.fprintf fmt "@[<hov 4>%a %a = %a.@]"
self#pp_clause "Let" self#pp_name x self#pp_core e
method pp_intro ~step ~clause ?(dot=".") fmt p =
ignore step ;
Format.fprintf fmt "@[<hov 4>%a %a%s@]"
self#pp_clause clause lang#pp_pred p dot
(* -------------------------------------------------------------------------- *)
(* --- Block Printers --- *)
(* -------------------------------------------------------------------------- *)
method pp_condition ~step fmt = function
| State _ -> ()
| Core p -> self#pp_intro ~step ~clause:"Core:" fmt p
| Type p -> self#pp_intro ~step ~clause:"Type:" fmt p
| Init p -> self#pp_intro ~step ~clause:"Init:" fmt p
| Have p -> self#pp_intro ~step ~clause:"Have:" fmt p
| When p -> self#pp_intro ~step ~clause:"When:" fmt p
| Branch(p,sa,sb) ->
begin
self#pp_intro ~step ~clause:"If" ~dot:"" fmt p ;
if not (Conditions.is_true sa)
then self#sequence ~clause:"Then" fmt sa ;
if not (Conditions.is_true sb)
then self#sequence ~clause:"Else" fmt sb ;
end
| Either cases ->
begin
pp_open_block self#pp_clause fmt "Either" "{" ;
List.iter
(fun seq ->
Format.fprintf fmt "@ @[<hv 2>%a" self#pp_clause "Case:" ;
self#block fmt seq ;
Format.fprintf fmt "@]" ;
) cases ;
pp_close_block fmt "}" ;
end
method pp_step fmt step =
match step.condition with
| State _ ->
self#pp_condition ~step fmt step.condition
| _ ->
begin
( match step.descr with None -> () | Some s ->
spaced self#pp_comment fmt s ) ;
Warning.Set.iter (spaced self#pp_warning fmt) step.warn ;
List.iter (spaced self#pp_property fmt) step.deps ;
spaced (self#pp_condition ~step) fmt step.condition ;
end
method private sequence ~clause fmt seq =
Format.pp_print_space fmt () ; self#pp_block ~clause fmt seq
method pp_block ~clause fmt seq =
if Conditions.is_true seq then
Format.fprintf fmt "%a {}" self#pp_clause clause
else
begin
pp_open_block self#pp_clause fmt clause "{";
self#block fmt seq ;
pp_close_block fmt "}" ;
end
method private dump fmt seq () = alloc_seq (Plang.pool ()) (fun x -> ignore (lang#bind x)) seq ;
let env,marks = lang#marks in
let hs,goal = seq in
F.mark_p marks goal ;
Conditions.iter (self#mark marks) hs ;
Format.fprintf fmt "@[<hv 0>" ;
List.iter (append (self#define env) fmt) (F.defs marks) ;
lang#set_env env ;
if not (Conditions.is_true hs) then
begin
self#pp_block ~clause:"Assume" fmt hs ;
Format.pp_print_newline fmt () ;
end ;
self#pp_goal fmt goal ;
Format.fprintf fmt "@]@."
method pp_goal fmt goal =
Format.fprintf fmt "@[<hov 4>%a %a.@]"
self#pp_clause "Prove:" lang#pp_pred goal
method pp_sequence ~clause fmt seq =
lang#global (fun () -> self#pp_block ~clause fmt seq)
method pp_sequent fmt seq =
lang#global (self#dump fmt seq)
method pp_esequent env fmt seq =
lang#set_env env ;
self#dump fmt seq ()
(* --- Scope Management --- *)
method mark m s = mark_step m s
method name env e = Env.fresh env ~sanitizer:lang#sanitize (F.basename e)
method private define env fmt e =
let name = self#name env e in
lang#scope env (fun () -> self#pp_definition fmt name e) ;
Env.define env name e
method private block fmt seq =
begin
let env,marks = lang#marks in
Conditions.iter (self#mark marks) seq ;
List.iter (spaced (self#define env) fmt) (F.defs marks) ;
lang#scope env (fun () -> Conditions.iter (self#pp_step fmt) seq) ;
end
end
(* -------------------------------------------------------------------------- *)
(* --- All-In-One Printers --- *)
(* -------------------------------------------------------------------------- *)
let is_nop = function None -> true | Some(_,upd) -> Bag.is_empty upd
class seqengine (lang : #state) =
object(self)
inherit engine lang as super
method private label step = function
| State _ ->
(try Some (lang#label_at ~id:step.id)
with Not_found -> None)
| _ -> None
method private updates fmt = function
| None -> ()
| Some( lbl , upd ) ->
if not (Bag.is_empty upd) then
Bag.iter ((spaced (lang#pp_update lbl)) fmt) upd
method! pp_condition ~step fmt cond =
match self#label step cond with
| None -> super#pp_condition ~step fmt cond
| Some lbl ->
let before = match Pcfg.prev lbl with
| [ pre ] when (Pcfg.branching pre) ->
let seq = Sigs.{ pre ; post = lbl } in
let upd = lang#updates seq in
Some(pre,upd)
| _ -> None in
let after = match Pcfg.next lbl with
| [ post ] ->
let seq = Sigs.{ pre = lbl ; post } in
let upd = lang#updates seq in
Some(lbl,upd)
| _ -> None in
if Pcfg.visible lbl || not (is_nop before) || not (is_nop after)
|| Wp_parameters.debug_atleast 1
then
lang#with_mode Qed.Engine.Mterm
(fun _mode ->
begin
Format.fprintf fmt "@ @[<hv 0>@[<hv 2>%a {" self#pp_stmt "Stmt" ;
self#updates fmt before ;
if Pcfg.visible lbl then
Format.fprintf fmt "@ %a:" lang#pp_label lbl ;
if Wp_parameters.debug_atleast 1 then
begin
if not (Pcfg.visible lbl) then
Format.fprintf fmt "@ label %a:" lang#pp_label lbl ;
List.iter
(fun lbl -> Format.fprintf fmt "@ from %a;" lang#pp_label lbl)
(Pcfg.prev lbl) ;
List.iter
(fun lbl -> Format.fprintf fmt "@ goto %a;" lang#pp_label lbl)
(Pcfg.next lbl) ;
(*
Pcfg.iter
(fun _m v ->
if Vars.intersect lang#domain (F.vars v) then
Format.fprintf fmt "@ (%a := %a)"
lang#pp_term v lang#pp_value v
) lbl ;
*)
end ;
self#updates fmt after ;
Format.fprintf fmt " @]@ }@]" ;
end)
val mutable active = true
method set_state s = active <- s
method get_state = active
method set_sequence seq =
if active then
lang#set_sequence seq
else
lang#clear
method set_goal p =
lang#set_domain (Vars.union lang#domain (F.varsp p))
method set_sequent (hs,p) =
self#set_sequence hs ; self#set_goal p
method! pp_sequence ~clause fmt seq =
begin
self#set_sequence seq ;
super#pp_sequence ~clause fmt seq ; end
method! pp_sequent fmt seq =
begin
self#set_sequent seq ;
super#pp_sequent fmt seq ;
end
method! pp_esequent env fmt seq =
begin
self#set_sequent seq ;
super#pp_esequent env fmt seq ;
end
end
(* -------------------------------------------------------------------------- *)
(* --- All-In-One Printers --- *)
(* -------------------------------------------------------------------------- *)
let engine () =
if Wp_parameters.has_dkey dkey_state then
( new seqengine (new state) :> engine )
else
new engine (new Plang.engine)
let pretty fmt seq =
(engine())#pp_sequent fmt seq
let () = Conditions.pretty := pretty
let dump_sequence ?(clause="Sequence") ?goal fmt seq =
let plang = new Plang.engine in
let pcond = new engine plang in
plang#global
begin fun () ->
pcond#pp_block ~clause fmt seq ;
match goal with
| None -> ()
| Some g -> Format.fprintf fmt "@ @[<hov 2>Prove %a@]" plang#pp_pred g
end
let dump_bundle ?clause ?goal fmt bundle =
dump_sequence ?clause ?goal fmt (Conditions.bundle bundle)
let dump = dump_bundle ?goal:None ~clause:"Bundle"