verigraph/src/it/polito/verigraph/mcnet/netobjs/EndHost.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 import com.microsoft.z3.BoolExpr;
  14 import com.microsoft.z3.Context;
  15 import com.microsoft.z3.DatatypeExpr;
  16 import com.microsoft.z3.Expr;
  17 import com.microsoft.z3.IntExpr;
  18 import com.microsoft.z3.Solver;
  19 import it.polito.verigraph.mcnet.components.NetContext;
  20 import it.polito.verigraph.mcnet.components.Network;
  21 import it.polito.verigraph.mcnet.components.NetworkObject;
  22 /**
  23  * End host network objects
  24  *
  25  *
  26  */
  27 public class EndHost extends NetworkObject{
  28
  29     List<BoolExpr> constraints;
  30     Context ctx;
  31     DatatypeExpr node;
  32     Network net;
  33     NetContext nctx;
  34
  35     public EndHost(Context ctx, Object[]... args) {
  36         super(ctx, args);
  37     }
  38
  39     @Override
  40     protected void init(Context ctx, Object[]... args) {
  41         this.ctx = ctx;
  42         isEndHost=true;
  43         constraints = new ArrayList<BoolExpr>();
  44         z3Node = ((NetworkObject)args[0][0]).getZ3Node();
  45         node = z3Node;
  46         net = (Network)args[0][1];
  47         nctx = (NetContext)args[0][2];
  48         endHostRules();
  49     }
  50
  51     @Override
  52     public DatatypeExpr getZ3Node() {
  53         return node;
  54     }
  55
  56     @Override
  57     protected void addConstraints(Solver solver) {
  58         BoolExpr[] constr = new BoolExpr[constraints.size()];
  59         solver.add(constraints.toArray(constr));
  60     }
  61
  62     public void endHostRules (){
  63         Expr n_0 = ctx.mkConst("eh_"+node+"_n_0", nctx.node);
  64         IntExpr t_0 = ctx.mkIntConst("eh_"+node+"_t_0");
  65         Expr p_0 = ctx.mkConst("eh_"+node+"_p_0", nctx.packet);
  66
  67         //Constraint1send(node, n_0, p, t_0) -> nodeHasAddr(node,p.src)
  68         constraints.add(
  69                 ctx.mkForall(new Expr[]{n_0, p_0, t_0},
  70                         ctx.mkImplies(
  71                                 (BoolExpr)nctx.send.apply(new Expr[]{ node, n_0, p_0, t_0}),
  72                                 (BoolExpr)nctx.nodeHasAddr.apply(new Expr[]{node, nctx.pf.get("src").apply(p_0)})),1,null,null,null,null));
  73         //Constraint2send(node, n_0, p, t_0) -> p.origin == node
  74         constraints.add(
  75                 ctx.mkForall(new Expr[]{n_0, p_0, t_0},
  76                         ctx.mkImplies(
  77                                 (BoolExpr)nctx.send.apply(new Expr[]{ node, n_0, p_0, t_0}),
  78                                 ctx.mkEq(nctx.pf.get("origin").apply(p_0),node)),1,null,null,null,null));
  79         //Constraint3      send(node, n_0, p, t_0) -> p.orig_body == p.body
  80         constraints.add(
  81                 ctx.mkForall(new Expr[]{n_0, p_0, t_0},
  82                         ctx.mkImplies(
  83                                 (BoolExpr)nctx.send.apply(new Expr[]{ node, n_0, p_0, t_0}),
  84                                 ctx.mkEq(nctx.pf.get("orig_body").apply(p_0),nctx.pf.get("body").apply(p_0))),1,null,null,null,null));
  85         //Constraint4recv(n_0, node, p, t_0) -> nodeHasAddr(node,p.dest)
  86         constraints.add(
  87                 ctx.mkForall(new Expr[]{n_0, p_0, t_0},
  88                         ctx.mkImplies(
  89                                 (BoolExpr)nctx.recv.apply(new Expr[]{ n_0, node, p_0, t_0}),
  90                                 (BoolExpr)nctx.nodeHasAddr.apply(new Expr[]{node, nctx.pf.get("dest").apply(p_0)})),1,null,null,null,null));
  91
  92         //       Just a try: here we state that an endhost is not able to issue a HTTP response traffic
  93         //       See PolitoCache.py model for constants definition (2 means HTTP_RESPONSE, 1 means HTTP_REQUEST)
  94         //         constraints.add(ctx.mkForall(new Expr[]{n_0, p_0, t_0},
  95         //                 ctx.mkImplies((BoolExpr)nctx.send.apply(node, n_0, p_0, t_0),
  96         //                            ctx.mkEq(nctx.pf.get("proto").apply(p_0), ctx.mkInt(1))),1,null,null,null,null));
  97     }
  98 }