formalsec/smtml

A Multi Back-end Front-end for SMT Solvers in OCaml

Smt.ml

Smt.ml is a Multi Back-end Front-end for SMT Solvers in OCaml. The primary objective of Smt.ml is to facilitate the effortless transition between different SMT solvers during program analysis, as certain SMT solvers may prove more efficient at handling specific logics and formulas. Presently, Smt.ml offers support for Z3, Colibri2, and Bitwuzla, and ongoing efforts are directed towards incorporating support for cvc5 and Alt-Ergo.

Installation

OPAM

• Install opam.
• Bootstrap the OCaml compiler:

opam init
opam switch create 5.1.0 5.1.0

• And, then install encoding:

opam install smtml

Build from source

• Install the library dependencies:

git clone https://github.com/formalsec/smtml.git
cd smtml
opam install . --deps-only

• Build and test:

dune build
dune runtest

• Install smtml on your path by running:

dune install

Code Coverage Reports

BISECT_FILE=`pwd`/bisect dune runtest --force --instrument-with bisect_ppx
bisect-ppx-report summary # Shell summary
bisect-ppx-report html    # Detailed Report in _coverage/index.html

Supported Solvers

Solver	Status
Z3	Yes
Colibri2	Yes
Bitwuzla	Yes
cvc5	Ongoing
Alt-Ergo	Planned
Minisat	Planned

About

Project Name

The name Smt.ml is a portmanteau of the terms SMT and OCaml. The .ml extension is a common file extension for OCaml source files. The library itself is named smtml and can be imported into OCaml programs using the following syntax:

open Smtml

Changelog

See CHANGES

Copyright

Smt.ml Copyright (C) 2023-2024 formalsec

This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program.  If not, see <https://www.gnu.org/licenses/>.

smtml's Issues

add `is_available` a boolean to know if we're using the `nop` version or the `default` version

For instance, it would allow to do something like:

let solver =
  if Z3_mappings.is_available then Ok Z3_mappings
  else if Colibri2_mappings.is_available then Ok Colibri2
  else if ...
  else Error (`Msg "no available solver")

It would be useful for instance to try many solvers when the user didn't specified one in Owi - instead of only trying Z3 and to fail if it's not there.

The implementation is quite straightforward (add let is_available = false to the nop file and let is_available = true in all default implementations).

Make the expression type a GADT

Mainly resistant due to operators types. Maybe we could type operators like this?

(* ty.ml *)
type _ t =
  | Ty_int : [ `Ty_int ] t
  | Ty_real : [ `Ty_real ] t
  | Ty_bool : [ `Ty_bool ] t
  | Ty_str : [ `Ty_str ] t
  | Ty_bitv : int -> [ `Ty_bitv ] t
  | Ty_fp : int -> [ `Ty_fp ] t

type _ unop =
  | Abs : [< `Ty_real | `Ty_fp ] unop
  | Ceil : [< `Ty_real | `Ty_fp ] unop
  | Clz : [ `Ty_bitv ] unop
  | Ctz : [ `Ty_bitv ] unop
  | Floor : [< `Ty_real | `Ty_fp ] unop
  | Is_nan : [ `Ty_fp ] unop
  | Len : [ `Ty_str ] unop
  | Neg : [< `Ty_int | `Ty_real | `Ty_bitv | `Ty_fp ] unop
  | Nearest : [< `Ty_real | `Ty_fp ] unop
  | Not : [< `Ty_bitv | `Ty_bool ] unop
  | Sqrt : [< `Ty_real | `Ty_fp ] unop
  | Trim : [ `Ty_str ] unop
  | Trunc : [< `Ty_real | `Ty_fp ] unop

...

Add Model.to_json

Bitwuzla segfaults due to `Obj.magic 0`

Colibri2 mappings

https://github.com/hra687261/encoding/commits/use_colibri2/

Allow Z3 mappings to create contexts without models

During symbolic executions, contexts without models are slightly faster than when this option is enabled. Models are only used for test-suite generation at the end of the analysis, accounting for only a fraction of the executed queries.

Crash in symbolic string operations

