formalsec / smtml / 555

Committed 01 Jul 2026 02:55PM UTC coverage: 44.611% (-1.8%) from 46.445%

Build # 555

Build Type

push

github

Committed by

filipeom

Commit Message

Use explicit result return in smtml parsing functions

It already bit me in the ass by not treating exceptions in injector.
With explicit types I'm forced to treat them and also it allows me to
use monadic syntax.

Coverage Stats

17 of 48 new or added lines in 9 files covered. (35.42%)

368 existing lines in 3 files now uncovered.

2384 of 5344 relevant lines covered (44.61%)

38.81 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

58.62

/src/smtml/parse.ml

(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2026 formalsec *)
(* Written by the Smtml programmers *)

module Smtml = struct
  open Lexer
  open Lexing

  let pp_pos fmt lexbuf =
    let pos = lexbuf.lex_curr_p in
    Fmt.pf fmt "%s:%d:%d" pos.pos_fname pos.pos_lnum
      (pos.pos_cnum - pos.pos_bol + 1)

  let parse_with_error parser lexbuf =
    try Ok (parser Lexer.token lexbuf) with
    | SyntaxError msg -> Fmt.error_msg "%a: %s" pp_pos lexbuf msg
    | Parser.Error -> Fmt.error_msg "%a: syntax error" pp_pos lexbuf

  module Script = struct
    let from_file filename =
      let open Result.Syntax in
      let* result =
        Bos.OS.File.with_ic filename
          (fun chan () ->
            let lexbuf = Lexing.from_channel chan in
            lexbuf.lex_curr_p <-
              { lexbuf.lex_curr_p with pos_fname = Fpath.to_string filename };
            parse_with_error Parser.script lexbuf )
          ()
      in
      result

    let from_string contents =
      parse_with_error Parser.script (Lexing.from_string contents)
  end

  module Expr = struct
    let from_file filename =
      let open Result.Syntax in
      let* result =
        Bos.OS.File.with_ic filename
          (fun chan () ->
            let lexbuf = Lexing.from_channel chan in
            lexbuf.lex_curr_p <-
              { lexbuf.lex_curr_p with pos_fname = Fpath.to_string filename };
            parse_with_error Parser.expression lexbuf )
          ()
      in
      result

    let from_string contents =
      parse_with_error Parser.expression (Lexing.from_string contents)
  end
end

module Smtlib = struct
  let from_file filename =
    try
      let _, st = Smtlib.parse_all (`File (Fpath.to_string filename)) in
      Ok (Lazy.force st)
    with
    | Dolmen.Std.Loc.Syntax_error (loc, `Regular msg) ->
      Fmt.error_msg "%a: syntax error: %t" Dolmen.Std.Loc.print_compact loc msg
    | Dolmen.Std.Loc.Syntax_error (loc, `Advanced (x, _, _, _)) ->
      Fmt.error_msg "%a: syntax error: %s" Dolmen.Std.Loc.print_compact loc x
end

let from_file filename =
  match Fpath.split_ext filename with
  | _, ".smtml" -> Smtml.Script.from_file filename
  | _, ".smt2" -> Smtlib.from_file filename
  | fname, ext -> (
    (* FIXME: I don't like this *)
    match Fpath.to_string fname with
    | "-" -> Smtml.Script.from_file filename
    | _ -> Fmt.failwith "Unsupported script type with extension '%s'" ext )

1	(* SPDX-License-Identifier: MIT *)
2	(* Copyright (C) 2023-2026 formalsec *)
3	(* Written by the Smtml programmers *)
4
5	module Smtml = struct
6	open Lexer
7	open Lexing
8
9	let pp_pos fmt lexbuf =
10	let pos = lexbuf.lex_curr_p in	×
11	Fmt.pf fmt "%s:%d:%d" pos.pos_fname pos.pos_lnum
12	(pos.pos_cnum - pos.pos_bol + 1)
13
14	let parse_with_error parser lexbuf =
15	try Ok (parser Lexer.token lexbuf) with	9✔
NEW 16	\| SyntaxError msg -> Fmt.error_msg "%a: %s" pp_pos lexbuf msg	×
NEW 17	\| Parser.Error -> Fmt.error_msg "%a: syntax error" pp_pos lexbuf	×
18
19	module Script = struct
20	let from_file filename =
21	let open Result.Syntax in	7✔
22	let* result =
23	Bos.OS.File.with_ic filename	7✔
24	(fun chan () ->
25	let lexbuf = Lexing.from_channel chan in	7✔
26	lexbuf.lex_curr_p <-	7✔
27	{ lexbuf.lex_curr_p with pos_fname = Fpath.to_string filename };	7✔
28	parse_with_error Parser.script lexbuf )
29	()
30	in
31	result	7✔
32
33	let from_string contents =
34	parse_with_error Parser.script (Lexing.from_string contents)	1✔
35	end
36
37	module Expr = struct
38	let from_file filename =
NEW 39	let open Result.Syntax in	×
40	let* result =
UNCOV 41	Bos.OS.File.with_ic filename	×
42	(fun chan () ->
43	let lexbuf = Lexing.from_channel chan in	×
44	lexbuf.lex_curr_p <-	×
45	{ lexbuf.lex_curr_p with pos_fname = Fpath.to_string filename };	×
46	parse_with_error Parser.expression lexbuf )
47	()
48	in
NEW 49	result	×
50
51	let from_string contents =
52	parse_with_error Parser.expression (Lexing.from_string contents)	1✔
53	end
54	end
55
56	module Smtlib = struct
57	let from_file filename =
58	try	26✔
59	let _, st = Smtlib.parse_all (`File (Fpath.to_string filename)) in	26✔
60	Ok (Lazy.force st)	26✔
61	with
62	\| Dolmen.Std.Loc.Syntax_error (loc, `Regular msg) ->	×
63	Fmt.error_msg "%a: syntax error: %t" Dolmen.Std.Loc.print_compact loc msg
UNCOV 64	\| Dolmen.Std.Loc.Syntax_error (loc, `Advanced (x, _, _, _)) ->	×
65	Fmt.error_msg "%a: syntax error: %s" Dolmen.Std.Loc.print_compact loc x
66	end
67
68	let from_file filename =
69	match Fpath.split_ext filename with	33✔
70	\| _, ".smtml" -> Smtml.Script.from_file filename	6✔
71	\| _, ".smt2" -> Smtlib.from_file filename	26✔
72	\| fname, ext -> (	1✔
73	(* FIXME: I don't like this *)
74	match Fpath.to_string fname with
75	\| "-" -> Smtml.Script.from_file filename	1✔
76	\| _ -> Fmt.failwith "Unsupported script type with extension '%s'" ext )	×

formalsec / smtml / 555

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous