Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Dependencies of Run #233

Closed
wants to merge 2 commits into from
Closed

Dependencies of Run #233

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0053850
deps of run
jcp19 Oct 30, 2023
7fc510d
Backup
jcp19 Oct 31, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 24 additions & 30 deletions private/underlay/conn/conn.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,29 +44,29 @@ type Messages []ipv4.Message
type Conn interface {
//@ pred Mem()
// (VerifiedSCION) Reads a message to b. Returns the number of read bytes.
//@ preserves Mem()
//@ requires acc(Mem(), _)
//@ preserves slices.AbsSlice_Bytes(b, 0, len(b))
//@ ensures err == nil ==> 0 <= n && n <= len(b)
//@ ensures err == nil ==> acc(addr.Mem(), _)
//@ ensures err != nil ==> err.ErrorMem()
ReadFrom(b []byte) (n int, addr *net.UDPAddr, err error)
//@ preserves Mem()
//@ requires acc(Mem(), _)
//@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> m[i].Mem(1)
//@ ensures err == nil ==> 0 <= n && n <= len(m)
//@ ensures err != nil ==> err.ErrorMem()
ReadBatch(m Messages) (n int, err error)
//@ preserves Mem()
//@ requires acc(Mem(), _)
//@ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R10)
//@ ensures err == nil ==> 0 <= n && n <= len(b)
//@ ensures err != nil ==> err.ErrorMem()
Write(b []byte) (n int, err error)
//@ requires acc(u.Mem(), _)
//@ preserves Mem()
//@ requires acc(Mem(), _)
//@ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R10)
//@ ensures err == nil ==> 0 <= n && n <= len(b)
//@ ensures err != nil ==> err.ErrorMem()
WriteTo(b []byte, u *net.UDPAddr) (n int, err error)
//@ preserves Mem()
//@ requires acc(Mem(), _)
//@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> acc(m[i].Mem(1), R10)
//@ ensures err == nil ==> 0 <= n && n <= len(m)
//@ ensures err != nil ==> err.ErrorMem()
Expand Down Expand Up @@ -163,25 +163,23 @@ func newConnUDPIPv4(listen, remote *net.UDPAddr, cfg *Config) (res *connUDPIPv4,

// ReadBatch reads up to len(msgs) packets, and stores them in msgs.
// It returns the number of packets read, and an error if any.
// @ preserves c.Mem()
// @ requires acc(c.Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1)
// @ ensures errRet == nil ==> 0 <= nRet && nRet <= len(msgs)
// @ ensures errRet != nil ==> errRet.ErrorMem()
func (c *connUDPIPv4) ReadBatch(msgs Messages) (nRet int, errRet error) {
//@ unfold c.Mem()
//@ unfold acc(c.Mem(), _)
// (VerifiedSCION) 1 is the length of the buffers of the messages in msgs
n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE /*@, 1 @*/)
//@ fold c.Mem()
return n, err
}

// @ preserves c.Mem()
// @ requires acc(c.Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(1), R10)
// @ ensures err == nil ==> 0 <= n && n <= len(msgs)
// @ ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv4) WriteBatch(msgs Messages, flags int) (n int, err error) {
//@ unfold c.Mem()
//@ defer fold c.Mem()
//@ unfold acc(c.Mem(), _)
// (VerifiedSCION) 1 is the length of the buffers of the messages in msgs
return c.pconn.WriteBatch(msgs, flags /*@, 1 @*/)
}
Expand Down Expand Up @@ -239,25 +237,23 @@ func newConnUDPIPv6(listen, remote *net.UDPAddr, cfg *Config) (res *connUDPIPv6,

// ReadBatch reads up to len(msgs) packets, and stores them in msgs.
// It returns the number of packets read, and an error if any.
// @ preserves c.Mem()
// @ requires acc(c.Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1)
// @ ensures errRet == nil ==> 0 <= nRet && nRet <= len(msgs)
// @ ensures errRet != nil ==> errRet.ErrorMem()
func (c *connUDPIPv6) ReadBatch(msgs Messages) (nRet int, errRet error) {
//@ unfold c.Mem()
//@ unfold acc(c.Mem(), _)
// (VerifiedSCION) 1 is the length of the buffers of the messages in msgs
n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE /*@, 1 @*/)
//@ fold c.Mem()
return n, err
}

// @ preserves c.Mem()
// @ requires acc(c.Mem(), _)
// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(1), R10)
// @ ensures err == nil ==> 0 <= n && n <= len(msgs)
// @ ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv6) WriteBatch(msgs Messages, flags int) (n int, err error) {
//@ unfold c.Mem()
//@ defer fold c.Mem()
//@ unfold acc(c.Mem(), _)
// (VerifiedSCION) 1 is the length of the buffers of the messages in msgs
return c.pconn.WriteBatch(msgs, flags /*@, 1 @*/)
}
Expand Down Expand Up @@ -398,38 +394,36 @@ func (cc *connUDPBase) initConnUDP(network string, laddr, raddr *net.UDPAddr, cf
return nil
}

