CLI: Parse isla's value expression including function calls

cli/lib/isla/assertion.ml

@@ -1,14 +1,8 @@
 (** Boolean expression language for isla litmus test assertions. *)
 
-type loc =
-  | Reg of int * string
-  | Mem of string
-
 type op = Eq | Ne
 
-type atom =
-  | CmpCst of loc * op * Z.t
-  | CmpLoc of loc * op * loc
+type atom = Cmp of Term.t * op * Term.t
 
 type expr =
   | Atom of atom
@@ -18,15 +12,11 @@ type expr =
   | True
   | False
 
-module Testrepr = Litmus.Testrepr
-
 let negate_op = function
   | Eq -> Ne
   | Ne -> Eq
 
-let negate_atom = function
-  | CmpCst (loc, op, value) -> CmpCst (loc, negate_op op, value)
-  | CmpLoc (lhs, op, rhs) -> CmpLoc (lhs, negate_op op, rhs)
+let negate_atom (Cmp (lhs, op, rhs)) = Cmp (lhs, negate_op op, rhs)
 
 let rec negate = function
   | Atom atom -> Atom (negate_atom atom)

cli/lib/isla/assertion.mli

@@ -1,13 +1,6 @@
-type loc =
-  | Reg of int * string
-  | Mem of string
-(** A location to get data from. [Mem] mean the data at that location in memory *)
-
 type op = Eq | Ne
 
-type atom =
-  | CmpCst of loc * op * Z.t
-  | CmpLoc of loc * op * loc
+type atom = Cmp of Term.t * op * Term.t
 
 type expr =
   | Atom of atom

cli/lib/isla/converter.ml

@@ -49,14 +49,24 @@ let mem_requirement op value =
   | Assertion.Eq -> Testrepr.MemEq value
   | Assertion.Ne -> Testrepr.MemNe value
 