// inherit parent's constructor
var code = members.__parent.toString();
var args = code.substring( code.indexOf("(")+1, code.indexOf(")") );
var inner_code = code.substring( code.indexOf("{")+1, code.lastIndexOf("}") );
eval('constructor = function ('+args+') {'+inner_code+'};');
	

Move operators `extract` and `concat` expressions into `bvOp.ml`

Is your feature request related to a problem? Please describe.
Currently, the operators extract and concat are defined as generic expressions in expression.ml. However, these operators are only semantically defined over bit vector values.

Describe the solution you'd like
So, it is more semantically correct that the extract and concat operators are moved into the bvOp.ml module as, respectively, triops and binops.

Describe alternatives you've considered
No alternatives.

Additional context
No additional context.

Add solver `get_statistics` function

Add a get_statistics function that returns a statistics type, ensuring that each entry is correctly typed to allow for easy statistics merging.

Due to OCamlPro/owi#198

Z3 model completion can interfere with `Model` solver parameter

Related to #31. Maybe we could implement an overlay in the solver to fail when attempting to retrieve models with model generation turned off.

Nary operators

Maybe we could have something like this?

type nary = Add | Sub | Mul
type bary = And | Or
type sary = Concat
...

type nop =
  | Int of nary
  | Real of nary
  | Bool of bary
  | Str of sary
  | ...

type expr =
  ...
  | Nary of nop * expr list

Fix display of gigantic floats in `Model.pp`

Model:
    (model
      (symbol_1 f64 (f64 -338460706455329128135018695364373065576360054171204343201037173805357995568625611429596369334345869072216864991017687935090688.000000))
      (symbol_2 i32 (i32 11821))
      (symbol_0 f32 (f32 nan))
      (symbol_3 i64 (i64 0)))

Provide datastructures for hashconsed expressions

Provide data structures like sets and maps for hash consed expressions?

wrong repo

better error message on missing solver

For now, the message is: Z3 not installed

Something like:

The Z3 solver is not installed. You must install it through opam with the command `opam install z3`. You could also try to use another solver (have a look at the documentation of the application you are using). Note that installing the solver with your system package manager is not enough, you must install it through opam.

Would be better, WDYT ? I'm trying to prevent something like OCamlPro/owi#332 to happen again.

Eval_numeric Rotl, Rotl, and Trunc

They are mapped to z3 but not evaluated in eval_numeric

https://github.com/formalsec/encoding/blob/3a6be3b12b79fe9a1adb88f4758b496712b2221c/lib/eval_numeric.ml#L64

and

https://github.com/formalsec/encoding/blob/3a6be3b12b79fe9a1adb88f4758b496712b2221c/lib/eval_numeric.ml#L156

misplaced alert attribute

$ dune b
File "lib/bitwuzla_mappings.ml", line 83, characters 29-34:
83 |     let int = Obj.magic 0 [@@alert not_implemented "Not supported"]
                                  ^^^^^
Error (warning 53 [misplaced-attribute]): the "alert" attribute cannot appear in this context

This is on OCaml 5.2 only (the warning is new or has been updated to handle more cases).

Update README.md with documentation on installing at least one solver

Update documentation with instructions on how to install different
solvers

Incorrect float parsing

Error on 2.

Apply normalization at the constructor level

https://dl.acm.org/doi/10.1145/2393596.2393665
http://www.cs.sun.ac.za/~jaco/PAPERS/vgd12.pdf

Test simplifications

Due to #60

Improve parsing error messages

Undefined references just blow up with Not_found 😢

SMT Arrays

Model linear memory using arrays

Add support for I8 and I16 bitvectors

Current state:

• I8
• I16

Restructure lib directory to organise source files

Is your feature request related to a problem? Please describe.
Although the files in lib are correctly named, it would help having them organised into sub-directories that aggregate related code. This feature would reduce mental effort in locating desired source files.

Describe the solution you'd like
For example, files related with the abstract syntax (e.g., intOp.ml or floatOp.ml) should be place in a directory titled syntax.

Describe alternatives you've considered
Alternatives have yet to be considered.

Additional context
No additional context.

SAT caching

Dune caching makes bitwuzla CI fail?

