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

fix: improve golang externs #1133

Merged
merged 2 commits into from
Dec 17, 2024
+23 −13
Merged

fix: improve golang externs #1133

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
78ca0dd
fix: improve golang externs
ajewellamz Dec 17, 2024
bd23e6a
m
ajewellamz Dec 17, 2024
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
18 changes: 10 additions & 8 deletions StandardLibrary/runtimes/go/ImplementationFromDafny-go/FileIO/externs.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ import (
os "os"
"path/filepath"

"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
_dafny "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
)

Expand All @@ -28,8 +29,7 @@ func (_static CompanionStruct_Default___) INTERNAL_ReadBytesFromFile(path _dafny

dat, err := ioutil.ReadFile(p)
if err != nil {
errAsSequence := _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
return true, _dafny.EmptySeq, errAsSequence
return true, _dafny.EmptySeq, _dafny.SeqOfChars([]dafny.Char(err.Error())...)
}
datAsSequence := _dafny.SeqOfBytes(dat)
return false, datAsSequence, _dafny.EmptySeq
Expand All @@ -53,8 +53,7 @@ func (_static CompanionStruct_Default___) INTERNAL_WriteBytesToFile(path _dafny.
bytesArray := _dafny.ToByteArray(bytes)
err := ioutil.WriteFile(p, bytesArray, 0644)
if err != nil {
errAsSequence := _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
return true, errAsSequence
return true, _dafny.SeqOfChars([]dafny.Char(err.Error())...)
}
return false, _dafny.EmptySeq
}
Expand All @@ -73,21 +72,24 @@ func (_static CompanionStruct_Default___) INTERNAL_AppendBytesToFile(path _dafny
}()

// Create directories
os.MkdirAll(filepath.Dir(p), os.ModePerm)
err := os.MkdirAll(filepath.Dir(p), os.ModePerm)
if err != nil {
return true, _dafny.SeqOfChars([]dafny.Char(err.Error())...)
}

bytesArray := _dafny.ToByteArray(bytes)

f, err := os.OpenFile(p, os.O_APPEND|os.O_CREATE|os.O_WRONLY, 0644)
if err != nil {
return true, _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
return true, _dafny.SeqOfChars([]dafny.Char(err.Error())...)
}

if _, err := f.Write(bytesArray); err != nil {
return true, _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
return true, _dafny.SeqOfChars([]dafny.Char(err.Error())...)
}

if err := f.Close(); err != nil {
return true, _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
return true, _dafny.SeqOfChars([]dafny.Char(err.Error())...)
}

return false, _dafny.EmptySeq
Expand Down
7 changes: 5 additions & 2 deletions StandardLibrary/runtimes/go/ImplementationFromDafny-go/Time_/externs.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,10 @@ func (CompanionStruct_Default___) GetProcessCpuTimeMillis() int64 {
}

func GetProcessCpuTimeMillis() int64 {
usage := new(syscall.Rusage)
syscall.Getrusage(syscall.RUSAGE_SELF, usage)
var usage syscall.Rusage
err := syscall.Getrusage(syscall.RUSAGE_SELF, &usage)
if err != nil {
return 0
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I assume 0 is okay, but why not return error in the method signature?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Because what else could the caller do but pretend it was zero?
None of the other languages had this issue, and so like "get current time" it seems silly to return an error.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, Go returns error with output instead of separately? Maybe -1 if not err?

}
return (usage.Utime.Nano() + usage.Stime.Nano()) / 1000000
}
3 changes: 0 additions & 3 deletions StandardLibrary/test/GetOpt.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,6 @@ module GetOptTest {
]);
var x :- expect GetOptions(MyOptions, ["cmd", "--help"]);
var y :- expect NeedsHelp(MyOptions, x);
print "\n", y, "\n";
}

method {:test} TestHelpFail() {
Expand Down Expand Up @@ -196,11 +195,9 @@ module GetOptTest {

x :- expect GetOptions(MyOptions, ["MyProg", "--help"]);
var y :- expect NeedsHelp(MyOptions, x);
print "\n", y, "\n";

x :- expect GetOptions(MyOptions, ["MyProg", "command", "--help"]);
y :- expect NeedsHelp(MyOptions, x);
print "\n", y, "\n";
}

method {:test} TestDefault() {
Expand Down
8 changes: 8 additions & 0 deletions StandardLibrary/test/TestString.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,4 +47,12 @@ module TestStrings {
expect y == [1,2,3,4,5];
}

// ensure that FileIO error are returned properly, and not a panic! or the like
// This fails to fail on Windows+Dotnet, becasue \ instead of /
// method {:test} TestBadFileIO()
// {
// var x := WriteBytesToFile("/../../MyFile", [1,2,3,4,5]);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why commented code? Shouldn't we remove it?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  1. we really want this test, and I want to leave a reminder that we can't do this.
  2. it's convenient to test locally by uncommenting, even if you can't run it in CI.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should add a comment Enable this test if you want to test X locally?

// expect x.Failure?;
// }

}
Loading