Interpreter

src/argOptions.ml

@@ -12,11 +12,13 @@ module ExecMode = struct
     | Consort
     | Ownership
     | Typecheck
+    | Interp
 
   let pairs = [
     ("consort", Consort);
     ("ownership", Ownership);
-    ("typecheck", Typecheck)
+    ("typecheck", Typecheck);
+    ("interp", Interp)
   ]
   let default = "consort"
   let candidates = List.map (fun (s, _) -> s) pairs

src/ast.ml

@@ -54,7 +54,10 @@ let position_of_sexp sexp =
   | _ -> Sexplib.Conv_error.tuple_of_size_n_expected "position" 2 sexp
 
 type raw_exp =
-  | Unit
+  | Unit of string option (* The constructor could be called Ignore, because the
+                             argument to this constructor is a variable name,
+                             whose value is just ignored by the analysis;
+                             it is used only by the interpreter. *)
   | Fail
   | Cond of string * exp * exp
   | NCond of string * exp * exp

src/astPrinter.ml

@@ -158,7 +158,7 @@ let rec pp_expr ~ip:((po_id,pr_id) as ip) ~annot (id,e) =
           semi;
           pp_expr ~ip ~annot e
         ]
-    | Unit -> ps "()"
+    | Unit _ -> ps "()"
     | Return v -> pf "return%a %s" po_id id v
     | Fail -> ps "fail"
   in

src/astUtil.ml

@@ -1,7 +1,4 @@
-let parse_file in_name =
-  let f = open_in in_name in
-  let lexbuf = Lexing.from_channel f in
-  Locations.set_file_name lexbuf in_name 1;
+let parse lexbuf =
   try
     Parser.prog Lexer.read lexbuf |> SurfaceAst.simplify
   with
@@ -11,3 +8,11 @@ let parse_file in_name =
       let open Lexing in
       failwith @@ Printf.sprintf "Lexing error at %s" @@ Locations.string_of_location lexbuf.lex_curr_p
 
+let parse_file in_name =
+  let f = open_in in_name in
+  let lexbuf = Lexing.from_channel f in
+  Locations.set_file_name lexbuf in_name 1;
+  parse lexbuf
+
+let parse_string s =
+  parse @@ Lexing.from_string s

src/astUtil.mli

@@ -1 +1,2 @@
 val parse_file: string -> Ast.prog
+val parse_string: string -> Ast.prog

src/consort.ml

@@ -222,3 +222,14 @@ let typecheck ~opts file =
   let simple_res = SimpleChecker.typecheck_prog simple_op ast in
   print_typecheck simple_res ast;
   Verified
+
+let interp ~opts file =
+  let ast = AstUtil.parse_file file in
+  let intr_op = (ArgOptions.get_intr opts).op_interp in
+  let simple_typing = RefinementTypes.to_simple_funenv intr_op in
+  let simple_res = SimpleChecker.typecheck_prog simple_typing ast in
+  ignore simple_res;
+  let open Interpreter in
+  pp_val (eval_prog ast) Format.std_formatter;
+  Format.pp_print_newline Format.std_formatter ();
+  Verified

src/consort.mli

@@ -16,3 +16,4 @@ val result_to_string : check_result -> string
 val consort : opts:ArgOptions.t -> string -> check_result
 val ownership : opts:ArgOptions.t -> string -> check_result
 val typecheck : opts:ArgOptions.t -> string -> check_result
+val interp : opts:ArgOptions.t -> string -> check_result

src/dune

@@ -19,7 +19,7 @@
  (preprocess (pps ppx_sexp_conv ppx_let with_monad ppx_custom_printf ppx_cast))
  (wrapped false)
  (libraries sexplib util)
- (modules Parser Ast SurfaceAst AstPrinter SimpleChecker Lexer LabelManager SimpleTypes RefinementTypes Paths AstUtil Intrinsics Locations))
+ (modules Parser Ast SurfaceAst AstPrinter SimpleChecker Lexer LabelManager SimpleTypes RefinementTypes Paths AstUtil Intrinsics Locations Interpreter))
 
 (library
  (name solving)
@@ -75,3 +75,9 @@
  (preprocess (pps ppx_sexp_conv ppx_let with_monad ppx_custom_printf ppx_cast))
  (libraries lang)
  (modules genFlags))