Improve hc

Improve hc see https://fs.zapashcanon.fr/pdf/ter-report.pdf

Add remaining cases to Expr simplification

Related to OCamlPro/owi#122

Missing simplifications

Some simplifications are missing/incomplete.

Current:
(int.add (int.add $_descending 3) 10)

Should be:
(int.add $_descending 13)

remove dependency on Core

it's heavy!

CI Caching broke `test-colibri2` CI pass

Abstract the underlying expression variant representations

Is your feature request related to a problem? Please describe.
Currently, one must directly use the variant representations from Expressions and Types to build expressions of the abstract syntax. This make expression building an extremely painful process.

Describe the solution you'd like
To solve this, create the following six modules: Integer, Real, Boolean, Strings, FloatingPoint and BitVector that expose mk_ function constructors. The obvious advantage of this feature is the employment of ocamldoc for documention.

Describe alternatives you've considered
No alternatives.

Additional context
No additional context required.

Add `compare` function to module Expr

Integer numeric evaluation

Por exemplo:

antes era:

Program Print
(Val Int -1)

Agora é:

>Program Print
(int.sub 5 6)

Model with incorrect symbol

Introduced in #59

Z3 mappings implementation

Hello,

I'm currently working on improving Owi's test coverage, especially for symbolic interpretation.
OCamlPro/owi#96

Some z3 mappings are missing.
For example, Ceil and Floor float unop.
https://github.com/formalsec/encoding/blob/4cd856eacc9fb23fdfcf4fd0b21d0de311ac2ae7/lib/z3_mappings.ml#L408

Do you plan to implement them?

Thanks

Z3 overrides signal handlers

When solving, signals raised in ocaml are typically ignored.

Code that creates signals:

let run_with_timeout limit f =
  let set_timer limit =
    ignore
    @@ Unix.setitimer Unix.ITIMER_REAL
         Unix.{ it_value = limit; it_interval = 0.01 }
  in
  let unset () =
    ignore
    @@ Unix.setitimer Unix.ITIMER_REAL Unix.{ it_value = 0.; it_interval = 0. }
  in
  set_timer limit;
  Sys.set_signal Sys.sigalrm (Sys.Signal_handle (fun _ -> raise Out_of_time));
  let f () = try `Ok (f ()) with Out_of_time -> `Timeout in
  Fun.protect f ~finally:unset

No mappings for `to_ieee_bv` operator in Bitwuzla

Possible solution from smt-lib:

:note
 "There is no function for converting from (_ FloatingPoint eb sb) to the
  corresponding IEEE 754-2008 binary format, as a bit vector (_ BitVec m) with 
  m = eb + sb, because (_ NaN eb sb) has multiple, well-defined representations.
  Instead, an encoding of the kind below is recommended, where f is a term
  of sort (_ FloatingPoint eb sb):

   (declare-fun b () (_ BitVec m))
   (assert (= ((_ to_fp eb sb) b) f))
 "

Bitwuzla segfaults when running with multiple solvers in parallel

Use Z3 bindings to lift floating-point values

Is your feature request related to a problem? Please describe.
Currently, floating-point (fp) value lifting is done through string parsing of the fp numeral string representation. This is problematic as one cannot guarantee that this fp numeral string representation will be kept in future versions of Z3.

Describe the solution you'd like
Rather than parsing the floating-point numeral string, employ the OCaml Z3 bindings to decode floating-point values into the abstract syntax.

Describe alternatives you've considered
Alternatives have yet to be considered.

Additional context
No additional context.

Test simplifications for `extract` and `concat`

After #32 we need to properly rewrite extract and concat operators

Bring ECMA-SL's concrete evaluation to encoding

Needed in order to allow for the completion of formalsec/ECMA-SL#20

• ☑️ Exists
• ❌ TODO
• ⛔ Will not support
• ❗ Might exist, needs verification
• ❓ Don't know yet, don't add for now

Unary

