Simple implementation of ifptr via lexer/parser modification

.gitignore

@@ -15,3 +15,4 @@ auto/
 *~
 **/.merlin
 _build/
+.vscode/

.travis.yml

@@ -1,4 +1,7 @@
 language: c
+os:
+  - "linux"
+dist: "xenial"
 addons:
   apt:
     sources:
@@ -9,8 +12,8 @@ addons:
       - libstdc++6
       - libgomp1
       - libgmp-dev
-      - python
-sudo: false
+      - python3-pip
+      - python3-setuptools
 cache:
   directories:
     - $HOME/.opam

src/consort.ml

@@ -97,18 +97,27 @@ module Options = struct
           ("-show-model", Set show_model, "Print model produced from successful verification");
           ("-sigh", Unit (fun () -> save_cons := Some "sigh.smt"), "Here we go again...");
           ("-save-cons", string_opt save_cons, "Save constraints in <file>");
+          ("-show-warn", Unit (fun () ->
+              Log.set_level Log.level_warn;
+              Log.all ();
+            ), "Show warning output");
           ("-show-all", Unit (fun () ->
              List.iter (fun r -> r := true) all_debug_flags;
+             Log.set_level Log.level_debug;
              Log.all ();
            ), "Show all debug output");
           ("-none", Unit (fun () ->
              List.iter (fun r -> r:= false) all_debug_flags;
              Log.disable ()
            ), "Suppress all debug output");
           ("-debug", String (fun s ->
+             Log.set_level Log.level_debug;
              Log.filter @@ List.map String.trim @@ String.split_on_char ',' s
            ), "Debug sources s1,s2,...");
