fixes variable rewriter and some Primus Lisp symbolic functions (#1350)

* fixes variable rewriter and some Primus Lisp symbolic functions

The variable rewriter was incorrectly setting the mask when a register
was modified through its alias. Instead of preserving the bits that
are not set it was erasing them.

There were also a couple of issues in handling registers and variables
in the Primus Lisp lifter. First of all, let bindings were breaching
the type system by binding variables to values that have different
type. The set function was sometimes mistyping the
registers (reminiscent of times when there were no pseudo-registers).

* allows macos to fail without canceling all other jobs

It fails too often and for random but independent of us reasons.

Author: ivg

.github/workflows/build-dev-repo.yml

@@ -15,6 +15,7 @@ jobs:
           - 4.08.x
 
     runs-on: ${{ matrix.os }}
+    continue-on-error: ${{ matrix.os == 'macos-latest'}}
 
     env:
       TMPDIR: /tmp

lib/bap_core_theory/bap_core_theory.mli

@@ -1296,6 +1296,11 @@ module Theory : sig
     (** the slot to store program semantics.  *)
     val slot : (program, t) Knowledge.slot
 
+    (** the value of the effect.
+
+        Represents the value of side-effectful compuations.
+
+        @since 2.3.0 *)
     val value : (cls, unit Value.t) Knowledge.slot
 
     include Knowledge.Value.S with type t := t
@@ -2041,37 +2046,53 @@ module Theory : sig
   *)
   module Origin : sig
 
-    (** []  *)
+    (** the abstract representation of an aliased register origin.  *)
     type ('s,'k) t = ('s,'k) origin
 
-    (** type index of the *)
+    (** the type index of the sub-registers *)
     type sub
+
+    (** the type index for the super-registers  *)
     type sup
 
+    (** [cast_sub origin] recovers the kind of the origin.  *)
     val cast_sub : ('a,unit) t -> ('a,sub) t option
