c4-project / c4f

The C4 Concurrent C Fuzzer
MIT License
13 stars 1 forks source link

FIR: generalise algebraic properties to arbitrary constants #207

Closed MattWindsor91 closed 3 years ago

MattWindsor91 commented 3 years ago

Currently, the FIR operator enumeration contains various 'algebraic property' functions that answer questions like 'is x OP x always x' or 'is x OP 0 always 0'. These properties get used by the expression generator to produce statically known values.

Last evening, I inadvertently caused a lot of type system fun when I tried to posit that x != x was always 0. (This is true in C, but not in FIR, which doesn't unify false with 0.) This has got me wondering whether there is a more general design that can capture the following rules:

x +  0 -> x
x -  0 -> x
x -  x -> 0
x *  0 -> 0
x *  1 -> x
x /  1 -> x
x /  x -> 1        // hopefully!
x <= x -> true
x >= x -> true
x == x -> true
x <  x -> false
x >  x -> false
x != x -> false

Presently, the algebraic properties look like this (S_binary in Act_fir.Op_types):

val refl : t -> [`Idem | `Zero] option
(** [refl op] retrieves whether [x op x] equals [x] (Idem) or [0] (Zero). *)

val zero_lhs : t -> [`Idem | `Zero] option
(** [zero_lhs op] retrieves whether [0 op x] equals [x] (Idem) or [0]
    (Zero). *)

val zero_rhs : t -> [`Idem | `Zero] option
(** [zero_rhs op] retrieves whether [x op 0] equals [x] (Idem) or [0]
    (Zero). *)

One approach might be to introduce a new Op_rule.t type that looks like this:

type t =
  | Idem (** Reduces to the variable in the expression. *)
  | Const of Constant.t (** Reduces to a particular constant. *)
  | Unknown (** Reduction can't be statically determined. *)

(* insert existing `is_idem`, `is_zero`, etc. getters here *)

and promote zero_lhs and zero_rhs to instead accept constants to put on the left and right hand side respectively.

MattWindsor91 commented 3 years ago

This is done now, though things other than 0, true, and false aren't actually exercised yet.