-          ("-debug-all", Unit Log.all, "Show all debug output")
+          ("-debug-all", Unit ( fun () -> 
+            Log.set_level Log.level_debug; 
+            Log.all ();
+          ), "Show all debug output")
         ] in
     (arg_defs, (fun ?(comb=default) () ->
        { comb with

src/flowInference.ml

@@ -2385,9 +2385,7 @@ let rec process_expr ~output (((relation : relation),tyenv) as st) continuation
 
   | Seq (e1, e2) ->
     let%bind e2_rel = fresh_relation_for relation e2 in
-    let%bind flg = process_expr ~output st (to_cont e2_rel) e1 in
-    (* otherwise we have dead code *)
-    (assert flg);
+    let%bind _ = process_expr ~output st (to_cont e2_rel) e1 in
     process_expr (e2_rel,tyenv) ~output continuation e2
 
   | Assign (lhs,IInt i,k) ->

src/lexer.mll

@@ -31,6 +31,7 @@ rule read =
   | "()" { UNIT }
   | int { let i = int_of_string @@ Lexing.lexeme lexbuf in LabelManager._internal_incr i; INT i }
   | "ifnull" { IFNULL }
+  | "ifptr" {IFPTR}
   | "if" { IF }
   | "then" { THEN }
   | "else" { ELSE }

src/log.ml

@@ -3,8 +3,16 @@ type log_filter =
   | All
   | Subset of Std.StringSet.t
 
-let sources = ref None
+  type log_level = Level of int
+let level_debug = Level 0
+and level_warn = Level 1
+and level_none = Level 2
+
+let level = ref level_none
+
+let set_level lvl = level := lvl
 
+let sources = ref None
 let all () = sources := All
 let disable () = sources := None
 let filter d =
@@ -18,19 +26,33 @@ let check_source w =
   | None, Subset _ -> false
 
 let debug ?src fmt =
-  if (check_source src) then
+  let Level lvl = !level in
+  if (check_source src) && lvl <= 0 then
+    match src with
+    | Some w -> Printf.eprintf ("Debug: [%s] " ^^ fmt ^^ "\n%!") w
+    | None -> Printf.eprintf ("Debug: " ^^ fmt ^^ "\n%!")
+  else
+    Printf.ifprintf stderr fmt
+
+let yellow s = "\027[33m " ^^ s ^^ " \027[0m"
+
+let warn ?src fmt = 
+  let Level lvl = !level in
+  if (check_source src) && lvl <= 1 then
     match src with
-    | Some w -> Printf.eprintf ("[%s] " ^^ fmt ^^ "\n%!") w
-    | None -> Printf.eprintf (fmt ^^ "\n%!")
+    | Some w -> Printf.eprintf ((yellow "Warn: [%s]") ^^ fmt ^^ "\n%!") w
+    | None -> Printf.eprintf ((yellow "Warn: ") ^^ fmt ^^ "\n%!")
   else
     Printf.ifprintf stderr fmt
 
 module type LocatedD = sig
   val debug : ('a, out_channel, unit) format -> 'a
+  val warn : ('a, out_channel, unit) format -> 'a
 end
 
 module Located(W : sig val where : string end) : LocatedD = struct
   let debug fmt = debug ~src:W.where fmt
+  let warn fmt = warn ~src:W.where fmt
 end
 
 let located ~where =

src/negative-tests/ifptr/fail.imp

@@ -0,0 +1,20 @@
+f(p,q){
+    if _ then{
+        p := mkref 5;
+    }
+    else {
+        ()
+    }
+}
+
+{
+    let p = mkref (mkref 3) in
+    let q = p in {
+        f(p,q);
+        ifptr *p = *q then { 
+            let pp = *p in
+            let qq = *q in
+            assert(*pp = *qq)
+        } else ()
+    }
+}

src/negative-tests/ifptr/ownership.imp

@@ -0,0 +1,8 @@
+{
+    let x = _ in
+    let p = mkref x in
+    let q = mkref x in
+    ifptr p = q then {
+        assert(*p = *q)
+    } else ()
+}

src/ownershipInference.ml

@@ -590,8 +590,7 @@ let rec process_expr ~output ((e_id,_),expr) =
     >> return `Return
   | Unit -> return `Cont
   | Seq (e1,e2) ->
-    let%bind stat = process_expr ~output e1 in
-    assert (stat <> `Return);
+    let%bind _ = process_expr ~output e1 in
     process_expr ~output e2
   | NCond (v,e1,e2) ->
     process_conditional ~e_id ~tr_branch:(

src/parser.mly

@@ -15,7 +15,7 @@
 %token NULL
 %token TRUE FALSE
 // conditionals
-%token IF THEN ELSE IFNULL
+%token IF THEN ELSE IFNULL IFPTR
 // control flow
 %token RETURN FAIL
 // bindings
@@ -86,6 +86,16 @@ let expr :=
   | IFNULL; lbl = expr_label; id = ID; THEN; thenc = expr; ELSE; elsec = expr; {
 		NCond ((lbl,$startpos),id,thenc,elsec)
 	  }
+  | IFPTR; lbl = expr_label; (a,b) = pcond_expr; THEN; thenc = expr; ELSE; elsec = expr; {
+    Cond ((lbl, $startpos), `Nondet,
+     Seq ($startpos, Seq ($startpos, 
+      Alias ((LabelManager._internal_fresh (), $startpos), a,b), 
+      thenc), 
+      Alias ((LabelManager._internal_fresh (), $startpos), a,b)
+      ),
+     elsec
+    )
+  }
   | lbl = pre_label; x = ID; ASSIGN; y = lhs; {
 		Assign((lbl,$startpos),x,y)
 	  }
@@ -152,6 +162,9 @@ let cond_expr :=
   | f = fn_call; { `Call f }
   | UNDERSCORE; { `Nondet }
 
+let pcond_expr := 
+  | a = ap; EQ; b = ap; { (a,b) }
+
 let bin_op :=
   | o1 = op; op_name = operator; o2 = op; <`BinOp>
 

src/positive-tests/ifptr/array.imp

@@ -0,0 +1,11 @@
+{
+  let y = mkarray 4 in {
+      y[0] <- 5;
+      let x = mkref y[0] in
+      let z = x in {
+          ifptr z = x then {
+              assert(*z = y[0])
+          } else ()
+      }
+  }
+}

src/positive-tests/ifptr/basic.imp

@@ -0,0 +1,20 @@
+f(p,q){
+    if _ then{
+        p := mkref 5;
+    }
+    else {
+        ()
+    }
+}
+
+{
+    let p = mkref (mkref 3) in
+    let q = p in {
+        f(p,q);
+        ifptr p = q then { 
+            let pp = *p in
+            let qq = *q in
+            assert(*pp = *qq)
+        } else ()
+    }
+}

src/positive-tests/ifptr/recursive.imp

@@ -0,0 +1,23 @@
+f(x){
+    if *x < 1 then 0 else {
+        x := *x - 1;
+        *x + f(x)
+    }
+}
+
+
+{
+    let x = mkref 5 in
+    let y = x in
+    let z = f(y) in {
+        ifptr x = y then {
+            assert(*x = 0);
+        } else {
+            // if we set the code as:
+            // assert(*x = 5)
+            // this should also be safe, but it won't pass because we don't know that alias(x != y) here.
+            // (If ifptr is implemented properly, ignore this)
+            assert(z = 10)
+        }
+    }
+}

src/positive-tests/ifptr/unknown_val.imp

@@ -0,0 +1,9 @@
+f(x) *x
+
+{
+    let x = _ in
+    let p = mkref x in
+    let q = p in {
+        ifptr p = q then assert(f(p) = f(q)) else ()
+    }
+}

src/regnant/.travis-ci.sh

@@ -11,4 +11,5 @@ if [[ ! -d $HOME/jdk8/jdk8u232-b09 ]]; then
         tar xf /tmp/jdk.tar.gz -C $HOME/jdk8;
 fi
 
-python $THIS_DIR/integration-test.py $HOME/jdk8/jdk8u232-b09
+pip3 install PyYaml
+python3 $THIS_DIR/integration-test.py $HOME/jdk8/jdk8u232-b09