Add header check

src/bin/loop.ml

@@ -5,7 +5,7 @@ module State = Dolmen_loop.State
 module Pipeline = Dolmen_loop.Pipeline.Make(State)
 
 module Parser = Dolmen_loop.Parser.Pipe(Dolmen.Std.Expr)(State)
-
+module Header = Dolmen_loop.Headers.Pipe(State)
 module Typer = struct
   module T = Dolmen_loop.Typer.Make(State)
   include T

src/bin/main.ml

@@ -41,12 +41,14 @@ let () =
     run ~finally g st (
       (fix (apply ~name:"expand" Loop.Parser.expand) (
           (apply ~name:"debug" debug_pipe)
+          @>>> (apply ~name:"headers" Loop.Header.inspect)
           @>>> (apply ~name:"typecheck" Loop.Typer.typecheck)
           @>|> ((apply fst) @>>> _end)
         )
       )
     )
   in
+  let st = Loop.Header.check st in
   let _st = Dolmen_loop.State.flush st () in
   ()
 

src/bin/options.ml

@@ -31,6 +31,7 @@ let mk_state
     gc gc_opt bt colors
     time_limit size_limit
     input_lang input_mode input
+    header_check header_licenses
     type_check type_strict
     debug context max_warn
   =
@@ -54,9 +55,11 @@ let mk_state
 
     input_dir; input_lang;
     input_mode; input_source;
-
     input_file_loc = Dolmen.Std.Loc.mk_file "";
 
+    header_check; header_licenses;
+    header_state = Dolmen_loop.Headers.empty;
+
     type_check; type_strict;
     type_state = Dolmen_loop.Typer.new_state ();
 
