[asl-carpenter] Bug fix on random generation

Random generation constructed the list of needed tests non-lazily, which
is now fixed.

asllib/carpenter/RandomAST.ml

@@ -8,6 +8,7 @@ open AST
 open ASTUtils
 open QCheck2.Gen
 
+let _dbg = false
 let annot desc = ASTUtils.add_dummy_pos desc
 
 type 'a gen = 'a QCheck2.Gen.t
@@ -22,6 +23,7 @@ let protected_oneof = function [] -> None | li -> Some (oneof li)
 let protected_filter_oneofl li = filter li |> protected_oneofl
 let protected_filter_oneof li = filter li |> protected_oneof
 let names = string_size ~gen:(char_range 'a' 'z') (1 -- 20)
+let pay n = if n <= 0 then 0 else n - 1
 
 let rec ensure_satisfies p t =
   let* v = t in
@@ -131,7 +133,9 @@ module Untyped (C : Config.S) = struct
       ]
       |> filter_oneof
     in
-    Nat.list_sized slice
+    fun n ->
+      if n >= 1 then Nat.list_sized slice (n - 1)
+      else slice_single n >|= fun x -> [ x ]
 
   let expr : expr sgen =
     let e_literal = literal >|== fun l -> E_Literal l |> annot in
@@ -156,10 +160,11 @@ module Untyped (C : Config.S) = struct
       E_Slice (e, slices) |> annot
     in
     fix @@ fun expr n ->