Operators	Status	New Name
Typeof	⛔
Neg	☑️
BitwiseNot	☑️
LogicalNot	☑️
IntToFloat	☑️
IntToString	☑️
IntToFourHex	⛔
OctalToDecimal	⛔
FloatToInt	☑️
FloatToString	☑️
ToInt	⛔
ToInt32	⛔
ToUint16	⛔
ToUint32	⛔
IsNaN	☑️
StringToInt	☑️
StringToFloat	☑️
FromCharCode	☑️
FromCharCodeU	⛔
ToCharCode	☑️
ToCharCodeU	⛔
ToLowerCase	⛔
ToUpperCase	⛔
Trim	☑️
StringLen	☑️	Length
StringLenU	⛔
StringConcat	☑️
ObjectToList	⛔
ObjectFields	⛔
ArrayLen	⛔
ListToArray	⛔
ListHead	❌	Head
ListTail	❌	Tail
ListLen	❌	Length
ListSort	⛔
ListReverse	❌	Reverse
ListRemoveLast	⛔
TupleFirst	❌	Head
TupleSecond	❌	Tail
TupleLen	❌	Length
FloatToByte	⛔
Float32ToLEBytes	⛔
Float32ToBEBytes	⛔
Float64ToLEBytes	⛔
Float64ToBEBytes	⛔
Float32FromLEBytes	⛔
Float32FromBEBytes	⛔
Float64FromLEBytes	⛔
Float64FromBEBytes	⛔
BytesToString	⛔
Random	⛔
Abs	☑️
Sqrt	☑️
Ceil	☑️
Floor	☑️
Trunc	☑️
Exp	☑️
Log2	⛔
LogE	⛔
Log10	⛔
Sin	⛔
Cos	⛔
Tan	⛔
Sinh	⛔
Cosh	⛔
Tanh	⛔
Asin	⛔
Acos	⛔
Atan	⛔
Utf8Decode	⛔
HexDecode	⛔
ParseNumber	⛔
ParseString	⛔
ParseDate	⛔

Binary

Operator	Status	New Name
Plus	☑️
Minus	☑️
Times	☑️
Div	☑️
Modulo	☑️
Pow	☑️
BitwiseAnd	☑️
BitwiseOr	☑️
BitwiseXor	☑️
ShiftLeft	☑️
ShiftRight	☑️
ShiftRightLogical	☑️
LogicalAnd	☑️
LogicalOr	☑️
SCLogicalAnd	☑️
SCLogicalOr	☑️
Eq	☑️
NE	☑️
Lt	☑️
Gt	☑️
Le	☑️
Ge	☑️
ToPrecision	⛔
ToExponential	⛔
ToFixed	⛔
ObjectMem	⛔
StringNth	☑️
StringNthU	⛔
StringSplit	⛔
ArrayMake	⛔
ArrayNth	⛔
ListMem	⛔
ListNth	❌	At
ListAdd	❌	List_append_last
ListPrepend	❌	List_append
ListConcat	❌	Concat
ListRemove	⛔
ListRemoveNth	⛔
TupleNth	❌	At
IntToBEBytes	⛔
IntFromLEBytes	⛔
UintFromLEBytes	⛔
Min	☑️
Max	☑️
Atan2	⛔

Ternary

Operator	Status	New Name
ITE	☑️
StringSubstr	☑️
StringSubstrU	⛔
ArraySet	⛔
ListSet	❌	List_set

N-Ary

Operator	Status
NAryLogicalAnd	⛔
NAryLogicalOr	⛔
ArrayExpr	☑️
ListExpr	☑️
TupleExpr	☑️

Rename `Seq_` to `String_` to avoid exposing solver implementation of string operators

Lower bounds CI

Add a CI rule that maximise this criteria in opam to emulate the lower-bounds checking in opam-ci:

+removed,+count[version-lag,solution]

Add Bitwuzla solver

Bitwuzla mappigs

• Bitv (#78)
• Float
• Solver
• Model

Hash-consing

`Unit` value

Add support for Unit

Unit

Unit is like void

Avoid installing Z3 as default solver

Ship the encoding with another solver that is quicker to install (Bitwuzla?). Is it possible to retain the z3_mappings implementation? Perhaps, utilize a stub z3 library that fails at runtime if z3 is not installed?

Update code documentation