Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381
(* This file is free software, part of Dolmen. See file "LICENSE" for more details. *)
(* Header check
This module defines a pipe to check the presence of headers in an input file. Headerts are there to provide meta-data about problems, such as version, source, classification, and even satisifability status in some cases. Note that this does *not* include the checking of constraints between successivestatements such as what smtlib specifies, see flow.ml
The way this check is implemented/done: - a number of meta-data fields are defines in module [Field], together with ways to parse/print them. - then each language defines its list of headers that are: + required (causing an error if they are absent) + wanted (causing a warning if they are absent) - additionally, some checks are performed on the values of some headers, particularly lang_version and license, which are provided by the state (and usually controlled by the command line, as there are not reasonable defaults for them). - finally the pipe accumulates header (parsing them using the functions from the [Field] module, and a checking function is provided to check the presence of headers at the end of the file processing.
Note that the current way means that headers can theoretically be present anywhere in the file, rather than at the beginning.*)
(* Header fields *)(* ************************************************************************ *)
module Field = struct
type t = | Lang_version | Problem_version | Problem_source | Problem_license | Problem_category | Problem_status
let equal = (=) let compare = compare let hash = Hashtbl.hash
(* Correspondance between fields and their names in languages *) let name lang field = match lang, field with | Some Logic.Smtlib2 _, Lang_version -> ":smt-lib-version" | Some Logic.Smtlib2 _, Problem_source -> ":source" | Some Logic.Smtlib2 _, Problem_license -> ":license" | Some Logic.Smtlib2 _, Problem_category -> ":category" | Some Logic.Smtlib2 _, Problem_status -> ":status" | _, Lang_version -> "Language version" | _, Problem_version -> "Problem version" | _, Problem_source -> "Problem source" | _, Problem_license -> "Problem license" | _, Problem_category -> "Problem_category" | _, Problem_status -> "Problem status"
let print ?lang fmt field = Format.fprintf fmt "%s" (name lang field)
(* Parse an attribute into an (optional) field and value. *)
module Id = Dolmen.Std.Id module Loc = Dolmen.Std.Loc module Ast = Dolmen.Std.Term
type res = | Ok of t * string | Error of Loc.t * string | Not_a_header
module Smtlib2 = struct
let check_version_number version = if String.length version >= 3 && String.sub version 0 2 = "2." then begin try let s = String.sub version 2 (String.length version - 2) in let _ = int_of_string s in true with Failure _ -> false end else false
let rec parse = function | { Ast.term = Ast.App ({ Ast.term = Ast.Symbol s; _ }, args); loc; _ } -> parse_aux loc s args | _ -> Not_a_header
and parse_aux loc s args = match s with
(* Language version *) | { Id.ns = Attr; Id.name = Simple ":smt-lib-version"; } -> begin match args with | [ { Ast.term = Ast.Symbol { Id.ns = Value Real; Id.name = Simple version; }; _ } ] -> if check_version_number version then Ok (Lang_version, version) else Error (loc, ":smt-lib-version number must be in the form 2.X") | [] -> Error (loc, "empty value for :smt-lib-version") | { Ast.loc; _ } :: _ -> Error (loc, "Expected a version number") end
(* Problem source *) | { Id.ns = Attr; Id.name = Simple ":source"; } -> begin match args with | [ { Ast.term = Ast.Symbol { Id.ns = (Attr | Term | Value String); Id.name = Simple descr }; _ } ] -> Ok (Problem_source, descr) | [] -> Error (loc, "empty value for :source") | { Ast.loc; _ } :: _ -> Error (loc, "Expected a single symbol as description") end
(* Problem license *) | { Id.ns = Attr; Id.name = Simple ":license"; } -> begin match args with | [ { Ast.term = Ast.Symbol { Id.ns = Value String; Id.name = Simple license }; _ } ] -> Ok (Problem_license, license) | [] -> Error (loc, "empty value for :license") | { Ast.loc; _ } :: _ -> Error (loc, "Expected a single string in quotes") end
(* Problem category *) | { Id.ns = Attr; Id.name = Simple ":category"; } -> begin match args with | [ { Ast.term = Ast.Symbol { Id.ns = Value String; Id.name = Simple (("crafted"|"random"|"industrial") as category) }; _ }; ] -> Ok (Problem_category, category) | [] -> Error (loc, "empty value for :category") | { Ast.loc; _ } :: _ -> Error (loc, {|Expected "crafted", "random", or "industrial" (in quotes)|}) end
(* Problem status *) | { Id.ns = Attr; Id.name = Simple ":status"; } -> begin match args with | [ { Ast.term = Ast.Symbol { Id.name = Simple (("sat"|"unsat"|"unknown") as status) ; _ }; _ }; ] -> Ok (Problem_status, status) | _ -> Error (loc, "Expected sat|unsat|unknown") end
(* catch-all *) | _ -> Not_a_header
end
let parse ?lang t = match lang with | Some Logic.Smtlib2 _ -> Smtlib2.parse t | _ -> Not_a_header
end
(* Header errors & warnings *)(* ************************************************************************ *)
let code = Code.create ~category:"Header" ~descr:"on header errors"
let missing_header_error = Report.Error.mk ~code ~mnemonic:"header-missing" ~message:(fun fmt (lang, missing) -> let pp_sep fmt () = Format.fprintf fmt ",@ " in Format.fprintf fmt "The following header fields are missing: %a" (Format.pp_print_list ~pp_sep (Field.print ?lang)) missing) ~name:"Missing header statement" ()
let invalid_header_value_error = Report.Error.mk ~code ~mnemonic:"header-invalid-value" ~message:(fun fmt (field, lang, msg) -> Format.fprintf fmt "Invalid value for header %a: %s" (Field.print ?lang) field msg) ~name:"Invalid header value" ()
let bad_header_payload = Report.Error.mk ~code ~mnemonic:"header-bad-payload" ~message:(fun fmt msg -> Format.fprintf fmt "Could not parse the header: %s" msg) ~name:"Incorrect header payload" ()
let empty_header_field = Report.Warning.mk ~code ~mnemonic:"empty-header-field" ~message:(fun fmt (lang, l) -> let pp_sep fmt () = Format.fprintf fmt ",@ " in Format.fprintf fmt "The following header fields are missing and thus \ default values will be assumed: %a" (Format.pp_print_list ~pp_sep (Field.print ?lang)) l) ~name:"Header field with a missing value" ()
(* Headers *)(* ************************************************************************ *)
module M = Map.Make(Field)
type t = { fields : string M.t;}
let empty = { fields = M.empty;}
let set h f v = { fields = M.add f v h.fields;}
let remove h f = { fields = M.remove f h.fields;}
let get h f = try Some (M.find f h.fields) with Not_found -> None
let mem h f = M.mem f h.fields
(* Required headers for languages *)(* ************************************************************************ *)
let smtlib2_required : Field.t list = [ Lang_version; Problem_source; Problem_category; (* Problem_status is checked for every check-sat *)]
let smtlib2_wanted : Field.t list = [ Problem_license;]
(* Required headers for languages *)(* ************************************************************************ *)
module type S = Headers_intf.S
module Make(State : State.S) = struct
let pipe = "Headers"
let header_check : bool State.key = State.create_key ~pipe "header_check"
let header_state : t State.key = State.create_key ~pipe "header_state"
let header_licenses : string list State.key = State.create_key ~pipe "header_licenses"
let header_lang_version : string option State.key = State.create_key ~pipe "header_lang_version"
let init ~header_check:header_check_value ?header_state:(header_state_value=empty) ~header_licenses:header_licenses_value ~header_lang_version:header_lang_version_value st = st |> State.set header_check header_check_value |> State.set header_state header_state_value |> State.set header_licenses header_licenses_value |> State.set header_lang_version header_lang_version_value
(* Final check for headers *)
let check_wanted st h = let lang = (State.get State.logic_file st).lang in let wanted = match lang with | Some Logic.Smtlib2 _ -> smtlib2_wanted | _ -> [] in match List.filter (fun f -> not (mem h f)) wanted with | [] -> st | missing -> State.warn st empty_header_field (lang, missing)
let check_required st h = let lang = (State.get State.logic_file st).lang in let required = match lang with | Some Logic.Smtlib2 _ -> smtlib2_required | _ -> [] in match List.filter (fun f -> not (mem h f)) required with | [] -> st | missing -> State.error st missing_header_error (lang, missing)
(* Incremental checks and construction of the header set *)
let error st loc err param = let file = (State.get State.logic_file st).loc in let loc : Dolmen.Std.Loc.full = { file; loc; } in State.error ~loc st err param
let invalid_header_value st loc field msg = let lang = (State.get State.logic_file st).lang in error st loc invalid_header_value_error (field, lang, msg)
let check_header st loc field value = match (field : Field.t) with | Lang_version -> begin match State.get header_lang_version st with | None -> st | Some v -> if v = value then st else invalid_header_value st loc Lang_version (Format.sprintf "language version must be: %s" v) end | Problem_license -> begin match State.get header_licenses st with | [] -> st | allowed -> if List.mem value allowed then st else invalid_header_value st loc Problem_license "this license is not in the list of allowed licenses" end | _ -> st
let inspect st c = if not (State.get header_check st) then (st, c) else begin let lang = (State.get State.logic_file st).lang in let h = State.get header_state st in let st = match (c : Dolmen.Std.Statement.t) with | { descr = Set_info t; loc; _ } -> begin match Field.parse ?lang t with | Not_a_header -> st | Error (loc, msg) -> error st loc bad_header_payload msg | Ok (field, value) -> let st = check_header st loc field value in let st = State.set header_state (set h field value) st in st end | { descr = Prove _; loc; _ } -> if mem h Problem_status then State.set header_state (remove h Problem_status) st else error st loc missing_header_error (lang, [Problem_status]) | { descr = End; _ } -> let st = check_wanted st h in let st = check_required st h in st | _ -> st in st, c end
end