Merge "update verigraph"

1 files changed, 0 insertions, 363 deletions

diff --git a/verigraph/service/src/mcnet/components/Checker.java b/verigraph/service/src/mcnet/components/Checker.java
deleted file mode 100644
index 3c13d28..0000000
--- a/verigraph/service/src/mcnet/components/Checker.java
+++ /dev/null
@@ -1,363 +0,0 @@
-/*******************************************************************************
- * Copyright (c) 2017 Politecnico di Torino and others.
- *
- * All rights reserved. This program and the accompanying materials
- * are made available under the terms of the Apache License, Version 2.0
- * which accompanies this distribution, and is available at
- * http://www.apache.org/licenses/LICENSE-2.0
- *******************************************************************************/
-
-package mcnet.components;
-
-
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.List;
-
-import com.microsoft.z3.BoolExpr;
-import com.microsoft.z3.Context;
-import com.microsoft.z3.Expr;
-import com.microsoft.z3.IntExpr;
-import com.microsoft.z3.Model;
-import com.microsoft.z3.Solver;
-import com.microsoft.z3.Status;
-
-/**Various checks for specific properties in the network.
- *
- */
-public class Checker {
-
-	Context ctx;
-	Network net;
-	NetContext nctx;
-	Solver solver;
-	ArrayList<BoolExpr> constraints;
-	public BoolExpr [] assertions;
-	public Status result;
-	public Model model;
-
-
-   public Checker(Context context,NetContext nctx,Network network){
-        this.ctx = context;
-        this.net = network;
-        this.nctx = nctx;
-        this.solver = ctx.mkSolver();
-        this.constraints = new ArrayList<BoolExpr>();
-   }
-
-   /**Resets the constraints
-    *
-    */
-    public void clearState (){
-        this.solver.reset();
-        this.constraints = new ArrayList<BoolExpr>();
-    }
-
-	/**Checks whether the source provided can reach the destination
-	 *
-	 * @param src
-	 * @param dest
-	 * @return
-	 */
-	public IsolationResult checkIsolationProperty (NetworkObject src, NetworkObject dest){
-		assert(net.elements.contains(src));
-	    assert(net.elements.contains(dest));
-	    solver.push ();
-	    addConstraints();
-
-	    Expr p0 = ctx.mkConst("check_isolation_p0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
-	    Expr p1 = ctx.mkConst("check_isolation_p1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
-	    Expr n_0 =ctx.mkConst("check_isolation_n_0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
-	    Expr n_1 =ctx.mkConst("check_isolation_n_1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
-	    IntExpr t_0 = ctx.mkIntConst("check_isolation_t0_"+src.getZ3Node()+"_"+dest.getZ3Node());
-	    IntExpr t_1 = ctx.mkIntConst("check_isolation_t1_"+src.getZ3Node()+"_"+dest.getZ3Node());
-
-	//	        Constraint1		recv(n_0,destNode,p0,t_0)
-	    this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p0, t_0));
-
-	//	        Constraint2		send(srcNode,n_1,p1,t_1)
-	    this.solver.add((BoolExpr)nctx.send.apply(src.getZ3Node(), n_1, p1, t_1));
-
-	//	        Constraint3		nodeHasAddr(srcNode,p1.srcAddr)
-	    this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(src.getZ3Node(), nctx.pf.get("src").apply(p1)));
-
-	//	        Constraint4		p1.origin == srcNode
-	    this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p1), src.getZ3Node()));
-
-	//	        Constraint5		nodeHasAddr(destNode,p1.destAddr)
-	    this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(dest.getZ3Node(), nctx.pf.get("dest").apply(p1)));
-
-		//NON sembrano necessari
-		//         this.solver.add(z3.Or(this.ctx.nodeHasAddr(src.getZ3Node(), this.ctx.packet.src(p0)),\
-		//                               this.ctx.nodeHasAddr(n_0, this.ctx.packet.src(p0)),\
-		//                               this.ctx.nodeHasAddr(n_1, this.ctx.packet.src(p0))))
-		//this.solver.add(this.ctx.packet.dest(p1) == this.ctx.packet.dest(p0))
-
-	//	        Constraint6		p1.origin ==  p0.origin
-	    this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p1),nctx.pf.get("origin").apply(p0)));
-
-	//	        Constraint7		nodeHasAddr(destNode, p0.destAddr)
-	    this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(dest.getZ3Node(), nctx.pf.get("dest").apply(p0)));
-
-	    result = this.solver.check();
-	    model = null;
-	    assertions = this.solver.getAssertions();
-	    if (result == Status.SATISFIABLE){
-	    	model = this.solver.getModel();
-	    }
-	    this.solver.pop();
-	    return new IsolationResult(ctx,result, p0, n_0, t_1, t_0, nctx, assertions, model);
-	}
-
-
-
-	public IsolationResult CheckIsolationFlowProperty (NetworkObject src, NetworkObject dest){
-		assert(net.elements.contains(src));
-	    assert(net.elements.contains(dest));
-	    solver.push ();
-	    addConstraints();
-
-	    Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
-	    Expr n_0 =ctx.mkConst("check_isolation_n_0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
-	    Expr n_1 =ctx.mkConst("check_isolation_n_1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
-	    Expr n_2 =ctx.mkConst("check_isolation_n_1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
-
-	    IntExpr t_0 = ctx.mkIntConst("check_isolation_t0_"+src.getZ3Node()+"_"+dest.getZ3Node());
-	    IntExpr t_1 = ctx.mkIntConst("check_isolation_t1_"+src.getZ3Node()+"_"+dest.getZ3Node());
-	    IntExpr t_2 = ctx.mkIntConst("check_isolation_t2_"+src.getZ3Node()+"_"+dest.getZ3Node());
-
-	//	        Constraint1		recv(n_0,destNode,p,t_0)
-	    this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t_0));
-
-	//	        Constraint2		send(srcNode,n_1,p1,t_1)
-	    this.solver.add((BoolExpr)nctx.send.apply(src.getZ3Node(), n_1, p, t_1));
-
-	//	        Constraint3		nodeHasAddr(srcNode,p.srcAddr)
-	    this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(src.getZ3Node(), nctx.pf.get("src").apply(p)));
-
-	//	        Constraint4		p.origin == srcNode
-	    this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
-
-
-	    Expr p_2 = ctx.mkConst("check_isolation_p_flow_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
-
-	    //	    Constraint5		there does not exist p_2, n_2, t_2 :
-							//	    		 send(destNode,n_2,p_2,t_2) &&
-							//	    	     p_2.srcAddr == p. destAddr &&
-							//	    	     p_2.srcPort == p.destPort &&
-							//	    	     p_2.destPort == p.srcPort &&
-							//	    	     p_2.destt == p.src &&
-							//	    	     t_2 < t_0
-	    this.solver.add(ctx.mkNot(ctx.mkExists(new Expr[]{p_2,n_2,t_2},
-	    				ctx.mkAnd(
-	    						(BoolExpr)nctx.send.apply(dest.getZ3Node(), n_2, p_2, t_2),
-	    						ctx.mkEq(nctx.pf.get("src").apply(p_2), nctx.pf.get("dest").apply(p)),
-	    						ctx.mkEq(nctx.pf.get("src_port").apply(p_2), nctx.pf.get("dest_port").apply(p)),
-	    						ctx.mkEq(nctx.pf.get("dest_port").apply(p_2), nctx.pf.get("src_port").apply(p)),
-	    						ctx.mkEq(nctx.pf.get("dest").apply(p_2), nctx.pf.get("src").apply(p)),
-	    						ctx.mkLt(t_2,t_0)),1,null,null,null,null)));
-
-
-	    result = this.solver.check();
-	    model = null;
-	    assertions = this.solver.getAssertions();
-	    if (result == Status.SATISFIABLE){
-	    	model = this.solver.getModel();
-	    }
-	    this.solver.pop();
-	    return new IsolationResult(ctx,result, p, n_0, t_1, t_0, nctx, assertions, model);
-	}
-
-
-
-    public IsolationResult CheckNodeTraversalProperty (NetworkObject src, NetworkObject dest, NetworkObject node){
-		assert(net.elements.contains(src));
-	    assert(net.elements.contains(dest));
-	    solver.push ();
-	    addConstraints();
-
-	    Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
-
-	    Expr n_0 =ctx.mkConst("check_isolation_n_0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
-	    Expr n_1 =ctx.mkConst("check_isolation_n_1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
-	    Expr n_2 =ctx.mkConst("check_isolation_n_1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
-
-	    IntExpr t_0 = ctx.mkIntConst("check_isolation_t0_"+src.getZ3Node()+"_"+dest.getZ3Node());
-	    IntExpr t_1 = ctx.mkIntConst("check_isolation_t1_"+src.getZ3Node()+"_"+dest.getZ3Node());
-	    IntExpr t_2 = ctx.mkIntConst("check_isolation_t2_"+src.getZ3Node()+"_"+dest.getZ3Node());
-
-	//	        Constraint1		recv(n_0,destNode,p,t_0)
-	    this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t_0));
-
-	//	        Constraint2		send(srcNode,n_1,p1,t_1)
-	    this.solver.add((BoolExpr)nctx.send.apply(src.getZ3Node(), n_1, p, t_1));
-
-	//	        Constraint3		nodeHasAddr(srcNode,p.srcAddr)
-	    this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(src.getZ3Node(), nctx.pf.get("src").apply(p)));
-
-	//	        Constraint4		p.origin == srcNode
-	    this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
-
-
-	//			Constraint5		there does not exist n_2, t_2 : recv(n_2,node,p,t_2) && t_2 < t_0
-	    this.solver.add(ctx.mkNot(ctx.mkExists(new Expr[]{n_2,t_2},
-	    				ctx.mkAnd(
-	    						(BoolExpr)nctx.recv.apply(n_2, node.getZ3Node(), p, t_2),
-	    						ctx.mkLt(t_2,t_0)),1,null,null,null,null)));
-
-	//			Constraint 6	there does not exist n_2, t_2 : send(node,n_2,p,t_2) && t_2 < t_0
-	    this.solver.add(ctx.mkNot(ctx.mkExists(new Expr[]{n_2,t_2},
-				ctx.mkAnd(
-						(BoolExpr)nctx.send.apply(node.getZ3Node(), n_2, p, t_2),
-						ctx.mkLt(t_2,t_0)),1,null,null,null,null)));
-
-
-	    result = this.solver.check();
-	    model = null;
-	    assertions = this.solver.getAssertions();
-	    if (result == Status.SATISFIABLE){
-	    	model = this.solver.getModel();
-	    }
-	    this.solver.pop();
-	    return new IsolationResult(ctx,result, p, n_0, t_1, t_0, nctx, assertions, model);
-    	
-    }
-
-    public IsolationResult CheckLinkTraversalProperty (NetworkObject src, NetworkObject dest, NetworkObject le0, NetworkObject le1){
-		assert(net.elements.contains(src));
-	    assert(net.elements.contains(dest));
-	    solver.push ();
-	    addConstraints();
-
-	    Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
-
-	    Expr n_0 =ctx.mkConst("check_isolation_n_0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
-	    Expr n_1 =ctx.mkConst("check_isolation_n_1_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
-
-	    IntExpr t_0 = ctx.mkIntConst("check_isolation_t0_"+src.getZ3Node()+"_"+dest.getZ3Node());
-	    IntExpr t_1 = ctx.mkIntConst("check_isolation_t1_"+src.getZ3Node()+"_"+dest.getZ3Node());
-	    IntExpr t_2 = ctx.mkIntConst("check_isolation_t2_"+src.getZ3Node()+"_"+dest.getZ3Node());
-
-	//	        Constraint1		recv(n_0,destNode,p,t_0)
-	    this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t_0));
-
-	//	        Constraint2		send(srcNode,n_1,p1,t_1)
-	    this.solver.add((BoolExpr)nctx.send.apply(src.getZ3Node(), n_1, p, t_1));
-
-	//	        Constraint3		nodeHasAddr(srcNode,p.srcAddr)
-	    this.solver.add((BoolExpr)nctx.nodeHasAddr.apply(src.getZ3Node(), nctx.pf.get("src").apply(p)));
-
-	//	        Constraint4		p.origin == srcNode
-	    this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
-
-	//			Constraint5		∃ t_1, t_2 :
-	    					//	    send(linkNode0,linkNode1,p,t_1) &&
-							//	    recv(linkNode0,linkNode1,p,t_2) &&
-							//	    t_1 < t_0 &&
-							//	    t_2 < t_0
-	    this.solver.add(ctx.mkExists(new Expr[]{t_1,t_2},
-	    				ctx.mkAnd(
-	    						(BoolExpr)nctx.send.apply(le0.getZ3Node(), le1.getZ3Node(), p, t_1),
-	    						(BoolExpr)nctx.recv.apply(le0.getZ3Node(), le1.getZ3Node(), p, t_2),
-	    						ctx.mkLt(t_1,t_0),
-	    						ctx.mkLt(t_2,t_0)),1,null,null,null,null));
-
-
-	    result = this.solver.check();
-	    model = null;
-	    assertions = this.solver.getAssertions();
-	    if (result == Status.SATISFIABLE){
-	    	model = this.solver.getModel();
-	    }
-	    this.solver.pop();
-	    return new IsolationResult(ctx,result, p, n_0, t_1, t_0, nctx, assertions, model);
-
-    }
-
-   public Result CheckDataIsolationPropertyCore (NetworkObject src, NetworkObject dest){
-	   	assert(net.elements.contains(src));
-	    assert(net.elements.contains(dest));
-	    List<BoolExpr> constr = this.getConstraints();
-	    Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
-
-	    Expr n_0 =ctx.mkConst("check_isolation_n_0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
-	    IntExpr t = ctx.mkIntConst("check_isolation_t_"+src.getZ3Node()+"_"+dest.getZ3Node());
-
-	//	        Constraint1		recv(n_0,destNode,p,t)
-	    constr.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t));
-
-	//	        Constraint2		p.origin == srcNode
-	    this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
-
-	    this.solver.push();
-
-    //     	   Constraint3		for each constraint( n -> constraint)
-	    ArrayList<BoolExpr> names =new ArrayList<BoolExpr>();
-	    for(BoolExpr con : constr){
-	    	BoolExpr n = ctx.mkBoolConst(""+con);
-	    	names.add(n);
-	    	this.solver.add(ctx.mkImplies(n, con));
-	    }
-
-	    BoolExpr[] nam = new BoolExpr[names.size()];
-	    result = this.solver.check(names.toArray(nam));
-	    Result ret =null;
-
-	    if (result == Status.SATISFIABLE){
-	    	System.out.println("SAT");
-	    	ret = new Result(ctx,this.solver.getModel());
-	    }else if(result == Status.UNSATISFIABLE){
-	    	System.out.println("unsat");
-	    	ret = new Result(ctx,this.solver.getUnsatCore());
-	    }
-	    this.solver.pop();
-	    return ret;
-   }
-
-    public DataIsolationResult CheckDataIsolationProperty(NetworkObject src, NetworkObject dest){
-    	assert(net.elements.contains(src));
-	    assert(net.elements.contains(dest));
-	    solver.push ();
-	    addConstraints();
-
-	    Expr p = ctx.mkConst("check_isolation_p_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.packet);
-
-	    Expr n_0 =ctx.mkConst("check_isolation_n_0_"+src.getZ3Node()+"_"+dest.getZ3Node(), nctx.node);
-	    IntExpr t = ctx.mkIntConst("check_isolation_t_"+src.getZ3Node()+"_"+dest.getZ3Node());
-
-	//	        Constraint1		recv(n_0,destNode,p,t)
-	    this.solver.add((BoolExpr)nctx.recv.apply(n_0, dest.getZ3Node(), p, t));
-
-	//	        Constraint2		p.origin == srcNode
-	    this.solver.add(ctx.mkEq(nctx.pf.get("origin").apply(p), src.getZ3Node()));
-
-	    result = this.solver.check();
-	    model = null;
-	    assertions = this.solver.getAssertions();
-	    if (result == Status.SATISFIABLE){
-	    	model = this.solver.getModel();
-	    }
-	    this.solver.pop();
-	    return new DataIsolationResult(ctx,result, p, n_0, t, nctx, assertions, model);
-    }
-
-
-
-
-	public void addConstraints(){
-	    nctx.addConstraints(solver);
-	    net.addConstraints(solver);
-	    for (NetworkObject el : net.elements)
-	        el.addConstraints(solver);
-	}
-
-
-	 public List<BoolExpr> getConstraints(){
-	        Solver l = ctx.mkSolver();
-	        nctx.addConstraints(l);
-	        net.addConstraints(l);
-	        for (NetworkObject el : net.elements)
-	            el.addConstraints(l);
-	        return Arrays.asList(l.getAssertions());
-	}
-}