Fix a bug in the evaluation of cvtops for bitvectors

dune-project

@@ -70,6 +70,7 @@
   (ocaml
    (>= "4.14.0"))
   ocaml_intrinsics
+  ppx_deriving
   (prelude
    (>= "0.5"))
   (scfg

smtml.opam

@@ -32,6 +32,7 @@ depends: [
   "menhir" {build & >= "20220210"}
   "ocaml" {>= "4.14.0"}
   "ocaml_intrinsics"
+  "ppx_deriving"
   "prelude" {>= "0.5"}
   "scfg" {>= "0.5"}
   "mtime" {>= "2.0.0"}

src/bin/cmd_run.ml

@@ -36,39 +36,48 @@ let run (s : Settings.Run.t) =
   let total_t = ref 0. in
   let exception_log = ref [] in
   let exception_count = ref 0 in
+
   let run_file state file =
     Log.debug (fun k -> k "File %a..." Fpath.pp file);
     incr total_tests;
     let start_t = Unix.gettimeofday () in
-    Fun.protect ~finally:(fun () ->
-      if s.print_statistics then (
-        let exec_t = Unix.gettimeofday () -. start_t in
-        total_t := !total_t +. exec_t;
-        Log.app (fun m -> m "Run %a in %.06f" Fpath.pp file exec_t) ) )
-    @@ fun () ->
     let ast =
-      try Ok (Compile.until_rewrite file)
-      with Parse.Syntax_error err -> Error (`Parsing_error (file, err))
+      try Ok (Compile.until_rewrite file) with
+      | Parse.Syntax_error err -> Error (`Parsing_error (file, err))
+      | Smtml.Eval.Eval_error err -> Error (`Eval_error err)
+    in
+    let state =
+      match ast with
+      | Ok _ when s.dry -> state
+      | Ok ast ->
+        Some (Interpret.start ?state ast ~no_strict_status:s.no_strict_status)
+      | Error (`Parsing_error ((fpath, err_msg) as err)) ->
+        Log.err (fun k -> k "%a: %s" Fpath.pp fpath err_msg);
+        incr exception_count;
+        exception_log := err :: !exception_log;
+        state
+      | Error (`Eval_error kind) ->
+        Log.err (fun k ->
+          k "@[<h>%a: Eval_error: %a@]" Fpath.pp file Smtml.Eval.pp_error_kind
+            kind );
+        incr exception_count;
+        state
     in
-    match ast with
-    | Ok _ when s.dry -> state
-    | Ok ast ->
-      Some (Interpret.start ?state ast ~no_strict_status:s.no_strict_status)
-    | Error (`Parsing_error ((fpath, err_msg) as err)) ->
-      Log.err (fun k -> k "%a: %s" Fpath.pp fpath err_msg);
-      incr exception_count;
-      exception_log := err :: !exception_log;
-      state
+    if s.print_statistics then (
+      let exec_t = Unix.gettimeofday () -. start_t in
+      total_t := !total_t +. exec_t;
+      Log.app (fun m -> m "Run %a in %.06f" Fpath.pp file exec_t) );
+    state
   in
+
   let run_dir prev_state d =
-    let result =
-      Bos.OS.Dir.fold_contents ~traverse:`Any
-        (fun path state ->
-          if Fpath.has_ext ".smt2" path then run_file state path else state )
-        prev_state d
-    in
-    match result with Error (`Msg e) -> failwith e | Ok state -> state
+    Bos.OS.Dir.fold_contents ~traverse:`Any
+      (fun path state ->
+        if Fpath.has_ext ".smt2" path then run_file state path else state )
+      prev_state d
+    |> Result.get_ok
   in
+
   let run_path prev_state path =
     match Fpath.to_string path with
     | "-" -> run_file prev_state path
@@ -84,6 +93,7 @@ let run (s : Settings.Run.t) =
         Log.err (fun k -> k "%s" err);
         prev_state )
   in
+
   let _ =
     match s.from_file with
     | None -> List.fold_left run_path None s.filenames
@@ -94,6 +104,7 @@ let run (s : Settings.Run.t) =
         None
       | Ok files -> List.fold_left run_file None files )
   in
+
   if s.print_statistics then Log.app (fun k -> k "total time: %.06f" !total_t);
   let write_exception_log =
     let open Smtml_prelude.Result in

src/smtml/dune

@@ -111,7 +111,7 @@
   (backend bisect_ppx --exclusions src/smtml/bisect.exclude)
   (deps bisect.exclude))
  (preprocess
-  (pps ppx_deriving.std)))
+  (pps ppx_deriving.std ppx_deriving.show)))
 
 (rule
  (targets

src/smtml/eval.ml

@@ -15,14 +15,7 @@ type op_type =
   | `Cvtop of Ty.Cvtop.t
   | `Naryop of Ty.Naryop.t
   ]
-
-let pp_op_type fmt = function
-  | `Unop op -> Fmt.pf fmt "unop '%a'" Ty.Unop.pp op
-  | `Binop op -> Fmt.pf fmt "binop '%a'" Ty.Binop.pp op
-  | `Relop op -> Fmt.pf fmt "relop '%a'" Ty.Relop.pp op
-  | `Triop op -> Fmt.pf fmt "triop '%a'" Ty.Triop.pp op
-  | `Cvtop op -> Fmt.pf fmt "cvtop '%a'" Ty.Cvtop.pp op
-  | `Naryop op -> Fmt.pf fmt "naryop '%a'" Ty.Naryop.pp op
+[@@deriving show]
 
 type type_error_info =
   { index : int
@@ -31,6 +24,7 @@ type type_error_info =
   ; op : op_type
   ; msg : string
   }
+[@@deriving show]
 
 type error_kind =
   [ `Divide_by_zero
@@ -42,6 +36,7 @@ type error_kind =
   | `Unsupported_theory of Ty.t
   | `Type_error of type_error_info
   ]
+[@@deriving show]
 
 exception Eval_error of error_kind
 
@@ -535,6 +530,17 @@ module Bitv = struct
     | GeU -> Bitvector.ge_u bv1 bv2
     | Eq -> Bitvector.equal bv1 bv2
     | Ne -> not @@ Bitvector.equal bv1 bv2
+
+  let cvtop op bv =
+    let bv = of_bitv 1 (`Cvtop op) bv in
+    to_bitv
+    @@
+    match op with
+    | Ty.Cvtop.Sign_extend m -> Bitvector.sign_extend m bv
+    | Ty.Cvtop.Zero_extend m -> Bitvector.zero_extend m bv
+    | _ ->
+      eval_error
+        (`Unsupported_operator (`Cvtop op, Ty_bitv (Bitvector.numbits bv)))
 end
 
 module F32 = struct
@@ -988,6 +994,8 @@ let cvtop = function
   | Ty_str -> Str.cvtop
   | Ty_bitv 32 -> I32CvtOp.cvtop
   | Ty_bitv 64 -> I64CvtOp.cvtop
+  (* Remaining fall into arbitrary-width bv cvtop operations *)
+  | Ty_bitv _m -> Bitv.cvtop
   | Ty_fp 32 -> F32CvtOp.cvtop
   | Ty_fp 64 -> F64CvtOp.cvtop
   | ty -> eval_error (`Unsupported_theory ty)

src/smtml/eval.mli

@@ -42,6 +42,8 @@ type error_kind =
   | `Type_error of type_error_info
   ]
 
+val pp_error_kind : error_kind Fmt.t
+
 (** Exception raised when an error occurs during concrete evaluation. *)
 exception Eval_error of error_kind