Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452
(* Flow check
This module defined a pipe to check the coherence of the sequence of statements in a file. This is pertinent for non-declarative languages, such as smtlib (whereas languages such as TPTP are coherent by design).*)
module S = State
(* Automaton *)(* ************************************************************************ *)
module type Automaton = sig type st type node type statement
val init : node val step : st -> node -> statement -> st * nodeend
(* Dummy automaton *)(* ************************************************************************ *)
module Dummy = struct type node = unit let init = () let step st () _ = st, ()end
(* Smtlib automaton *)(* ************************************************************************ *)
let code = Code.create ~category:"Flow" ~descr:"on flow verification errors"
let ignored_statement = Report.Warning.mk ~code ~mnemonic:"ignored-statement" ~message:(fun fmt () -> Format.fprintf fmt "%a" Format.pp_print_text "This statement is effectively ignored: there is no check-sat/prove \ statement between it and a following pop/exit/reset statement.") ~name:"Ignored Statement" ()
let unclosed_push = Report.Warning.mk ~code ~mnemonic:"unclosed-push" ~message:(fun fmt () -> Format.fprintf fmt "%a" Format.pp_print_text "This push statement was not closed") ~hints:[fun () -> Some (Format.dprintf "%a" Format.pp_print_text "You can close a push statement with one of the following statements: \ pop, reset, reset-assertions.") ] ~name:"Unclosed Push" ()
let pop_without_push = Report.Error.mk ~code ~mnemonic:"pop-without-push" ~message:(fun fmt () -> Format.fprintf fmt "%a" Format.pp_print_text "This pop statement is missing a corresponding 'push' statement.") ~name:"Pop without a Push" ()
let missing_exit = Report.Error.mk ~code ~mnemonic:"missing-exit" ~message:(fun fmt () -> Format.fprintf fmt "Missing exit statement") ~name:"Missing Exit statement" ()
let stmt_after_exit = Report.Error.mk ~code ~mnemonic:"stmt-after-push" ~message:(fun fmt () -> Format.fprintf fmt "Statement after an exit") ~name:"Statement after an Exit" ()
let forbidden_stmt = Report.Error.mk ~code ~mnemonic:"forbidden-stmt" ~message:(fun fmt msg -> Format.fprintf fmt "Forbidden statement: %a" Format.pp_print_text msg) ~name:"Forbidden Statement" ()
module Smtlib2(State : State.S) : Automaton with type st := State.t and type statement := Dolmen.Std.Statement.t= struct
type loc = { file : Logic.language S.input_file; loc : Dolmen.Std.Loc.t; }
(* Smtlib transitions, the reference is page 53 of: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
However, here we are insterested in doing a bit more, and actually ensuring that any assertions is never "lost". For instance, consider the following: ```smt2 (set-logic ALL) (assert true) (check-sat) (assert false) (exit) ``` The last assertion is effectively lost, and cannot be used, which is most likely an error. While such a situation is not likely to happen in regular problems, once you add push/pop operations, it is much easier to end up in such a situation. *) type assert_level = { start : loc; (* None for top-level, Some push.loc for levels pushed *) stmts : loc list; (* asserts and declares/defines for the current level *) }
type assert_stack = { top : loc list; stack: assert_level list; }
type node = | Start_mode | Assert_mode of assert_stack | Sat_or_unsat_mode of assert_stack | Exited
(* Reporting helpers *)
let loc st (stmt : Dolmen.Std.Statement.t) = let file = State.get State.logic_file st in { file; loc = stmt.loc; }
let lose_stmts st l = List.fold_left (fun st { file; loc } -> let loc : Dolmen.Std.Loc.full = { file = file.loc; loc; } in State.warn ~file ~loc st ignored_statement () ) st l
let after_exit st stmt = let { file; loc; } = loc st stmt in let loc : Dolmen.Std.Loc.full = { file = file.loc; loc; } in State.error ~file ~loc st stmt_after_exit (), Exited
let forbidden st mode stmt msg = let { file; loc; } = loc st stmt in let loc : Dolmen.Std.Loc.full = { file = file.loc; loc; } in State.error ~file ~loc st forbidden_stmt msg, mode
let no_set_logic st mode stmt = forbidden st mode stmt "missing set-logic statement prior to this one"
(* Automaton helpers *)
let add st { top; stack; } stmt = match stack with | [] -> { top = loc st stmt :: top; stack; } | { start; stmts; } :: r -> { top; stack = { start; stmts = loc st stmt :: stmts; } :: r; }
let push stmt (st, { top; stack; }) = st, { top; stack = { start = loc st stmt; stmts = []; } :: stack; }
let pop stmt (st, { top; stack; }) = match stack with | [] -> let loc = loc st stmt in let file = loc.file in let loc : Dolmen.Std.Loc.full = { file = file.loc; loc = loc.loc; } in let st = State.error ~file ~loc st pop_without_push () in st, { top; stack = []; } | { start = _; stmts; } :: r -> let st = lose_stmts st stmts in st, { top; stack = r; }
let check_sat { top = _; stack; } = let stack = List.map (fun { start; stmts = _ } -> { start; stmts = []; }) stack in { top = []; stack; }
let reset_assertions ~explicit st { top; stack; } = let st = match stack with | [] -> st | (_ :: _) as l -> List.fold_left (fun st { start = { file; loc; }; stmts; } -> let st = if explicit then st else begin let loc : Dolmen.Std.Loc.full = { file = file.loc; loc; } in State.warn ~file ~loc st unclosed_push () end in lose_stmts st stmts ) st l in let st = lose_stmts st top in st, { top = []; stack = []; }
(* Automaton functions *)
let init = Start_mode
let step st mode (stmt : Dolmen.Std.Statement.t) = match stmt.descr with
(* this *) | End -> begin match mode with | Exited -> st, mode | Start_mode -> let file = State.get State.logic_file st in State.error st ~file missing_exit (), mode | Assert_mode stack | Sat_or_unsat_mode stack -> (* check for "lost" statements or unclosed "pushs" *) let st, _stack = reset_assertions ~explicit:false st stack in let file = State.get State.logic_file st in State.error st ~file missing_exit (), mode end
(* these should not happen, just ignore them (TODO: emit warning ?) *) | Pack _ | Include _ -> begin match mode with | Start_mode | Assert_mode _ | Sat_or_unsat_mode _ -> st, mode | Exited -> after_exit st stmt end
(* non smtlib ref case *) | Exit -> begin match mode with | Start_mode -> st, Exited | Assert_mode stack | Sat_or_unsat_mode stack -> let st, _stack = reset_assertions ~explicit:false st stack in st, Exited | Exited -> after_exit st stmt end
(* smtlib ref case: 'gsio' *) | Other _ | Get_info _ | Set_info _ | Get_option _ | Set_option _ -> begin match mode with | Start_mode | Assert_mode _ | Sat_or_unsat_mode _ -> st, mode | Exited -> after_exit st stmt end
(* smtlib ref case: 'e' *) | Echo _ -> begin match mode with | Start_mode | Assert_mode _ | Sat_or_unsat_mode _ -> st, mode | Exited -> after_exit st stmt end
(* smtlib ref case: 'sl' *) | Set_logic _ -> begin match mode with | Start_mode -> st, Assert_mode { top = []; stack = []; } | Assert_mode _ | Sat_or_unsat_mode _ -> forbidden st mode stmt "there is already a previous set-logic statement" | Exited -> after_exit st stmt end
(* smtlib ref case: 'g' *) | Get_assertions -> begin match mode with | Start_mode -> no_set_logic st mode stmt | Assert_mode _ | Sat_or_unsat_mode _ -> st, mode | Exited -> after_exit st stmt end
(* smtlib ref case: 'r' *) | Reset -> begin match mode with | Start_mode -> st, Start_mode | Assert_mode stack | Sat_or_unsat_mode stack -> let st, _stack = reset_assertions ~explicit:true st stack in st, Start_mode | Exited -> after_exit st stmt end
(* smtlib ref case: 'ra' *) | Reset_assertions -> begin match mode with | Start_mode -> st, Start_mode | Assert_mode stack | Sat_or_unsat_mode stack -> let st, stack = reset_assertions ~explicit:true st stack in st, Assert_mode stack | Exited -> after_exit st stmt end
(* stmlib ref case: 'p' *) | Pop n -> begin match mode with | Start_mode -> no_set_logic st mode stmt | Assert_mode stack | Sat_or_unsat_mode stack -> let st, stack = Dolmen.Std.Misc.foldn n (pop stmt) (st, stack) in st, Assert_mode stack | Exited -> after_exit st stmt end | Push n -> begin match mode with | Start_mode -> no_set_logic st mode stmt | Assert_mode stack | Sat_or_unsat_mode stack -> let st, stack = Dolmen.Std.Misc.foldn n (push stmt) (st, stack) in st, Assert_mode stack | Exited -> after_exit st stmt end
(* smtlib ref case: 'ad' *) | Defs _ | Decls _ | Clause _ | Antecedent _ | Consequent _ -> begin match mode with | Start_mode -> no_set_logic st mode stmt | Assert_mode stack | Sat_or_unsat_mode stack -> let stack = add st stack stmt in st, Assert_mode stack | Exited -> after_exit st stmt end
(* smtlib ref case: 'c' *) | Prove _ -> begin match mode with | Start_mode -> no_set_logic st mode stmt | Assert_mode stack -> let stack = check_sat stack in st, Sat_or_unsat_mode stack | Sat_or_unsat_mode _ -> st, mode | Exited -> after_exit st stmt end
(* smtlib ref case: 'gpu' *) | Get_proof | Get_unsat_core | Get_unsat_assumptions -> begin match mode with | Start_mode -> no_set_logic st mode stmt | Assert_mode _ -> forbidden st mode stmt "missing check-sat prior to this statement" | Sat_or_unsat_mode _ -> st, mode | Exited -> after_exit st stmt end
(* smtlib ref case: 'gamv' *) | Get_model | Get_value _ | Get_assignment -> begin match mode with | Start_mode -> no_set_logic st mode stmt | Assert_mode _ -> forbidden st mode stmt "missing check-sat prior to this statement" | Sat_or_unsat_mode _ -> st, mode | Exited -> after_exit st stmt end
end
(* Pipe *)(* ************************************************************************ *)
module type S = Flow_intf.S
module Make(State : State.S) = struct
module type S = Automaton with type st := State.t and type statement := Dolmen.Std.Statement.t
module Smtlib2 = Smtlib2(State)
type 'node automaton = 'node * (module S with type node = 'node)
type state = | No_check | Check_init | Check : 'node automaton -> state
type aux = { f : 'node. State.t -> 'node automaton -> State.t; }
let state_key : state State.key = State.create_key ~pipe:"flow" "flow_state"
let init ~flow_check st = let state = if flow_check then Check_init else No_check in State.set state_key state st
let with_automaton st ~check = match State.get state_key st with | No_check -> st | Check_init -> let (module Automaton : S) = let logic_file = State.get State.logic_file st in match logic_file.lang with | Some Smtlib2 _ -> (module Smtlib2) | _ -> (module Dummy) in check.f st (Automaton.init, (module Automaton)) | Check automaton -> check.f st automaton
let inspect_aux (type node) st c ((node,(module Automaton)) : node automaton) = let st, node = Automaton.step st node c in State.set state_key (Check (node, (module Automaton))) st
let inspect st c = let st = with_automaton st ~check:{ f = fun st automaton -> inspect_aux st c automaton } in st, c
end