+
+(test
+ (name interpreter_test)
+ (libraries consort ounit2)
+ (modules Interpreter_test))
+

src/flowInference.ml

@@ -2214,7 +2214,7 @@ let relation_name ((e_id,_),expr) ctxt =
     | Alias _ -> "alias"
     | NCond _ -> "ifnull"
     | Cond _ -> "ifz"
-    | Unit -> "unit"
+    | Unit _ -> "unit"
     | Return _ -> "return"
     | Fail -> "fail"
   in
@@ -2353,7 +2353,7 @@ let rec process_expr ~output (((relation : relation),tyenv) as st) continuation
   let%bind iso = get_iso_at e_id in
   save_snapshot >>
   match e with
-  | Unit ->
+  | Unit _ ->
     begin
       match continuation with
       | Some out_relation ->

src/interpreter.ml

@@ -0,0 +1,227 @@
+open Ast
+open PrettyPrint
+
+(* values *)
+type v =
+  | IntV of int
+  | NilV
+  | RefV of v ref
+  | ArrayV of v array
+  | TupleV of v list
+
+let rec pp_val = function
+  | IntV i -> pi i
+  | NilV -> ps "null"
+  | RefV v ->
+     pl [
+         ps "ref ";
+         pp_val !v
+       ]
+  | ArrayV arr ->
+     pl [
+         ps "[|";
+         psep "; " @@ Array.to_list @@ Array.map pp_val arr;
+         ps "|]"
+       ]
+  | TupleV [] -> assert false
+  | TupleV vs ->
+     pl [
+         ps "(";
+         psep ", " @@ List.map pp_val vs;
+         ps ")"
+       ]
+
+exception NotImplemented of string
+
+type env = (string * v) list
+
+let rec lookup_fundef f = function
+  | [] -> assert false
+  | { name = g; args = params; body = e} :: rest ->
+     if f = g then (params, e)
+     else lookup_fundef f rest
+
+let empty_env = []
+let lookup = List.assoc
+let rec extend patt valu env =
+  match patt with
+  | PVar id -> (id, valu) :: env
+  | PTuple pats ->
+     begin match valu with
+     | TupleV vs -> List.fold_right2 extend pats vs env
+     | _ -> assert false
+     end
+  | PNone -> env
+
+let intV_of_bool b =
+  if b then IntV 0 else IntV 1
+
+let intrinsic_funs = [
+    ("!=", function [IntV i1; IntV i2] -> intV_of_bool @@ (i1 != i2) | _ -> assert false);
+    ("%", function [IntV i1; IntV i2] -> IntV (i1 mod i2) | _ -> assert false);
+    ("&&", function [IntV i1; IntV i2] -> intV_of_bool ((i1 = 0) && (i2 = 0)) | _ -> assert false);
+    ("*", function [IntV i1; IntV i2] -> IntV (i1 * i2) | _ -> assert false);
+    ("+", function [IntV i1; IntV i2] -> IntV (i1 + i2) | _ -> assert false);
+    ("-", function [IntV i1; IntV i2] -> IntV (i1 - i2) | _ -> assert false);
+    ("<", function [IntV i1; IntV i2] -> intV_of_bool (i1 < i2) | _ -> assert false);
+    ("<=", function [IntV i1; IntV i2] -> intV_of_bool (i1 <= i2) | _ -> assert false);
+    ("=", function [IntV i1; IntV i2] -> intV_of_bool (i1 = i2) | _ -> assert false);
+    (">", function [IntV i1; IntV i2] -> intV_of_bool (i1 > i2) | _ -> assert false);
+    (">=", function [IntV i1; IntV i2] -> intV_of_bool (i1 >= i2) | _ -> assert false);
+    ("||", function [IntV i1; IntV i2] -> intV_of_bool ((i1 = 0) || (i2 = 0)) | _ -> assert false);
+  ]
+
+let eval_imm_op env = function
+  | IVar id -> lookup id env
+  | IInt i -> IntV i
+
+let eval_ap env (p : Paths.concr_ap) =
+  let rec follow_step v = function
+    | [] -> v
+    | `Deref :: rest -> (match follow_step v rest with RefV r -> !r | _ -> assert false)
+    | `Proj i :: rest -> (match follow_step v rest with TupleV tp -> List.nth tp i | _ -> assert false)
+    | _ -> assert false
+  in
+  match (p :> Paths.root * Paths.steps list * Paths.suff) with
+  | (Paths.Var id, steps, _) -> follow_step (lookup id env) steps
+  | _ -> assert false
+
+let rec eval_refine env =
+  let open RefinementTypes in
+  function
+  | Top -> (fun _ -> true)
+  | ConstEq n -> (fun i -> i = n)
+  | And(r1, r2) -> (fun i -> eval_refine env r1 i && eval_refine env r2 i)
+  | Relation {rel_cond; rel_op2; _} ->
+     (fun i ->
+       let j =
+         match rel_op2 with
+         | RAp ap -> eval_ap env ap
+         | RConst j -> IntV j
+       in
+       try
+         IntV 0 = List.assoc rel_cond intrinsic_funs [IntV i; j]
+       with
+       | Not_found -> assert false)
+  | NamedPred _ -> raise (NotImplemented "named predicate in the condition")
+
+let rec really_read_int env condopt =
+  match read_int(), condopt with
+  | i, None -> i
+  | i, Some cond ->
+     if eval_refine env cond i then i
+     else
+       begin
+         Printf.eprintf "Condition violated! Give me another integer: ";
+         flush stderr;
+         really_read_int env condopt
+       end
+  | exception Failure _ ->
+     begin
+       Printf.eprintf "It's not an integer! Give me an INTEGER: ";
+       flush stderr;
+       really_read_int env condopt
+     end
+
+let eval_ref_contents loc contents env = match contents with
+  | RNone ->
+     Printf.eprintf "%s: Give me an integer: " (Locations.string_of_location loc);
+     flush stderr;
+     IntV (really_read_int env None)
+  | RInt i -> IntV i
+  | RVar id -> lookup id env
+
+let eval_exp fundecls =
+  let rec aux env = function
+    | (_, Unit None) -> IntV 0
+    | (_, Unit (Some id)) -> lookup id env
+    | ((_,loc), Fail) -> Locations.raise_errorf ~loc "Fail"
+    | (_, Cond (var, then_exp, else_exp)) ->
+       begin match lookup var env with
+       | IntV 0 -> aux env then_exp
+       | IntV _ -> aux env else_exp
+       | _ -> assert false
+       end
+    | (_, NCond (var, then_exp, else_exp)) ->
+       begin match lookup var env  with
+       | NilV -> aux env then_exp
+       | RefV _ -> aux env else_exp
+       | _ -> assert false
+       end
+    | (_, Seq (exp1, exp2)) ->
+       ignore(aux env exp1);
+       aux env exp2
+    | ((_,loc), Assign (var1, rhs, exp')) ->
+       begin match lookup var1 env with
+       | RefV r -> r := eval_imm_op env rhs; aux env exp'
+       | NilV -> Locations.raise_errorf ~loc "NullPointerException"
+       | _ -> assert false
+       end
+    | ((_,loc), Let (pat, rhs, exp')) ->
+       let res =
+         match rhs with
+         | Var id -> lookup id env
+         | Const i -> IntV i
+         | Mkref init -> RefV (ref (eval_ref_contents loc init env))
+         | MkArray id ->
+            begin match lookup id env with
+            | IntV len -> ArrayV (Array.make len (IntV 0))
+            | _ -> assert false
+            end
+         | Call {callee=f; arg_names=xs; _} ->
+            let args = List.map (fun id -> lookup id env) xs in
+            begin
+              try List.assoc f intrinsic_funs args with
+                Not_found ->
+                let params, body = lookup_fundef f fundecls in
+                let newenv = List.fold_right2 (fun p v env -> (p, v)::env) params args env in
+                aux newenv body
+            end
+         | Deref id ->
+            begin match lookup id env with
+            | NilV -> Locations.raise_errorf ~loc "NullPointerException"
+            | RefV r -> !r
+            | _ -> assert false
+            end
+         | Tuple contents -> TupleV (List.map (fun c -> eval_ref_contents loc c env) contents)
+         | Nondet cond ->
+            Printf.eprintf "%s: Give me an integer: " (Locations.string_of_location loc);
+            flush stderr;
+            IntV (really_read_int env cond)
+         | Read (id1, id2) ->
+            begin match lookup id1 env, lookup id2 env with
+            | ArrayV arr, IntV ind -> arr.(ind)
+            | _ -> assert false
+            end
+         | LengthOf id ->
+            begin match lookup id env with
+            | ArrayV arr -> IntV (Array.length arr)
+            | _ -> assert false
+            end
+         | Null -> NilV
+       in
+       let newenv = extend pat res env in
+       aux newenv exp'
+    | (_, Update (base, ind, rhs, exp')) ->
+       begin match lookup base env, lookup ind env, lookup rhs env with
+       | ArrayV arr, IntV i, v -> arr.(i) <- v; aux env exp'
+       | _ -> assert false
+       end
+    | ((_, loc), Alias (ap1, ap2, exp')) ->
+       begin match eval_ap env ap1, eval_ap env ap2 with
+       |  RefV r1, RefV r2 -> if r1 == r2 then aux env exp'
+                              else Locations.raise_errorf ~loc "Alias Failure"
+       | _ -> assert false
+       end
+    | ((_, loc), Assert ({rop1; cond; rop2}, exp')) ->
+       begin match
+         List.assoc cond intrinsic_funs [eval_imm_op env rop1; eval_imm_op env rop2]
+       with
+       | IntV 0 -> aux env exp'
+       | _ -> Locations.raise_errorf ~loc "Assertion Failure"
+       | exception Not_found -> assert false
+       end
+    | (_, Return var) -> lookup var env
+  in aux
+
+let eval_prog (fundecls, main) = eval_exp fundecls empty_env main

src/interpreter_test.ml

@@ -0,0 +1,16 @@
+open OUnit2
+
+let test1 _test_ctxt =
+  assert_equal
+    (Interpreter.eval_prog (AstUtil.parse_string "{ 1 + 1 }"))
+    (Interpreter.IntV 2)
+
+let suite =
+  "suite">:::
+    [
+      "test1">:: test1
+    ]
+
+let () =
+  run_test_tt_main suite
+

src/ownershipInference.ml

@@ -593,7 +593,7 @@ let rec process_expr ~output ((e_id,_),expr) =
         constrain_eq ~e_id ~src:curr_t ~dst:out_t
       ) output_types
     >> return `Return
-  | Unit -> return `Cont
+  | Unit _ -> return `Cont
   | Seq (e1,e2) ->
     let%bind stat = process_expr ~output e1 in
     assert (stat <> `Return);

src/simpleChecker.ml

@@ -415,7 +415,7 @@ let rec process_expr ret_type ctxt ((id,loc),e) res_acc =
     | IVar v -> unify_var v t
   in
   match e with
-  | Unit -> res_acc,false
+  | Unit _ -> res_acc,false
   | Cond (v,e1,e2) ->
     unify_var v `Int;
     process_expr ret_type ctxt e1 res_acc

src/surfaceAst.ml

@@ -108,7 +108,7 @@ let rec simplify_expr ?next ~is_tail count e : pos * A.raw_exp =
     if is_tail then
       simplify_expr ~is_tail count @@ Value (i,`OInt 0)
     else
-      A.Unit |> tag_with i
+      A.Unit None |> tag_with i
   | Value (i, v) ->
     if is_tail then
       (* lift_to_var (or lift_to_imm or lift_to_lhs) 
@@ -124,7 +124,7 @@ let rec simplify_expr ?next ~is_tail count e : pos * A.raw_exp =
       )
     else
       lift_to_var ~ctxt:i count v (fun _ _tvar ->
-        A.Unit |> tag_with i
+        A.Unit (Some _tvar) |> tag_with i
       )
   | NCond (i,v,e1,e2) ->
     A.NCond (v,simplify_expr ~is_tail count e1,simplify_expr ~is_tail count e2) |> tag_with i