verigraph/service/src/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
  10 package mcnet.netobjs;
  11
  12
  13 import java.util.ArrayList;
  14 import java.util.List;
  15
  16 import com.microsoft.z3.BoolExpr;
  17 import com.microsoft.z3.Context;
  18 import com.microsoft.z3.DatatypeExpr;
  19 import com.microsoft.z3.Expr;
  20 import com.microsoft.z3.FuncDecl;
  21 import com.microsoft.z3.IntExpr;
  22 import com.microsoft.z3.Solver;
  23 import com.microsoft.z3.Sort;
  24
  25 import mcnet.components.NetContext;
  26 import mcnet.components.Network;
  27 import mcnet.components.NetworkObject;
  28 /**Cache Model
  29  *
  30  */
  31 public class PolitoCache extends NetworkObject{
  32
  33                 List<BoolExpr> constraints;
  34                 Context ctx;
  35                 DatatypeExpr politoCache;
  36                 Network net;
  37                 NetContext nctx;
  38                 FuncDecl isInBlacklist;
  39
  40                 public PolitoCache(Context ctx, Object[]... args) {
  41                         super(ctx, args);
  42                 }
  43
  44                 @Override
  45                 protected void init(Context ctx, Object[]... args) {
  46                         this.ctx = ctx;
  47                         isEndHost=false;
  48                         constraints = new ArrayList<BoolExpr>();
  49                 z3Node = ((NetworkObject)args[0][0]).getZ3Node();
  50                 politoCache = z3Node;
  51                 net = (Network)args[0][1];
  52                 nctx = (NetContext)args[0][2];
  53                 //net.saneSend(this);
  54             }
  55
  56                 @Override
  57                 public DatatypeExpr getZ3Node() {
  58                         return politoCache;
  59                 }
  60
  61                 @Override
  62                 protected void addConstraints(Solver solver) {
  63                                 BoolExpr[] constr = new BoolExpr[constraints.size()];
  64                             solver.add(constraints.toArray(constr));
  65                 }
  66
  67             public void installCache (NetworkObject[] internalNodes){
  68                 Expr n_0 = ctx.mkConst("politoCache_"+politoCache+"_n_0", nctx.node);
  69                 Expr n_1 = ctx.mkConst("politoCache_"+politoCache+"_n_1", nctx.node);
  70                 Expr n_2 = ctx.mkConst("politoCache_"+politoCache+"_n_2", nctx.node);
  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 }