formalsec/smtml

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

smtml's Issues

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+'};');
	

Add support for I8 and I16 bitvectors

Current state:

• I8
• I16

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.

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?

Model with incorrect symbol

Introduced in #59

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.

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

...

wrong repo

Add remaining cases to Expr simplification

Related to OCamlPro/owi#122

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

Test simplifications

Due to #60

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]

Colibri2 mappings

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

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

Hash-consing

remove dependency on Core

it's heavy!

SAT caching

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

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

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

Integer numeric evaluation

Por exemplo:

antes era:

Program Print
(Val Int -1)

Agora é:

>Program Print
(int.sub 5 6)

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.

Improve hc

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

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.

Missing simplifications

Some simplifications are missing/incomplete.

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

Should be:
(int.add $_descending 13)

Improve parsing error messages

Undefined references just blow up with Not_found 😢

SMT Arrays

Model linear memory using arrays

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	☑️

Add Bitwuzla solver

Bitwuzla mappigs

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

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)))

Incorrect float parsing

Error on 2.

Provide datastructures for hashconsed expressions

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

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

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.