Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM

Nikolaus Huber ^{(1, 3)}, Naomi Spargo ^{(2, 3)}, Nicolas Osborne ⁽³⁾, Samuel Hym ⁽³⁾,
Jan Midtgaard ⁽³⁾

⁽¹⁾ Uppsala University, Uppsala, Sweden
⁽²⁾ Galois Inc, Arlington, VA, USA
⁽³⁾ Tarides, Paris, France

• Caml (ML dialect) + OO
• Functional core
• Many imperative features
• References
• Mutable arrays
• I/O
• Exceptions

Infer

Astrée

...

Gospel

• Behavioural specification language
• Type invariants, function pre/post conditions, mutability, exceptions, ...
• Tool agnostic
• Cameleer
• Why3gospel
• ORTAC
• ...

ORTAC

• (O)Caml (R)un(T)ime (A)ssertion (C)hecker
• Module I/F + GOSPEL => code for testing
• Plugins
• Wrapper
• Monolith
• QCheck-STM
• ...

QCheck-STM

• QCheck + state
• black-box, model-based state-machine testing

Stack (Excerpt)

		type 'a t
		
		exception Empty
		
		val create : unit -> 'a t
		val push : 'a -> 'a t -> unit
		val pop : 'a t -> 'a
		val is_empty : 'a t -> bool
	

		type 'a t
		(*@ mutable model contents : 'a sequence *)
	

		val create : unit -> 'a t
		(*@ t = create ()
			  ensures t.contents = Sequence.empty *)
	

		val push : 'a -> 'a t -> unit
		(*@ push v t
				modifies t.contents
				ensures t.contents =
					Sequence.cons v (old t.contents) *)
	

		val is_empty : 'a t -> bool
		(*@ b = is_empty t
				ensures b = match Sequence.length t.contents with
				  | 0 -> true
				  | _ -> false *)
	

		val copy : 'a t -> 'a t
		(*@ r = copy t
				ensures r.contents = t.contents *)
	

		val transfer : 'a t -> 'a t -> unit
		(*@ transfer t1 t2
				modifies t1.contents
				modifies t2.contents
				ensures t1.contents = Sequence.empty
				ensures t2.contents =
					(old t1.contents) ++ (old t2.contents) *)
	

Evaluation - Errors/Bugs found

Hashtbl

		val create : ?random:bool -> int -> ('a, 'b) t
		(** [Hashtbl.create n] creates a new empty hash table, with
			initial size [n]. For best results, [n] should be on the
			order of the expected number of elements that will be in
			the table.  The table grows as needed, so [n] is just an
			initial guess. ... *)
	

		type ('a, 'b) t
		(*@ mutable model contents : ('a * 'b) list *)

		val create : ?random:bool -> int -> ('a, 'b) t
		(*@ h = create ?random size
				checks size >= 0
				ensures h.contents = [] *)
	

		Gospel specification violation in function create

		File "hashtbl.mli", line 7, characters 11-20:
			size >= 0
		when executing the following sequence of operations:

		[@@@ocaml.warning "-8"]
		open Hashtbl
		let protect f = try Ok (f ()) with e -> Error e
		let sut0 = create ~random:false 16
		let r = protect (fun () -> create ~random:true (-8))
		assert (match r with
					| Error (Invalid_argument _) -> true
					| _ -> false)
		(* returned Ok () *)
	

Errors found

• Documentation fix
• Hashtbl.create (initial size guess can be negative)
• 2 bugs in Varray library
• 7 bugs in Bitv library
• 3 functions with possible integer overflow
• 2 functions with possible division-by-zero
• 2 functions throwing unexpected exceptions
• ...

Evaluation - API coverage

Future work

• Aliased SUT arguments
• Higher-order functions (map, fold, iter)
• Utilise requires clauses for command generation
• Parallel testing

Thank you for listening!

Questions?

https://github.com/ocaml-gospel/ortac/

This work was partially funded by ANR grant ANR-22-CE48-0013 and Tarides.