// @ preserves c.Mem()
// @ preserves acc(c.Mem(), _)
// @ preserves slices.AbsSlice_Bytes(b, 0, len(b))
// @ preserves unfolding c.Mem() in c.conn == underlyingConn
// @ preserves unfolding acc(c.Mem(), _) in c.conn == underlyingConn
// @ ensures err == nil ==> 0 <= n && n <= len(b)
// @ ensures err == nil ==> acc(addr.Mem(), _)
// @ ensures err != nil ==> err.ErrorMem()
func (c *connUDPBase) ReadFrom(b []byte /*@, ghost underlyingConn *net.UDPConn @*/) (n int, addr *net.UDPAddr, err error) {
//@ unfold c.Mem()
//@ defer fold c.Mem()
//@ unfold acc(c.Mem(), _)
return c.conn.ReadFromUDP(b)
}

// @ preserves c.Mem()

// @ preserves acc(c.Mem(), _)
// @ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15)
// @ preserves unfolding c.Mem() in c.conn == underlyingConn
// @ preserves unfolding acc(c.Mem(), _) in c.conn == underlyingConn
// @ ensures err == nil ==> 0 <= n && n <= len(b)
// @ ensures err != nil ==> err.ErrorMem()
func (c *connUDPBase) Write(b []byte /*@, ghost underlyingConn *net.UDPConn @*/) (n int, err error) {
//@ unfold c.Mem()
//@ defer fold c.Mem()
//@ unfold acc(c.Mem(), _)
return c.conn.Write(b)
}

// @ requires acc(dst.Mem(), _)
// @ preserves c.Mem()
// @ preserves unfolding c.Mem() in c.conn == underlyingConn
// @ preserves acc(c.Mem(), _)
// @ preserves unfolding acc(c.Mem(), _) in c.conn == underlyingConn
// @ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15)
// @ ensures err == nil ==> 0 <= n && n <= len(b)
// @ ensures err != nil ==> err.ErrorMem()
func (c *connUDPBase) WriteTo(b []byte, dst *net.UDPAddr /*@, ghost underlyingConn *net.UDPConn @*/) (n int, err error) {
//@ unfold c.Mem()
//@ defer fold c.Mem()
//@ unfold acc(c.Mem(), _)
if c.Remote != nil {
return c.conn.Write(b)
}
Expand Down Expand Up @@ -475,7 +469,7 @@ func (c *connUDPBase) Close() (err error) {
func NewReadMessages(n int) (res Messages) {
m := make(Messages, n)
//@ invariant forall j int :: { &m[j] } (0 <= j && j < i0) ==> m[j].Mem(1)
//@ invariant forall j int :: { &m[j] } (i0 <= j && j < len(m)) ==> acc(&m[j])
//@ invariant forall j int :: { &m[j] } (i0 <= j && j < len(m)) ==> acc(&m[j]) && m[j].N == 0
//@ invariant forall j int :: { m[j].Addr } (i0 <= j && j < len(m)) ==> m[j].Addr == nil
//@ invariant forall j int :: { m[j].OOB } (i0 <= j && j < len(m)) ==> m[j].OOB == nil
//@ decreases len(m) - i
Expand Down
97 changes: 30 additions & 67 deletions private/underlay/conn/conn_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,74 +65,55 @@ pred (c *Config) Mem() {
/** Lift methods in *connUDPBase to *connUDPIPv4 **/
*connUDPIPv4 implements Conn

preserves c.Mem()
requires acc(c.Mem(), _)
preserves slices.AbsSlice_Bytes(b, 0, len(b))
ensures err == nil ==> 0 <= n && n <= len(b)
ensures err == nil ==> acc(addr.Mem(), _)
ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv4) ReadFrom(b []byte) (n int, addr *net.UDPAddr, err error) {
unfold c.Mem()
unfold c.connUDPBase.MemWithoutConn()
unfold acc(c.Mem(), _)
unfold acc(c.connUDPBase.MemWithoutConn(), _)
assert c.pconn.GetUnderlyingConn() == c.conn
tmpImpl := c.conn
tmpItf := c.pconn.ExchangePerm()
tmpItf := c.pconn.ExchangeWildcardPerm()
var packetconn *ipv4.PacketConn = c.pconn
assert tmpItf == c.conn
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.Mem()
fold acc(c.connUDPBase.Mem(), _)
n1, addr1, err1 := c.connUDPBase.ReadFrom(b, tmpImpl)
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
unfold c.connUDPBase.Mem()
apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.MemWithoutConn()
fold c.Mem()
return n1, addr1, err1
}

preserves c.Mem()
preserves acc(c.Mem(), _)
preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15)
ensures err == nil ==> 0 <= n && n <= len(b)
ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv4) Write(b []byte) (n int, err error) {
unfold c.Mem()
unfold c.connUDPBase.MemWithoutConn()
unfold acc(c.Mem(), _)
unfold acc(c.connUDPBase.MemWithoutConn(), _)
assert c.pconn.GetUnderlyingConn() == c.conn
tmpImpl := c.conn
tmpItf := c.pconn.ExchangePerm()
tmpItf := c.pconn.ExchangeWildcardPerm()
var packetconn *ipv4.PacketConn = c.pconn
assert tmpItf == c.conn
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.Mem()
fold acc(c.connUDPBase.Mem(), _)
n1, err1 := c.connUDPBase.Write(b, tmpImpl)
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
unfold c.connUDPBase.Mem()
apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.MemWithoutConn()
fold c.Mem()
return n1, err1
}

requires acc(dst.Mem(), _)
preserves c.Mem()
preserves acc(c.Mem(), _)
preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15)
ensures err == nil ==> 0 <= n && n <= len(b)
ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv4) WriteTo(b []byte, dst *net.UDPAddr) (n int, err error) {
unfold c.Mem()
unfold c.connUDPBase.MemWithoutConn()
unfold acc(c.Mem(), _)
unfold acc(c.connUDPBase.MemWithoutConn(), _)
assert c.pconn.GetUnderlyingConn() == c.conn
tmpImpl := c.conn
tmpItf := c.pconn.ExchangePerm()
tmpItf := c.pconn.ExchangeWildcardPerm()
var packetconn *ipv4.PacketConn = c.pconn
assert tmpItf == c.conn
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.Mem()
fold acc(c.connUDPBase.Mem(), _)
n1, err1 := c.connUDPBase.WriteTo(b, dst, tmpImpl)
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
unfold c.connUDPBase.Mem()
apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.MemWithoutConn()
fold c.Mem()
return n1, err1
}