+let resolve_term ~env expr =
+  match expr with
+  | Term.LocVal loc -> `Loc loc
+  | Term.Deref (Mem sym) -> `Deref sym
+  | _ -> `Const (Term.eval ~env expr)
+
 let atoms_to_conds ~resolve_sym ~memory_size atoms =
+  let env = function
+    | Term.Mem sym -> Some (Z.of_int (resolve_sym sym))
+    | Term.Reg _ -> None
+  in
   let reg_atoms, mem_atoms =
     List.fold_left
-      (fun (reg_atoms, mem_atoms) atom ->
-        match atom with
-        | Assertion.CmpCst (Assertion.Reg (tid, reg), op, value) ->
+      (fun (reg_atoms, mem_atoms) (Assertion.Cmp (lhs, op, rhs)) ->
+        match resolve_term ~env lhs, resolve_term ~env rhs with
+        | `Loc (Term.Reg (tid, reg)), `Const value ->
           ((tid, reg, reg_requirement op value) :: reg_atoms, mem_atoms)
-        | Assertion.CmpCst (Assertion.Mem sym, op, value) ->
+        | `Loc (Term.Mem sym), `Const value ->
           let mem_cond : Testrepr.mem_cond =
             {
               sym;
@@ -66,10 +76,26 @@ let atoms_to_conds ~resolve_sym ~memory_size atoms =
             }
           in
           (reg_atoms, mem_cond :: mem_atoms)
-        | Assertion.CmpLoc (Assertion.Reg _, _, _) ->
+        | `Loc (Term.Reg _), `Loc _ ->
           failwith "assertion: register-to-location comparisons are not supported"
-        | Assertion.CmpLoc (Assertion.Mem _, _, _) ->
-          failwith "assertion: memory-to-location comparisons are not supported")
+        | `Loc (Term.Mem _), _ ->
+          failwith "assertion: memory-to-location comparisons are not supported"
+        | _, `Deref _ ->
+          failwith "assertion: deref (*x) on RHS is not supported"
+        | `Deref sym, `Const value ->
+          let mem_cond =
+            {
+              Testrepr.sym = sym;
+              addr = resolve_sym sym;
+              size = memory_size sym;
+              req = mem_requirement op value;
+            }
+          in
+          (reg_atoms, mem_cond :: mem_atoms)
+        | `Deref _, _ ->
+          failwith "assertion: deref (*x) on LHS requires constant RHS"
+        | `Const _, _ ->
+          failwith "assertion: constant expression on LHS is not supported")
       ([], [])
       atoms
   in
@@ -109,10 +135,15 @@ let to_final_conds ~expect_is_sat ~resolve_sym ~memory_size assertion =
           Some (Testrepr.Unobservable (thread_conds, mem_conds)))
     dnf
 
-let z_of_value syms = function
-  | Ir.Int z -> z
-  | Ir.Sym sym ->
-    Z.of_int (Symbols.resolve syms sym)
+let sym_env syms = function
+  | Term.Mem sym ->
+    (match Symbols.resolve_opt syms sym with
+     | Some addr -> Some (Z.of_int addr)
+     | None -> None)
+  | Term.Reg _ -> None
+
+let z_of_value syms expr =
+  Term.eval ~env:(sym_env syms) expr
 
 let build_registers syms ~arch pc (thread : Ir.thread) =
   let pc_entry = (pc_reg arch, RegValGen.Number (Z.of_int pc)) in
@@ -180,7 +211,7 @@ let to_testrepr (ir : Ir.t) : Testrepr.t =
     List.map (fun sym ->
       let addr = Symbols.resolve syms sym in
       let init_value =
-        List.assoc_opt sym ir.locations |> Option.value ~default:(Ir.Int Z.zero)
+        List.assoc_opt sym ir.locations |> Option.value ~default:(Term.Const Z.zero)
       in
       build_data_memory syms sym addr init_value)
     ir.symbolic

cli/lib/isla/function.ml

@@ -0,0 +1,92 @@
+(** Functions for isla term evaluation.
+
+    Each function is registered with its parameter names (for keyword
+    argument alignment) and an evaluation function on positional args. *)
+
+type fn_spec = {
+  params : string list;
+  eval : Z.t list -> Z.t;
+}
+
+(** Built-in pure functions *)
+
+let arity_error name n =
+  failwith (Printf.sprintf "function %s: expected %d args" name n)
+
+let bv_functions : (string * fn_spec) list = [
+  "bvand", {
+    params = ["a"; "b"];
+    eval = (function [a; b] -> Z.logand a b | _ -> arity_error "bvand" 2);
+  };
+  "bvor", {
+    params = ["a"; "b"];
+    eval = (function [a; b] -> Z.logor a b | _ -> arity_error "bvor" 2);
+  };
+  "bvxor", {
+    params = ["a"; "b"];
+    eval = (function [a; b] -> Z.logxor a b | _ -> arity_error "bvxor" 2);
+  };
+  "bvshl", {
+    params = ["a"; "b"];
+    eval = (function [a; b] -> Z.shift_left a (Z.to_int b)
+            | _ -> arity_error "bvshl" 2);
+  };
+  "bvlshr", {
+    params = ["a"; "b"];
+    eval = (function [a; b] -> Z.shift_right a (Z.to_int b)
+            | _ -> arity_error "bvlshr" 2);
+  };
+  "extz", {
+    params = ["bits"; "len"];
+    eval = (function [bits; _len] -> bits
+            | _ -> arity_error "extz" 2);
+  };
+  "exts", {
+    params = ["bits"; "len"];
+    eval = (function [bits; len] ->
+              let src_bits = Z.numbits bits in
+              let len = Z.to_int len in
+              if src_bits = 0 || src_bits >= len then bits
+              else if Z.testbit bits (src_bits - 1) then
+                let mask = Z.sub (Z.shift_left Z.one len)
+                    (Z.shift_left Z.one src_bits) in
+                Z.logor bits mask
+              else bits
+            | _ -> arity_error "exts" 2);
+  };
+]
+
+let pgt_functions : (string * fn_spec) list = [
+  "page", {
+    params = ["a"];
+    eval = (function [a] ->
+              Z.logand (Z.shift_right a 12) (Z.sub (Z.shift_left Z.one 36) Z.one)
+            | _ -> arity_error "page" 1);
+  };
+]
+
+let functions : (string * fn_spec) list = bv_functions @ pgt_functions
+
+let find name = List.assoc_opt name functions
+
+let eval_fn name args =
+  match find name with
+  | Some spec -> spec.eval args
+  | None ->
+    failwith (Printf.sprintf "function: unknown %s/%d" name (List.length args))
+
+let align_kwargs name kwargs =
+  match find name with
+  | Some spec ->
+    List.map (fun param ->
+      match List.assoc_opt param kwargs with
+      | Some v -> v
+      | None ->
+        failwith (Printf.sprintf "function %s: missing argument %s" name param))
+    spec.params
+  | None ->
+    failwith (Printf.sprintf "function: unknown keyword function %s" name)
+
+let eval_kwfn name kwargs =
+  let args = align_kwargs name kwargs in
+  eval_fn name args

cli/lib/isla/ir.ml

@@ -2,14 +2,10 @@
 
 (** {1 Isla test internal representation } *)
 
-type value =
-  | Int of Z.t
-  | Sym of string
-
 type thread = {
   tid : int;
   code : string;
-  init : (string * value) list;
+  init : (string * Term.t) list;
 }
 
 type expect =
@@ -21,7 +17,7 @@ type t = {
   name : string;
   threads : thread list;
   symbolic : string list;
-  locations : (string * value) list;
+  locations : (string * Term.t) list;
   expect : expect;
   assertion : Assertion.expr;
 }
@@ -30,14 +26,44 @@ type t = {
 
 let type_error fmt = Printf.ksprintf (fun s -> raise (Otoml.Type_error s)) fmt
 
+(** Key prefixes treated as tool-internal metadata and silently ignored
+    when parsing [thread.N.reset] tables. *)
+let meta_key_prefixes = ["__isla"]
+
+let is_meta_key k =
+  List.exists (fun prefix ->
+    String.length k >= String.length prefix
+    && String.sub k 0 (String.length prefix) = prefix)
+  meta_key_prefixes
+
 let parse_value = function
-  | Otoml.TomlInteger i -> Int (Z.of_int i)
+  | Otoml.TomlInteger i -> Term.Const (Z.of_int i)
   | Otoml.TomlString s ->
-    (try Int (Z.of_string s) with Invalid_argument _ -> Sym s)
+    (try Const (Z.of_string s) with Invalid_argument _ -> LocVal (Mem s))
   | value ->
     type_error "Value is invalid, should be int or string, but is: %s"
       (Otoml.Printer.to_string value)
 
+let parse_term_string s =
+  let lexbuf = Lexing.from_string s in
+  try Parser.binding Lexer.token lexbuf
+  with Parser.Error ->
+    type_error "term parse error at position %d in: %s"
+      lexbuf.lex_curr_p.pos_cnum s
+
+let parse_reset_value = function
+  | Otoml.TomlInteger i -> Term.Const (Z.of_int i)
+  | Otoml.TomlString s ->
+    (try Term.Const (Z.of_string s)
+     with Invalid_argument _ ->
+       let expr = parse_term_string s in
+       match Term.eval ~env:(fun _ -> None) expr with
+       | z -> Const z
+       | exception Failure _ -> expr)
+  | value ->
+    type_error "reset value is invalid, should be int or string expression, but is: %s"
+      (Otoml.Printer.to_string value)
+
 let parse_thread (tid, table) =
   let tid =
     match int_of_string_opt tid with
@@ -47,7 +73,16 @@ let parse_thread (tid, table) =
   let _ = Otoml.get_table table in
   let code = Otoml.find table Otoml.get_string ["code"] |> String.trim in
   let init = Otoml.find_or ~default:[] table (Otoml.get_table_values parse_value) ["init"] in
-  { tid; code; init }
+  let parse_reset_table toml =
+    List.filter_map (fun (k, v) ->
+      if is_meta_key k then None
+      else Some (k, parse_reset_value v))
+    (Otoml.get_table toml)
+  in
+  let reset = Otoml.find_or ~default:[] table parse_reset_table ["reset"] in
+  let has_init name = List.exists (fun (k, _) -> k = name) init in
+  let merged = init @ List.filter (fun (k, _) -> not (has_init k)) reset in
+  { tid; code; init = merged }
 
 let parse_threads toml =
   let table = Otoml.get_table toml in

cli/lib/isla/lexer.mll

@@ -11,6 +11,7 @@ rule token = parse
   | [' ' '\t' '\n']+ { token lexbuf }
   | '(' { LPAREN }
   | ')' { RPAREN }
+  | ',' { COMMA }
   | '&' { AND }
   | '|' { OR }
   | '~' { NOT }

cli/lib/isla/normalize.ml

@@ -1,6 +1,7 @@
 (** Normalize architecture-specific register aliases in the IR. *)
 
 open Assertion
+open Term
 
 let register_renames () =
   Otoml.find_or ~default:[] (Litmus.Config.get ()) (Otoml.get_table_values Otoml.get_string)
@@ -15,9 +16,15 @@ let normalize_loc = function
   | Reg (tid, reg) -> Reg (tid, normalize_reg reg)
   | Mem _ as loc -> loc
 
-let normalize_atom = function
-  | CmpCst (loc, op, value) -> CmpCst (normalize_loc loc, op, value)
-  | CmpLoc (lhs, op, rhs) -> CmpLoc (normalize_loc lhs, op, normalize_loc rhs)
+let rec normalize_term = function
+  | Const _ as c -> c
+  | LocVal loc -> LocVal (normalize_loc loc)
+  | Deref loc -> Deref (normalize_loc loc)
+  | Fn (name, args) -> Fn (name, List.map normalize_term args)
+  | KwFn (name, kw) -> KwFn (name, List.map (fun (k, v) -> (k, normalize_term v)) kw)
+
+let normalize_atom (Cmp (lhs, op, rhs)) =
+  Cmp (normalize_term lhs, op, normalize_term rhs)
 
 let rec normalize_expr = function
   | Atom atom -> Atom (normalize_atom atom)