@@ -262,6 +265,16 @@ let state =
                dolmen will enter interactive mode and read on stdin." in
     Arg.(value & pos 0 input_source_conv `Stdin & info [] ~docv:"FILE" ~doc)
   in
+  let header_check =
+    let doc = "If true, then the presence of headers will be checked in the
+               input file (and errors raised if they are not present)." in
+    Arg.(value & opt bool false & info ["check-headers"] ~doc ~docs)
+  in
+  let header_licenses =
+    let doc = "Set the allowed set of licenses in the headers.
+               An empty list means allow everything." in
+    Arg.(value & opt (list string) [] & info ["header-licenses"] ~doc ~docs)
+  in
   let typing =
     let doc = "Decide whether to type-check input expressions. If false, only parsing
                is done. " in
@@ -297,6 +310,7 @@ let state =
   in
   Term.(const mk_state $ gc $ gc_t $ bt $ colors $
         time $ size $ in_lang $ in_mode $ input $
+        header_check $ header_licenses $
         typing $ strict $ debug $ context $ max_warn)
 
 

src/loop/dune

@@ -13,7 +13,7 @@
     )
   (modules
     ; Interfaces
-    Expr_intf Typer_intf State_intf
+    Expr_intf Typer_intf Headers_intf State_intf
     ; Implementations
-    Logic State Parser Typer Pipeline)
+    Logic State Parser Typer Headers Pipeline)
 )

src/loop/headers.ml

@@ -0,0 +1,242 @@
+
+(* 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 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 = Id.Attr; Id.name = ":smt-lib-version"; } ->
+        begin match args with
+          | [ { Ast.term = Ast.Symbol {
+                Id.ns = Id.Value Id.Real; Id.name = version }; _ } ] ->
+            Ok (Lang_version, version)
+          | [] -> Error (loc, "empty value for :smt-lib-version")
+          | { Ast.loc; _ } :: _ -> Error (loc, "Expected a version number")
+        end
+
+      (* Problem source *)
+      | { Id.ns = Id.Attr; Id.name = ":source"; } ->
+        begin match args with
+          | [ { Ast.term = Ast.Symbol {
+              Id.ns = Id.Attr; Id.name = 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 = Id.Attr; Id.name = ":license"; } ->
+        begin match args with
+          | [ { Ast.term = Ast.Symbol {
+              Id.ns = Id.Value Id.String; Id.name = 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 = Id.Attr; Id.name = ":category"; } ->
+        begin match args with
+          | [ { Ast.term = Ast.Symbol {
+              Id.ns = Id.Value Id.String; Id.name = category }; _ } ] ->
+            Ok (Problem_category, category)
+          | [] -> Error (loc, "empty value for :category")
+          | { Ast.loc; _ } :: _ -> Error (loc, "Expected a single string in quotes")
+        end
+
+
+      (* Problem status *)
+      | { Id.ns = Id.Attr; Id.name = ":status"; } ->
+        begin match args with
+          | [ { Ast.term = Ast.Symbol {
+              Id.name = (("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
+
+(* 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_fields_required : Field.t list = [
+  Lang_version;
+  Problem_source;
+  Problem_license;
+  Problem_category;
+  (* Problem_status is checked for every check-sat *)
+]
+
+
+(* Required headers for languages *)
+(* ************************************************************************ *)
+
+module Pipe(State : State_intf.Header_pipe
+            with type header_state := t)
+= struct
+
+  (* Final check for headers *)
+
+  let check_required st h =
+    let lang = State.input_lang st in
+    let required =
+      match lang with
+      | Some Logic.Smtlib2 _ -> smtlib2_fields_required
+      | _ -> []
+    in
+    match List.filter (fun f -> not (mem h f)) required with
+    | [] -> st
+    | missing ->
+      let pp_sep fmt () = Format.fprintf fmt ",@ " in
+      State.error st "The following header fields are missing: %a"
+        (Format.pp_print_list ~pp_sep (Field.print ?lang)) missing
+
+  let check st =
+    if not (State.check_headers st) then st
+    else begin
+      let h = State.header_state st in
+      check_required st h
+    end
+
+
+  (* Incremental checks and construction of the header set *)
+
+  let error st loc fmt =
+    let file = State.input_file_loc st in
+    let loc : Dolmen.Std.Loc.full = { file; loc; } in
+    State.error ~loc st fmt
+
+  let check_header st loc field value =
+    match (field : Field.t) with
+    | Problem_license ->
+      begin match State.allowed_licenses st with
+        | [] -> st
+        | allowed ->
+          if List.mem value allowed then st
+          else error st loc "This is not an allowed license"
+      end
+    | _ -> st
+
+  let inspect (st, c) =
+    if not (State.check_headers st) then (st, c)
+    else begin
+      let lang = State.input_lang st in
+      let h = State.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 "%s" msg
+            | Ok (field, value) ->
+              let st = check_header st loc field value in
+              let st = State.set_header_state st (set h field value) in
+              st
+          end
+        | { descr = Prove _; loc; _ } ->
+          if mem h Problem_status then
+            State.set_header_state st (remove h Problem_status)
+          else
+            error st loc "This statement lacks a %s header"
+              (Field.name lang Problem_status)
+        | _ -> st
+      in
+      st, c
+    end
+
+end
+

src/loop/headers.mli

@@ -0,0 +1,56 @@
+
+(* This file is free software, part of Dolmen. See file "LICENSE" for more details. *)
+
+(** {2 Header fields} *)
+
+module Field : sig
+
+  type t =
+    | Lang_version
+    | Problem_version
+    | Problem_source
+    | Problem_license
+    | Problem_category
+    | Problem_status (**)
+  (** Header fields. *)
+
+  val hash : t -> int
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+  (** Usual functions *)
+
+  val name : Logic.language option -> t -> string
+  (** Name of a header field, parameterized by language *)
+
+  val print : ?lang:Logic.language -> Format.formatter -> t -> unit
+  (** Print a header field (with the same string as {!name}). *)
+
+end
+
+(** {2 Header set} *)
+
+type t
+(** Header set, i.e. a map of fields to values for the header. *)
+
+val empty : t
+(** The empty header set *)
+
+val set : t -> Field.t -> string -> t
+(** Add/set a header to the corresponding value. *)
+
+val get : t -> Field.t -> string option
+(** Get a header value, if present in the set. *)
+
+val mem : t -> Field.t -> bool
+(** Test the presence of a header field. *)
+
+val remove : t -> Field.t -> t
+(** Remove a field from a set. *)
+
+(** {2 Pipe functor} *)
+
+module Pipe(State : State_intf.Header_pipe
+            with type header_state := t) :
+  Headers_intf.S with type state := State.t
+
+

src/loop/headers_intf.ml

@@ -0,0 +1,15 @@
+
+module type S = sig
+
+  type state
+  (** global state threaded through all the pipeline *)
+
+  val check : state -> state
+  (** Check a state for the required headers (once a whole pipeline
+      has been completed *)
+
+  val inspect :
+    state * Dolmen.Std.Statement.t -> state * Dolmen.Std.Statement.t
+  (** Check the headers *)
+
+end