+
+    (** [cast_sup origin] recovers the kind of the origin.  *)
     val cast_sup : ('a,unit) t -> ('a,sup) t option
 
 
     (** [reg origin] is the base register.
 
-        The returned value is never an alias itself. *)
+        The returned value is never an alias itself, i.e., it is a
+        base register. *)
     val reg : ('a,sub) t -> 'a Bitv.t Var.t
 
+
+    (** [is_alias origin] if the the base register has the same size
+        and sort as the aliased register.  *)
     val is_alias : ('a,sub) t -> bool
 
 
     (** [hi origin] the inclusive upper bound.
         When an alias is a subset of the [origin] register,
         [hi origin] is the most significant bit of the alias
-        register.
-
-    *)
+        register. *)
     val hi : ('a,sub) t -> int
 
     (** [lo origin] returns the inclusive upper bound of the origin register
         to which an alias belongs. *)
     val lo : ('a,sub) t -> int
 
+
+    (** [regs origin] returns an ordered list of constituent registers.
+
+        The registers are sorted in the big endian order, i.e., the
+        first element of the list corresponds to the most significant
+        part of the base register. This is the same order, in which
+        the aliasing was specified, e.g., if the aliasing was defined
+        as, [def x [reg hix; reg lox], then [regs] will
+        return [hix; lox].*)
     val regs : ('a,sup) t -> 'a Bitv.t Var.t list
 
   end

lib/bap_core_theory/bap_core_theory_pass.ml

@@ -97,7 +97,8 @@ module Desugar(CT : Core) : Core = struct
       let open Bitvec.Make(struct
           let modulus = Bitvec.modulus dst_len
         end) in
-      let mask = (one lsl int src_len - one) lsl int off in
+      let mask =
+        lnot ((one lsl int src_len - one) lsl int off) in
       let x = CT.(logand (var dst) (int s mask)) in
       let off = int off in
       let y = if Bitvec.equal off zero

lib/bap_primus/bap_primus_lisp_semantics.ml

@@ -432,7 +432,6 @@ module Prelude(CT : Theory.Core) = struct
       | {data=Var {data={exp=n}}} -> lookup@@var n
       | {data=Sym {data=s}} -> sym (KB.Name.unqualified s)
       | {data=Ite (cnd,yes,nay)} -> ite cnd yes nay
-      | {data=Let ({data={exp=n; typ=Type t}},x,y)} -> let_ ~t n x y
       | {data=Let ({data={exp=n}},x,y)} -> let_ n x y
       | {data=App (Dynamic name,args)} -> app name args
       | {data=Seq xs} -> seq_ xs
@@ -545,9 +544,10 @@ module Prelude(CT : Theory.Core) = struct
       Scope.lookup v >>= function
       | Some v -> eval x >>= assign target ~local:true v
       | None -> eval x >>= assign target v
-    and let_ ?(t=word) v x b =
+    and let_ v x b =
       let* xeff = eval x in
-      let orig = Theory.Var.define (bits t) (KB.Name.to_string v) in
+      let s = Theory.Value.sort (res xeff) in
+      let orig = Theory.Var.define s (KB.Name.to_string v) in
       if is_parameter prog orig
       then
         Env.set orig (res xeff) >>= fun () ->

lib/graphlib/graphlib.mli

@@ -1176,7 +1176,7 @@ module Std : sig
         solution is always a lower approximation of a real solution,
         so it is always safe to use it).
 
-        @param the upper bound to the number of iterations the solver
+        @param steps the upper bound to the number of iterations the solver
         can make.
 
         @param start the entry node of the graph

plugins/primus_lisp/primus_lisp_main.ml

@@ -320,7 +320,15 @@ module Semantics = struct
       sysdatadir / "primus" / "semantics";
     ]
 
+  let check_user_provided paths =
+    match List.find paths ~f:(Fn.non is_folder) with
+    | None -> ()
+    | Some path ->
+      invalid_argf "unable to load semantics from %S, \
+                    the path must exist and be a folder" path ()
+
   let load_lisp_sources paths =
+    check_user_provided paths;
     let paths = List.filter ~f:is_folder (paths @ default_paths) in
     let features = "core"::List.concat_map ~f:collect_features paths in
     let paths = paths @ library_paths in

plugins/primus_lisp/primus_lisp_semantic_primitives.ml

@@ -188,7 +188,7 @@ let export = Primus.Lisp.Type.Spec.[
     "get-current-program-counter", unit @-> int,
     "(get-current-program-counter) is an alias to (get-program-counter)";
 
-    "set-symbol-value", tuple [sym; a] @-> a,
+    "set-symbol-value", tuple [int; a] @-> a,
     "(set-symbol-value S X) sets the value of the symbol S to X.
          Returns X";
 
@@ -198,6 +198,10 @@ let export = Primus.Lisp.Type.Spec.[
     "is-symbol", one any @-> bool,
     "(is-symbol X) is true if X has a symbolic value.";
 
+    "alias-base-register", one int @-> int,
+    "(alias-base-register x) if X has a symbolic value that is an
+     aliased register returns the base register";
+
     "cast-low", tuple [int; a] @-> b,
     "(cast-low S X) extracts low S bits from X.";
 
@@ -582,13 +586,40 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
     | None -> !!(empty s)
     | Some addr -> forget@@const_int s addr
 
-  let set_symbol v x =
-    match KB.Value.get Primus.Lisp.Semantics.symbol v with
-    | Some name ->
-      let var = Theory.Var.define (Theory.Value.sort x) name in
-      CT.set var !!x
+  let require_symbol v k =
+    match symbol v with
+    | Some name -> k name
+    | None -> illformed "not a symbolic value"
+
+  let possibly_register target v =
+    require_symbol v @@ fun v ->
+    match Theory.Target.var target v with
+    | Some v -> !!v
     | None ->
-      illformed "requires a value reified to a variable"
+      let s = Theory.Bitv.define (Theory.Target.bits target) in
+      KB.return @@ Theory.Var.forget (Theory.Var.define s v)
+
+  let set_symbol t v x =
+    let* var = possibly_register t v in
+    let x = KB.Value.refine x (Theory.Var.sort var) in
+    CT.set var !!x
+
+  let alias_base_register target v =
+    let* r = possibly_register target v in
+    match Theory.Target.unalias target r with
+    | None ->
+      illformed "the register %a is not an alias in %a"
+        Theory.Var.pp r Theory.Target.pp target
+    | Some origin -> match Theory.Origin.cast_sub origin with
+      | None ->
+        illformed "the aliased register %a is not a subregister"
+          Theory.Var.pp r
+      | Some origin ->
+        let reg = Theory.Origin.reg origin in
+        let name = Theory.Var.name reg in
+        forget @@
+        CT.var reg >>| fun v ->
+        KB.Value.put Primus.Lisp.Semantics.symbol v (Some name)
 
   let symbol s v =
     match KB.Value.get Primus.Lisp.Semantics.symbol v with
@@ -755,9 +786,10 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
     | "store-word",_-> data@@store_word t args
     | "get-program-counter",[]
     | "get-current-program-counter",[] -> pure@@get_pc s lbl
-    | "set-symbol-value",[sym;x] -> data@@set_symbol sym x
+    | "set-symbol-value",[sym;x] -> data@@set_symbol t sym x
     | "symbol",[x] ->  pure@@symbol s x
     | "is-symbol", [x] -> pure@@is_symbol x
+    | "alias-base-register", [x] -> pure@@alias_base_register t x
     | "cast-low",xs -> pure@@low xs
     | "cast-high",xs -> pure@@high xs
     | "cast-signed",xs -> pure@@signed xs