concurrency printing bug

[redianthus]

The following code:

let pp_smtml fmt (es : t list) : unit =
  let def_num_printer = Num.get_default_printer () in
  Num.set_default_printer `Hexadecimal;
  Bitvector.set_default_printer `WithType;
  let pp_symbols fmt syms =
    Fmt.list ~sep:Fmt.cut
      (fun fmt sym ->
        let t = Symbol.type_of sym in
        Fmt.pf fmt "(let-const %a %a)" Symbol.pp sym Ty.pp t )
      fmt syms
  in
  let pp_asserts fmt es =
    Fmt.list ~sep:Fmt.cut
      (fun fmt e -> Fmt.pf fmt "(assert @[<h 2>%a@])" pp e)
      fmt es
  in
  let syms = get_symbols es in
  if List.length syms > 0 then Fmt.pf fmt "@[<v>%a@]@\n" pp_symbols syms;
  if List.length es > 0 then Fmt.pf fmt "@[<v>%a@]@\n" pp_asserts es;
  Fmt.string fmt "(check-sat)";
  Num.set_default_printer def_num_printer;
  Bitvector.set_default_printer `Pretty

Can lead to invalid strings being sent to Z3 when used concurrently.
For instance, if one domain starts executing, then a second one starts, but the first one ends and reset the printer, then, the second one will print things Z3 does not understand.
You can see a trace in Owi (have a look at the BITVECTOR lines, they should all be 0 but one of them is wrong because of this bug):

$ owi ...
owi: [INFO] typechecking ...
owi: [INFO] linking      ...
owi: [INFO] interpreting ...
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : i32.const 1024 (executed 0 times)
owi: [INFO] stack         : [ 1024 ]
owi: [INFO] running instr : i32.const 0 (executed 0 times)
owi: [INFO] stack         : [ 0 ; 1024 ]
owi: [INFO] running instr : i32.const 13 (executed 0 times)
owi: [INFO] stack         : [ 13 ; 0 ; 1024 ]
owi: [INFO] running instr : memory.init 0 (executed 0 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : data.drop 0 (executed 0 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : call 11 (executed 0 times)
owi: [INFO] calling func  : func anonymous
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : i32.const 0 (executed 0 times)
owi: [INFO] stack         : [ 0 ]
owi: [INFO] running instr : i32.const 0 (executed 0 times)
owi: [INFO] stack         : [ 0 ; 0 ]
owi: [INFO] running instr : call 10 (executed 0 times)
owi: [INFO] calling func  : func anonymous
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : call 9 (executed 0 times)
owi: [INFO] calling func  : func anonymous
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : i32.const 1028 (executed 0 times)
owi: [INFO] stack         : [ 1028 ]
owi: [INFO] running instr : call 1 (executed 0 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : i32.const 1026 (executed 0 times)
owi: [INFO] stack         : [ 1026 ]
owi: [INFO] running instr : call 8 (executed 0 times)
owi: [INFO] calling func  : func anonymous
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : local.get 0 (executed 0 times)
owi: [INFO] stack         : [ 1026 ]
owi: [INFO] running instr : call 1 (executed 0 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : call 3 (executed 0 times)
owi: [INFO] stack         : [ symbol_0 ]
owi: [INFO] running instr : local.set 0 (executed 0 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : call 2 (executed 0 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : local.get 0 (executed 0 times)
owi: [INFO] stack         : [ symbol_0 ]
owi: [INFO] running instr : local.set 0 (executed 0 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : i32.const 1024 (executed 0 times)
owi: [INFO] stack         : [ 1024 ]
owi: [INFO] running instr : call 8 (executed 0 times)
owi: [INFO] calling func  : func anonymous
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : local.get 0 (executed 1 times)
owi: [INFO] stack         : [ 1024 ]
owi: [INFO] running instr : call 1 (executed 1 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : call 3 (executed 1 times)
owi: [INFO] stack         : [ symbol_1 ]
owi: [INFO] running instr : local.set 0 (executed 1 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : call 2 (executed 1 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : local.get 0 (executed 1 times)
owi: [INFO] stack         : [ symbol_1 ]
owi: [INFO] running instr : local.set 1 (executed 0 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : call 2 (executed 0 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : block (executed 0 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : local.get 0 (executed 0 times)
owi: [INFO] stack         : [ symbol_0 ]
owi: [INFO] running instr : i32.const 0 (executed 0 times)
owi: [INFO] stack         : [ 0 ; symbol_0 ]
owi: [INFO] running instr : local.get 1 (executed 0 times)
owi: [INFO] stack         : [ symbol_1 ; 0 ; symbol_0 ]
owi: [INFO] running instr : i32.sub (executed 0 times)
owi: [INFO] stack         : [ (i32.sub 0 symbol_1) ; symbol_0 ]
owi: [INFO] running instr : i32.ne (executed 0 times)
owi: [INFO] stack         : [ (i32.of_bool
                               (bool.ne symbol_0 (i32.sub 0 symbol_1))) ]
owi: [INFO] running instr : br_if 0 (executed 0 times)
owi: [ERROR] saucisse
owi: [ERROR] saucisse
owi: [ERROR] BITVECTOR: 0
owi: [ERROR] BITVECTOR: 0
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : i32.const 0 (executed 0 times)
owi: [DEBUG] path condition smt query:
              (let-const symbol_1 i32)
              (let-const symbol_0 i32)
              (assert (bool.eq symbol_0 (i32.sub (i32 0) symbol_1)))
              (check-sat)
owi: [INFO] stack         : [ 0 ]
owi: [INFO] running instr : call 0 (executed 0 times)
owi: [DEBUG] path condition smt query:
              (let-const symbol_1 i32)
              (let-const symbol_0 i32)
              (assert (bool.eq symbol_0 (i32.sub (i32 0) symbol_1)))
              (check-sat)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : i32.const 0 (executed 0 times)
owi: [ERROR] saucisse
owi: [DEBUG] path condition smt query:
              (let-const symbol_1 i32)
              (let-const symbol_0 i32)
              (assert (bool.ne symbol_0 (i32.sub (i32 0) symbol_1)))
              (check-sat)
owi: [ERROR] BITVECTOR: (i32 0)
owi: [INFO] stack         : [ 0 ]
owi: [INFO] running instr : drop (executed 0 times)
owi: [DEBUG] path condition smt query:
              (let-const symbol_1 i32)
              (let-const symbol_0 i32)
              (assert (bool.ne symbol_0 (i32.sub (i32 0) symbol_1)))
              (check-sat)
owi: [ERROR] encode_expr: (bool.eq symbol_0 (i32.sub 0 symbol_1))
owi: [ERROR] saucisse
owi: [ERROR] a worker ended with exception Z3.Error("parser error"), backtrace is:
             Raised by primitive operation at Z3.BitVector.mk_numeral in file "../src/api/ml/z3.ml", line 1256, characters 30-74
Called from Smtml__Mappings.Make.Make_.Encoder.encode_expr in file "src/smtml/mappings.ml", line 664, characters 29-36
Called from Smtml__Mappings.Make.Make_.Encoder.encode_expr in file "src/smtml/mappings.ml", line 725, characters 24-42
Called from Smtml__Mappings.Make.Make_.Encoder.encode_expr in file "src/smtml/mappings.ml", line 735, characters 24-42
Called from Smtml__Mappings.Make.Make_.Encoder.wrapper in file "src/smtml/mappings.ml", line 771, characters 12-31
Re-raised at Smtml__Mappings.Make.Make_.Encoder.wrapper in file "src/smtml/mappings.ml", line 773, characters 7-14
Called from Smtml__Mappings.Make.Make_.Encoder.encode_exprs.(fun) in file "src/smtml/mappings.ml", line 779, characters 27-40
Called from Stdlib__List.fold_left in file "list.ml", line 125, characters 24-34
Called from Smtml__Mappings.Make.Make_.Encoder.encode_exprs in file "src/smtml/mappings.ml", lines 777-781, characters 10-24
Called from Smtml__Mappings.Make.Make_.Solver.check in file "src/smtml/mappings.ml", line 941, characters 40-76
Called from Smtml__Utils.run_and_time_call in file "src/smtml/utils.ml", line 7, characters 15-19
Called from Smtml__Solver.Base.check_set in file "src/smtml/solver.ml" (inlined), line 49, characters 28-63
Called from Smtml__Solver.Base.get_sat_model in file "src/smtml/solver.ml", line 62, characters 10-25
Called from Owi__Solver.model_of_path_condition.(fun) in file "src/symbolic/solver.ml", line 90, characters 16-41
Called from Stdlib__List.map in file "list.ml", line 85, characters 15-19
Called from Owi__Solver.model_of_path_condition in file "src/symbolic/solver.ml", lines 88-98, characters 6-22
Called from Owi__Symbolic_choice.bug.(fun) in file "src/symbolic/symbolic_choice.ml", line 215, characters 10-56
Called from Owi__Symbolic_choice.bug in file "src/symbolic/symbolic_choice.ml", lines 213-217, characters 4-74
Called from Symex__Monad.State.bind.(fun) in file "src/monad.ml", line 41, characters 21-30
Called from Symex__Monad.State.bind.(fun) in file "src/monad.ml", line 41, characters 21-30
Called from Symex__Monad.State.bind.(fun) in file "src/monad.ml", line 41, characters 21-30
Called from Symex__Monad.Schedulable.bind.(fun) in file "src/monad.ml", line 16, characters 56-65
Called from Owi__Symbolic_driver.run.run_worker.(fun) in file "src/symbolic/symbolic_driver.ml", line 122, characters 50-56
Called from Stdlib__Fun.protect in file "fun.ml", line 34, characters 8-15
Re-raised at Stdlib__Fun.protect in file "fun.ml", line 39, characters 6-52
Called from Synchronizer.work_while in file "src/synchronizer.ml", lines 72-77, characters 4-31
Called from Owi__Symbolic_driver.run.run_worker.(fun) in file "src/symbolic/symbolic_driver.ml", lines 121-123, characters 12-19

owi: [INFO] one domain exited with the following Z3 exception: parser error
owi: [INFO] Completed paths: 1
All OK!