Fix Go compilation issues

mit-pdos · Jan 12, 2024 · 8bfd1d4 · 8bfd1d4
1 parent a5e3c8e
commit 8bfd1d4
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 16 deletions.
diff --git a/dafny_go/jrnl/jrnl.go b/dafny_go/jrnl/jrnl.go
@@ -9,11 +9,7 @@ import (
 
 type Disk = disk.Disk
 
-type Companion_DefaultStruct struct{}
-
-var Companion_Default___ = Companion_DefaultStruct{}
-
-func (_ Companion_DefaultStruct) DiskSize(d *Disk) uint64 {
+func DiskSize(d *Disk) uint64 {
 	return (*d).Size()
 }
 

diff --git a/nfsd/ops.go b/nfsd/ops.go
@@ -519,7 +519,7 @@ func (nfs *Nfs) NFSPROC3_RMDIR(args nfstypes.RMDIR3args) nfstypes.RMDIR3res {
 	return reply
 }
 
-func (nfs *Nfs) runWithLocks(f func(txn Txn, locks dafny.Seq) Result) (v interface{}, status nfstypes.Nfsstat3) {
+func (nfs *Nfs) runWithLocks(f func(txn Txn, locks dafny.Sequence) Result) (v interface{}, status nfstypes.Nfsstat3) {
 	locks := lock_order.Companion_Default___.EmptyLockHint()
 	for {
 		txn := nfs.filesys.Begin()
@@ -544,7 +544,7 @@ func (nfs *Nfs) NFSPROC3_RENAME(args nfstypes.RENAME3args) (reply nfstypes.RENAM
 	dst_inum := fh2ino(args.To.Dir)
 	dst_name := filenameToBytes(args.To.Name)
 
-	_, status := nfs.runWithLocks(func(txn Txn, locks dafny.Seq) Result {
+	_, status := nfs.runWithLocks(func(txn Txn, locks dafny.Sequence) Result {
 		return nfs.filesys.RENAME(txn, locks, src_inum, src_name, dst_inum, dst_name)
 	})
 
@@ -579,19 +579,19 @@ func (nfs *Nfs) NFSPROC3_READDIR(args nfstypes.READDIR3args) (reply nfstypes.REA
 		util.DPrintf(1, "NFS Readdir error %v", status)
 		return reply
 	}
-	seq := r.(dafny.Seq)
+	seq := r.(dafny.Sequence)
 
-	seqlen := seq.LenInt()
+	seqlen := seq.Cardinality()
 	// TODO: produce this . from Dafny, or add it to every directory
 	ents := &nfstypes.Entry3{
 		Fileid:    nfstypes.Fileid3(inum),
 		Name:      nfstypes.Filename3("."),
 		Cookie:    1,
 		Nextentry: nil,
 	}
-	for i := 0; i < seqlen; i++ {
-		dirent := seq.IndexInt(i).(memdirents.MemDirEnt)
-		dirent2 := dirent.Get().(memdirents.MemDirEnt_MemDirEnt)
+	for i := uint32(0); i < seqlen; i++ {
+		dirent := seq.Select(i).(memdirents.MemDirEnt)
+		dirent2 := dirent.Get_().(memdirents.MemDirEnt_MemDirEnt)
 
 		de_ino := dirent2.Ino
 		var de_name []byte = dirent2.Name.Data

diff --git a/src/fs/inode_fs.dfy b/src/fs/inode_fs.dfy
@@ -188,7 +188,7 @@ module InodeFs {
     {
       var jrnl := NewJrnl(d, fs_kinds);
       this.jrnl := jrnl;
-      var num_blks := d.Size();
+      var num_blks := DiskSize(d);
       var actual_max := ballocMax;
       if super_data_start+8 < num_blks <= actual_max {
         actual_max := Round.roundup64(num_blks - super_data_start - 8, 8);

diff --git a/tests/dir_test.go b/tests/dir_test.go
@@ -23,11 +23,11 @@ func NewFs() *dirfs.DirFilesys {
 	if dfsopt.Is_None() {
 		panic("no dirfs")
 	}
-	dfs := dfsopt.Get().(std.Option_Some).X.(*dirfs.DirFilesys)
+	dfs := dfsopt.Get_().(std.Option_Some).X.(*dirfs.DirFilesys)
 	return dfs
 }
 
-func seqOfString(s string) _dafny.Seq {
+func seqOfString(s string) _dafny.Sequence {
 	xs_i := make([]interface{}, len(s))
 	for i, x := range []byte(s) {
 		xs_i[i] = x
@@ -75,7 +75,7 @@ func TestDirFsLookup(t *testing.T) {
 func TestPathEncode(t *testing.T) {
 	s := seqOfString("foo")
 	s2 := dirents.Companion_Default___.DecodeEncodeTest(s)
-	assert.Equal(t, s2.LenInt(), int(3), "decoded string is short")
+	assert.Equal(t, s2.Cardinality(), uint32(3), "decoded string is short")
 }
 
 // based on a test rtm came up with