verigraph/src/it/polito/verigraph/mcnet/netobjs/PolitoCache.java

   1 /*******************************************************************************
   2  * Copyright (c) 2017 Politecnico di Torino and others.
   3  *
   4  * All rights reserved. This program and the accompanying materials
   5  * are made available under the terms of the Apache License, Version 2.0
   6  * which accompanies this distribution, and is available at
   7  * http://www.apache.org/licenses/LICENSE-2.0
   8  *******************************************************************************/
   9 package it.polito.verigraph.mcnet.netobjs;
  10
  11 import java.util.ArrayList;
  12 import java.util.List;
  13
  14 import com.microsoft.z3.BoolExpr;
  15 import com.microsoft.z3.Context;
  16 import com.microsoft.z3.DatatypeExpr;
  17 import com.microsoft.z3.Expr;
  18 import com.microsoft.z3.FuncDecl;
  19 import com.microsoft.z3.IntExpr;
  20 import com.microsoft.z3.Solver;
  21 import com.microsoft.z3.Sort;
  22
  23 import it.polito.verigraph.mcnet.components.NetContext;
  24 import it.polito.verigraph.mcnet.components.Network;
  25 import it.polito.verigraph.mcnet.components.NetworkObject;
  26 /**Cache Model
  27  *
  28  *
  29  */
  30 public class PolitoCache extends NetworkObject{
  31
  32     List<BoolExpr> constraints;
  33     Context ctx;
  34     DatatypeExpr politoCache;
  35     Network net;
  36     NetContext nctx;
  37     FuncDecl isInBlacklist;
  38
  39     public PolitoCache(Context ctx, Object[]... args) {
  40         super(ctx, args);
  41     }
  42
  43     @Override
  44     protected void init(Context ctx, Object[]... args) {
  45         this.ctx = ctx;
  46         isEndHost=false;
  47         constraints = new ArrayList<BoolExpr>();
  48         z3Node = ((NetworkObject)args[0][0]).getZ3Node();
  49         politoCache = z3Node;
  50         net = (Network)args[0][1];
  51         nctx = (NetContext)args[0][2];
  52         //net.saneSend(this);
  53     }
  54
  55     @Override
  56     public DatatypeExpr getZ3Node() {
  57         return politoCache;
  58     }
  59
  60     @Override
  61     protected void addConstraints(Solver solver) {
  62         BoolExpr[] constr = new BoolExpr[constraints.size()];
  63         solver.add(constraints.toArray(constr));
  64     }
  65
  66     public void installCache (NetworkObject[] internalNodes){
  67         Expr n_0 = ctx.mkConst("politoCache_"+politoCache+"_n_0", nctx.node);
  68         Expr n_1 = ctx.mkConst("politoCache_"+politoCache+"_n_1", nctx.node);
  69         Expr n_2 = ctx.mkConst("politoCache_"+politoCache+"_n_2", nctx.node);
  70
  71         Expr p_0 = ctx.mkConst("politoCache_"+politoCache+"_p_0", nctx.packet);
  72         Expr p_1 = ctx.mkConst("politoCache_"+politoCache+"_p_1", nctx.packet);
  73         Expr p_2 = ctx.mkConst("politoCache_"+politoCache+"_p_2", nctx.packet);
  74
  75         IntExpr t_0 = ctx.mkIntConst("politoCache_"+politoCache+"_t_0");
  76         IntExpr t_1 = ctx.mkIntConst("politoCache_"+politoCache+"_t_1");
  77         IntExpr t_2 = ctx.mkIntConst("politoCache_"+politoCache+"_t_2");
  78
  79         Expr a_0 = ctx.mkConst(politoCache+"politoCache_a_0", nctx.node);
  80         IntExpr u_0 = ctx.mkIntConst("politoCache_"+politoCache+"_u_0");
  81
  82         FuncDecl isInternalNode = ctx.mkFuncDecl(politoCache+"_isInternalNode", nctx.node, ctx.mkBoolSort());
  83         FuncDecl isInCache = ctx.mkFuncDecl(politoCache+"_isInCache", new Sort[]{ctx.mkIntSort(),ctx.mkIntSort()}, ctx.mkBoolSort());
  84
  85         assert(internalNodes.length!=0); //No internal nodes => Should never happen
  86
  87         //Modeling the behavior of the isInternalNode() and isInCache() functions
  88         BoolExpr[] internalNodesConstraint = new BoolExpr[internalNodes.length];
  89         for(int w=0;w<internalNodesConstraint.length;w++)
  90             internalNodesConstraint[w]= (ctx.mkEq(a_0,internalNodes[w].getZ3Node()));
  91
  92         //Constraint1 if(isInternalNode(a_0) == or(listadeinodiinterni) ? True : false
  93         constraints.add(
  94                 ctx.mkForall(new Expr[]{a_0},
  95                         ctx.mkIff((BoolExpr)isInternalNode.apply(a_0), ctx.mkOr(internalNodesConstraint)),1,null,null,null,null));
  96
  97         //    constraints.add(ctx.mkForall(new Expr[]{a_0}, ctx.mkEq(isInternalNode.apply(a_0),ctx.mkOr(internalNodesConstraint)),1,null,null,null,null));
  98
  99         //    constraints.add(ctx.mkForall(new Expr[]{u_0, t_0},
 100         //                     ctx.mkITE(ctx.mkExists(new Expr[]{t_1, t_2, p_1, p_2, n_1, n_2},
 101         //                        ctx.mkAnd(ctx.mkLt(t_1, t_2),
 102         //                                ctx.mkLt(t_1, t_0),
 103         //                                ctx.mkLt(t_2, t_0),
 104         //                                (BoolExpr)nctx.recv.apply(n_1, politoCache, p_1, t_1),
 105         //                                (BoolExpr)nctx.recv.apply(n_2, politoCache, p_2, t_2),
 106         //                                ctx.mkEq(nctx.pf.get("proto").apply(p_1),ctx.mkInt(nctx.HTTP_REQUEST)),
 107         //                                ctx.mkEq(nctx.pf.get("proto").apply(p_2),ctx.mkInt(nctx.HTTP_RESPONSE)),
 108         //                                (BoolExpr)isInternalNode.apply(n_1),
 109         //                                ctx.mkNot((BoolExpr)isInternalNode.apply(n_2)),
 110         //                                ctx.mkEq(nctx.pf.get("url").apply(p_1),u_0),
 111         //                                ctx.mkEq(nctx.pf.get("url").apply(p_2),u_0)),1,null,null,null,null),
 112         //                     ctx.mkEq(isInCache.apply(u_0,t_0),ctx.mkBool(true)),ctx.mkEq(isInCache.apply(u_0,t_0),ctx.mkBool(false))),1,null,null,null,null));
 113         //
 114
 115         //Constraint2 isInCache(u_0,t_0), exist t_1, t_2, p_1, p_2, n_1, n_2 :
 116         //    (   t_1< t_2 < t_0 && recv(n_1, politoCache, p_1, t_1) && recv(n_2, politoCache, p_2, t_2))) &&
 117         //        p_1.proto == HTTP_REQ &&  p_2.proto == HTTP_RESP &&
 118         //        isInternalNode(n_1) && !isInternalNode(n_2) &&
 119         //        p_1.url == u_0 &&  p_2.url == u_0 )
 120         constraints.add(
 121                 ctx.mkForall(new Expr[]{u_0, t_0},
 122                         ctx.mkImplies((BoolExpr)isInCache.apply(u_0, t_0),
 123                                 ctx.mkExists(new Expr[]{t_1,t_2,p_1,p_2,n_1, n_2},
 124                                         ctx.mkAnd(
 125                                                 ctx.mkLt(t_1, t_2),
 126                                                 ctx.mkLt(t_1, t_0),
 127                                                 ctx.mkLt(t_2, t_0),
 128                                                 (BoolExpr)nctx.recv.apply(n_1, politoCache, p_1, t_1),
 129                                                 (BoolExpr)nctx.recv.apply(n_2, politoCache, p_2, t_2),
 130                                                 ctx.mkEq(nctx.pf.get("proto").apply(p_1), ctx.mkInt(nctx.HTTP_REQUEST)),
 131                                                 ctx.mkEq(nctx.pf.get("proto").apply(p_2), ctx.mkInt(nctx.HTTP_RESPONSE)),
 132                                                 (BoolExpr)isInternalNode.apply(n_1),
 133                                                 ctx.mkNot((BoolExpr)isInternalNode.apply(n_2)),
 134                                                 ctx.mkEq(nctx.pf.get("url").apply(p_1), u_0),
 135                                                 ctx.mkEq(nctx.pf.get("url").apply(p_2), u_0)),1,null,null,null,null)),1,null,null,null,null));
 136         //    //Always in cache
 137         //    constraints.add(ctx.mkForall(new Expr[]{u_0, t_0},ctx.mkEq(isInCache.apply(u_0,t_0),ctx.mkBool(true)),1,null,null,null,null));
 138
 139         //Constraint3 Modeling the behavior of the cache
 140         //send(politoCache, n_0, p, t_0) && !isInternalNode(n_0) ->
 141         //    (exist t_1,n_1 :
 142         //        (t_1 < t_0 && recv(n_1, politoCache, p, t_1) &&
 143         //         p.proto == HTTP_REQ &&  !isInCache(p.url,t_0))
 144         constraints.add(
 145                 ctx.mkForall(new Expr[]{n_0,p_0, t_0},
 146                         ctx.mkImplies(
 147                                 ctx.mkAnd((BoolExpr)nctx.send.apply(politoCache,n_0,p_0,t_0),ctx.mkNot((BoolExpr)isInternalNode.apply(n_0))),
 148                                 ctx.mkAnd(ctx.mkExists(new Expr[]{t_1, n_1},
 149                                         ctx.mkAnd(
 150                                                 ctx.mkLt(t_1, t_0),
 151                                                 (BoolExpr)isInternalNode.apply(n_1),
 152                                                 (BoolExpr)nctx.recv.apply(n_1, politoCache, p_0, t_1)),1,null,null,null,null),
 153                                         ctx.mkEq(nctx.pf.get("proto").apply(p_0), ctx.mkInt(nctx.HTTP_REQUEST)),
 154                                         ctx.mkNot((BoolExpr)isInCache.apply(nctx.pf.get("url").apply(p_0), t_0)))),1,null,null,null,null));
 155
 156         //Constraint4 send(politoCache, n_0, p, t_0) && isInternalNode(n_0) ->
 157         //    (exist p_1,t_1 :
 158         //        (t_1 < t_0 && recv(n_0, politoCache, p_1, t_1) &&
 159         //         p_1.proto == HTTP_REQ && p.proto == HTTP_RESP &&
 160         //         p_1.url == p.url &&  p.src == p_1.dest && p.dest==p_1.src
 161         //         && isInCache(p.url,t_0))
 162         constraints.add(
 163                 ctx.mkForall(new Expr[]{n_0,p_0, t_0},
 164                         ctx.mkImplies(
 165                                 ctx.mkAnd((BoolExpr)nctx.send.apply(politoCache,n_0,p_0,t_0),(BoolExpr)isInternalNode.apply(n_0)),
 166                                 ctx.mkAnd(ctx.mkExists(new Expr[]{p_1, t_1},
 167                                         ctx.mkAnd(
 168                                                 ctx.mkLt(t_1, t_0),
 169                                                 (BoolExpr)nctx.recv.apply(n_0, politoCache, p_1, t_1),
 170                                                 ctx.mkEq(nctx.pf.get("proto").apply(p_1), ctx.mkInt(nctx.HTTP_REQUEST)),
 171                                                 ctx.mkEq(nctx.pf.get("url").apply(p_1), nctx.pf.get("url").apply(p_0))),1,null,null,null,null),
 172                                         ctx.mkEq(nctx.pf.get("proto").apply(p_0), ctx.mkInt(nctx.HTTP_RESPONSE)),
 173                                         ctx.mkEq(nctx.pf.get("src").apply(p_0), nctx.pf.get("dest").apply(p_1)),
 174                                         ctx.mkEq(nctx.pf.get("dest").apply(p_0), nctx.pf.get("src").apply(p_1)),
 175                                         (BoolExpr)isInCache.apply(nctx.pf.get("url").apply(p_0), t_0))),1,null,null,null,null));
 176     }
 177 }