+    let n = pay n in
     [
       (if C.Syntax.e_literal then e_literal else None);
       (if C.Syntax.e_var then Some e_var else None);
-      (if C.Syntax.e_unop then e_unop expr n else None);
+      (if C.Syntax.e_unop && n >= 0 then e_unop expr n else None);
       (if C.Syntax.e_binop && n >= 2 then e_binop expr n else None);
       (if C.Syntax.e_tuple && n >= 2 then Some (e_tuple expr n) else None);
       (if C.Syntax.e_cond && n >= 3 then Some (e_cond expr n) else None);
@@ -188,7 +193,11 @@ module Untyped (C : Config.S) = struct
     |> filter
     |> function
     | [] -> None
-    | li -> Some (fun n -> List.map (fun sgen -> sgen n) li |> oneof)
+    | li ->
+        Some
+          (fun n ->
+            let n = pay n in
+            List.map (fun sgen -> sgen n) li |> oneof)
 
   let ty : ty sgen =
     let field ty n = pair names (ty n) in
@@ -214,6 +223,7 @@ module Untyped (C : Config.S) = struct
       T_Bits (width, bitfields) |> annot
     in
     fix @@ fun ty n ->
+    let n = pay n in
     [
       ty_basic;
       (if C.Syntax.t_int && n >= 1 then t_int n else None);
@@ -241,6 +251,7 @@ module Untyped (C : Config.S) = struct
       LDI_Tuple li
     in
     fix @@ fun ldi n ->
+    let n = pay n in
     [
       (if C.Syntax.ldi_var then Some ldi_var else None);
       (if C.Syntax.ldi_discard then Some ldi_ignore else None);
@@ -274,6 +285,7 @@ module Untyped (C : Config.S) = struct
       LE_SetArray (le, e) |> annot
     in
     fix @@ fun lexpr n ->
+    let n = pay n in
     [
       (if C.Syntax.le_discard then Some le_ignore else None);
       (if C.Syntax.le_var then Some le_var else None);
@@ -311,6 +323,7 @@ module Untyped (C : Config.S) = struct
       S_Assign (le, e, V1) |> annot
     in
     fix @@ fun stmt n ->
+    let n = pay n in
     [
       (if C.Syntax.s_assert then Some (s_assert n) else None);
       (if C.Syntax.s_cond && n >= 2 then Some (s_cond stmt n) else None);
@@ -365,13 +378,17 @@ module Typed (C : Config.S) = struct
     List.fold_left (add_with f) init li
 
   let rec minimal_direct_fuel_ty env ty =
+    let () =
+      if _dbg && true then
+        Format.eprintf "Getting minimal_direct_fuel of %a@." PP.pp_ty ty
+    in
     match (Types.make_anonymous env ty).desc with
     | T_Int _ | T_Bool | T_Bits _ | T_Enum _ | T_Real | T_String -> 1
     | T_Named _ -> assert false
     | T_Array _ -> 1000000000
-    | T_Tuple li -> list_sum ~init:1 (minimal_direct_fuel_ty env) li
+    | T_Tuple li -> list_sum ~init:2 (minimal_direct_fuel_ty env) li
     | T_Record fields | T_Exception fields ->
-        list_sum ~init:1 (fun (_, ty) -> minimal_direct_fuel_ty env ty) fields
+        list_sum ~init:2 (fun (_, ty) -> minimal_direct_fuel_ty env ty) fields
 
   let literal ty : literal gen =
     match ty.desc with
@@ -393,6 +410,7 @@ module Typed (C : Config.S) = struct
     T_Bits (E_Literal (L_Int (Z.of_int width)) |> annot, []) |> annot
 
   let slice expr env n : slice gen =
+    let n = pay n in
     let* n1, n2 = Nat.split2 n in
     let int n = expr (env, integer, n) in
     [
@@ -447,7 +465,8 @@ module Typed (C : Config.S) = struct
           Some
             (let+ e' = expr (env, T_Int UnConstrained |> annot, n) in
              E_CTC (e', ty) |> annot)
-      | T_Named _ -> Some (expr (env, ty_anon, n - 1))
+      | T_Named _ when Types.is_singular env ty_anon ->
+          Some (expr (env, ty_anon, n - 1))
       | _ -> None
     in
     let e_call expr env ty n =
@@ -589,7 +608,10 @@ module Typed (C : Config.S) = struct
     in
     let expr' =
       fix @@ fun expr (env, ty, n) ->
-      let n = if n > 0 then n - 1 else 0 in
+      let () =
+        if _dbg then Printf.eprintf "Generating an expr of size %d\n%!" n
+      in
+      let n = pay n in
       let ty_anon = Types.make_anonymous env ty in
       [
         (if C.Syntax.e_literal && can_construct_literal env ty_anon then
@@ -626,15 +648,19 @@ module Typed (C : Config.S) = struct
         (if C.Syntax.e_getfield && n >= 1 then e_get_field expr env ty n
          else None);
       ]
-      |> List.filter_map Fun.id
+      |> filter
       |> function
       | [] ->
-          if false then
+          if _dbg || false then
             Format.eprintf "@[<2>Cannot construct with fuel %d type@ %a@]@." n
               PP.pp_ty ty;
           expr (env, ty, minimal_direct_fuel_ty env ty)
-      | li -> oneof li
+      | li ->
+          let res = oneof li in
+          let () = if _dbg then Printf.eprintf "Generated expr.\n%!" in
+          res
     in
+
     fun env ty n -> expr' (env, ty, n)
 
   let slices = slices (fun (env, ty, n) -> expr env ty n)
@@ -716,6 +742,8 @@ module Typed (C : Config.S) = struct
     and t_array = None (* TODO *) in
     let ty' =
       fix @@ fun ty (is_decl, env, max, n) ->
+      let () = if _dbg then Printf.eprintf "Generating ty of size %d\n%!" n in
+      let n = pay n in
       [
         (if C.Syntax.t_bool then Some t_bool else None);
         (if C.Syntax.t_int then Some (t_integer env max n) else None);
@@ -735,6 +763,11 @@ module Typed (C : Config.S) = struct
         (if C.Syntax.t_named then t_named env max else None);
       ]
       |> filter_oneof
+      |>
+      if _dbg then (fun res ->
+        Printf.eprintf "type generated.\n%!";
+        res)
+      else Fun.id
     in
     fun is_decl env ?max n -> ty' (is_decl, env, max, n)
 
@@ -804,7 +837,10 @@ module Typed (C : Config.S) = struct
         | _ -> None
       in
       fix @@ fun lexpr (env, ty, n) ->
-      let n = if n > 0 then n - 1 else n in
+      let () =
+        if _dbg then Printf.eprintf "Generating lexpr of size %d\n%!" n
+      in
+      let n = pay n in
       let ty_anon = Types.make_anonymous env ty in
       [
         (if C.Syntax.le_discard then Some le_discard else None);
@@ -877,7 +913,10 @@ module Typed (C : Config.S) = struct
     in
     let stmt' =
       fix @@ fun stmt (env, n) ->
-      let n = if n > 0 then n - 1 else 0 in
+      let () =
+        if _dbg then Printf.eprintf "Generating a stmt of size %d\n%!" n
+      in
+      let n = pay n in
       [
         (if C.Syntax.s_decl then Some (s_decl env n) else None);
         (if C.Syntax.s_assert then Some (s_assert env n) else None);
@@ -939,6 +978,10 @@ module Typed (C : Config.S) = struct
       (D_Func func_sig |> annot, StaticEnv.add_subprogram name func_sig env)
     in
     fun env n ->
+      let () =
+        if _dbg then Printf.eprintf "Generating a decl of size %d\n%!" n
+      in
+      let n = pay n in
       [ type_decl env n ]
       |> (if n >= 2 then List.cons (global_decl env n) else Fun.id)
       |> (if n >= 3 then List.cons (func env n) else Fun.id)
@@ -951,6 +994,7 @@ module Typed (C : Config.S) = struct
     and subprogram_type = ST_Procedure
     and name = "main" in
     fun env n ->
+      let n = pay n in
       let env' =
         StaticEnv.
           { global = env.global; local = empty_local_return_type return_type }
@@ -964,6 +1008,9 @@ module Typed (C : Config.S) = struct
   let ast : AST.t sgen = function
     | 0 -> pure []
     | n ->
+        let () =
+          if _dbg then Printf.eprintf "Generating ast of size %d\n%!" n
+        in
         let* n_main = 1 -- ((n + 4) / 5) in
         let n = n - n_main in
         let* n_decl = if n = 0 then pure 0 else 1 -- ((n + 4) / 5) in
@@ -978,5 +1025,6 @@ module Typed (C : Config.S) = struct
             sizes
         in
         let+ main = main env n_main in
+        let () = if _dbg then Printf.eprintf "Generated ast.\n%!" in
         List.rev (main :: decls)
 end

asllib/carpenter/main.ml

@@ -84,54 +84,50 @@ let filter_instr = function
         res
   | None -> Fun.const true
 
-let generate_random (config, instr, o, progress) n =
-  let module Generator = RandomAST.Typed ((val config : Config.S)) in
-  let filter = filter_instr instr in
-  QCheck2.Gen.(generate ~n (sized Generator.ast))
-  |> List.filter filter
-  |> List.iteri (print_one progress o n);
-  hide_progress progress ()
+let random_asts (small : bool) config : AST.t Seq.t =
+  let asts =
+    let module Generator = RandomAST.Typed ((val config : Config.S)) in
+    let open QCheck2.Gen in
+    let sizes = if small then small_nat else nat in
+    sized_size sizes Generator.ast
+  in
+  let gen_one =
+    let rand = Random.State.make_self_init () in
+    fun () -> QCheck2.Gen.generate1 ~rand asts
+  in
+  Seq.forever gen_one
 
 let smallests_asts config : AST.t Seq.t =
   let module IFSeq = Feat.Enum.IFSeq in
   let module Enums = ASTEnums.Make ((val config : Config.S)) in
   let asts_of_size n = IFSeq.to_seq (Enums.asts n) Seq.empty in
   Seq.flat_map asts_of_size (Seq.ints 0)
 
-let generate_enum (config, instr, o, progress) n =
-  smallests_asts config
+let generalized_generate asts (config, instr, o, progress) n =
+  asts config
   |> Seq.filter (filter_instr instr)
   |> Seq.take n
   |> Seq.iteri (print_one progress o n);
   hide_progress progress ()
 
+let generate_enum c = generalized_generate smallests_asts c
+let generate_random small c = generalized_generate (random_asts small) c
+
 let generalized_fuzz (asts : 'a Seq.t) (on_ast : 'a -> AST.t option) progress o
     n =
   let do_one (i, counter) ast =
+    print_progress progress i n;
     match on_ast ast with
-    | None ->
-        print_progress progress i n;
-        (succ i, counter)
+    | None -> (succ i, counter)
     | Some ast ->
         Logs.info (fun m -> m "Discrepancy found.");
         let filename = filename o counter in
         print_ast filename ast;
-        print_progress progress i n;
         (succ i, succ counter)
   in
   let _i = asts |> Seq.take n |> Seq.fold_left do_one (0, 0) in
   hide_progress progress ()
 
-let random_asts config small : AST.t Seq.t =
-  let asts =
-    let module Generator = RandomAST.Typed ((val config : Config.S)) in
-    let open QCheck2.Gen in
-    let sizes = if small then small_nat else nat in
-    sized_size sizes Generator.ast
-  in
-  let gen_one () = QCheck2.Gen.generate1 asts in
-  Seq.forever gen_one
-
 let random_trees config small =
   let asts =
     let module Generator = RandomAST.Typed ((val config : Config.S)) in
@@ -203,7 +199,7 @@ let rec on_ast_tree on_ast ast_tree =
 
 let fuzz small (config, instr, type_only, target, o, progress) n =
   with_on_ast target @@ fun on_ast ->
-  generalized_fuzz (random_asts config small) (on_ast instr type_only) progress
+  generalized_fuzz (random_asts small config) (on_ast instr type_only) progress
     o n
 
 let bet (config, instr, type_only, target, o, progress) n =
@@ -353,7 +349,9 @@ module Cmd = struct
     Term.(
       const make $ setup_logs $ setup_random $ progress $ config $ instr $ o)
 
-  let generate_random = Term.(const generate_random $ common_options $ n)
+  let generate_random =
+    Term.(const generate_random $ small $ common_options $ n)
+
   let generate_enum = Term.(const generate_enum $ common_options $ n)
 
   let fuzzing_options =

asllib/error.ml

@@ -212,3 +212,8 @@ let pp_error =
 
 let error_to_string = Format.asprintf "%a" pp_error
 let eprintln = Format.eprintf "@[<2>%a@]@." pp_error
+
+let () =
+  Printexc.register_printer @@ function
+  | ASLException e -> Some (error_to_string e)
+  | _ -> None

asllib/types.ml

@@ -233,7 +233,7 @@ module Domain = struct
       in
       try StaticInterpreter.static_eval env e
       with
-      | Error.ASLException { desc = Error.UndefinedIdentifier _; _ } ->
+      | Error.ASLException _ ->
         raise_notrace StaticEvaluationTop
     in
     match v with
@@ -327,7 +327,6 @@ module Domain = struct
             Error.fatal_from e (Error.UndefinedIdentifier x)))
     | E_Unop (NEG, e') ->
         of_expr env (E_Binop (MINUS, !$0, e') |> add_pos_from e)
-    | E_Unop _ -> Error.(fatal_from e (Error.UnsupportedExpr e))
     | E_Binop (((PLUS | MINUS | MUL) as op), e1, e2) ->
         let is1 =
           match of_expr env e1 with D_Int is -> is | _ -> assert false
@@ -366,7 +365,7 @@ module Domain = struct
         try
           match of_expr env width with
           | D_Int is -> D_Bits is
-          | _ -> Error.(fatal_unknown_pos (UnsupportedExpr width))
+          | _ -> raise StaticEvaluationTop
         with StaticEvaluationTop ->
           D_Bits (FromSyntax [ Constraint_Exact width ]))
     | T_Array _ | T_Exception _ | T_Record _ | T_Tuple _ ->