Expand Down Expand Up @@ -169,74 +150,56 @@ func (c *connUDPIPv4) Close() (err error) {
/** Lift methods in *connUDPBase to *connUDPIPv6 **/
*connUDPIPv6 implements Conn

preserves c.Mem()
preserves acc(c.Mem(), _)
preserves slices.AbsSlice_Bytes(b, 0, len(b))
ensures err == nil ==> 0 <= n && n <= len(b)
ensures err == nil ==> acc(addr.Mem(), _)
ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv6) ReadFrom(b []byte) (n int, addr *net.UDPAddr, err error) {
unfold c.Mem()
unfold c.connUDPBase.MemWithoutConn()
unfold acc(c.Mem(), _)
unfold acc(c.connUDPBase.MemWithoutConn(), _)
assert c.pconn.GetUnderlyingConn() == c.conn
tmpImpl := c.conn
tmpItf := c.pconn.ExchangePerm()
tmpItf := c.pconn.ExchangeWildcardPerm()
var packetconn *ipv6.PacketConn = c.pconn
assert tmpItf == c.conn
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.Mem()
fold acc(c.connUDPBase.Mem(), _)
n1, addr1, err1 := c.connUDPBase.ReadFrom(b, tmpImpl)
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
unfold c.connUDPBase.Mem()
apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.MemWithoutConn()
fold c.Mem()
return n1, addr1, err1
}

preserves c.Mem()
preserves acc(c.Mem(), _)
preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15)
ensures err == nil ==> 0 <= n && n <= len(b)
ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv6) Write(b []byte) (n int, err error) {
unfold c.Mem()
unfold c.connUDPBase.MemWithoutConn()
unfold acc(c.Mem(), _)
unfold acc(c.connUDPBase.MemWithoutConn(), _)
assert c.pconn.GetUnderlyingConn() == c.conn
tmpImpl := c.conn
tmpItf := c.pconn.ExchangePerm()
tmpItf := c.pconn.ExchangeWildcardPerm()
var packetconn *ipv6.PacketConn = c.pconn
assert tmpItf == c.conn
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.Mem()
fold acc(c.connUDPBase.Mem(), _)
n1, err1 := c.connUDPBase.Write(b, tmpImpl)
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
unfold c.connUDPBase.Mem()
apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.MemWithoutConn()
fold c.Mem()
return n1, err1
}

requires acc(dst.Mem(), _)
preserves c.Mem()
preserves acc(c.Mem(), _)
preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15)
ensures err == nil ==> 0 <= n && n <= len(b)
ensures err != nil ==> err.ErrorMem()
func (c *connUDPIPv6) WriteTo(b []byte, dst *net.UDPAddr) (n int, err error) {
unfold c.Mem()
unfold c.connUDPBase.MemWithoutConn()
unfold acc(c.Mem(), _)
unfold acc(c.connUDPBase.MemWithoutConn(), _)
assert c.pconn.GetUnderlyingConn() == c.conn
tmpImpl := c.conn
tmpItf := c.pconn.ExchangePerm()
tmpItf := c.pconn.ExchangeWildcardPerm()
var packetconn *ipv6.PacketConn = c.pconn
assert tmpItf == c.conn
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.Mem()
fold acc(c.connUDPBase.Mem(), _)
n1, err1 := c.connUDPBase.WriteTo(b, dst, tmpImpl)
assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
unfold c.connUDPBase.Mem()
apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf)
fold c.connUDPBase.MemWithoutConn()
fold c.Mem()
return n1, err1
}

Expand Down
Loading
Loading