Skip to content

Commit

Permalink
Fixes to get unittest to build; remove some tests for primitives that
Browse files Browse the repository at this point in the history
likely don't need to exist anymore.
  • Loading branch information
upamanyus committed Aug 13, 2024
1 parent 122fee8 commit 8c1c96f
Show file tree
Hide file tree
Showing 4 changed files with 12 additions and 29 deletions.
14 changes: 2 additions & 12 deletions goose.go
Original file line number Diff line number Diff line change
Expand Up @@ -654,16 +654,11 @@ func (ctx Ctx) selectionMethod(addressable bool, expr glang.Expr,
}

if pointerT, ok := types.Unalias(curType).(*types.Pointer); ok {
// FIXME: the unaliased version might be preferred for consistent
// naming, but that breaks the way `prophId` works in `primitive` at the
// moment.
// t, ok := types.Unalias(pointerT.Elem()).(*types.Named)
t, ok := pointerT.Elem().(*types.Named)
t, ok := types.Unalias(pointerT.Elem()).(*types.Named)
if !ok {
ctx.nope(l, "methods can only be called on a pointer if the base type is a defined type, not %s", pointerT.Elem())
}
m := glang.TypeMethod(ctx.qualifiedName(t.Obj()), t.Method(fnIndex).Name())
fmt.Println(ctx.qualifiedName(t.Obj()))

// check for recursive call
var f glang.Expr
Expand All @@ -689,13 +684,8 @@ func (ctx Ctx) selectionMethod(addressable bool, expr glang.Expr,
// ctx.unsupported(e, "%v", funcSig)
return glang.NewCallExpr(f, glang.DerefExpr{X: expr, Ty: ctx.glangType(l, t)})
}
} else if t, ok := curType.(*types.Named); ok {
// else if t, ok := types.Unalias(curType).(*types.Named); ok {
// FIXME: the unaliased version might be preferred for consistent
// naming, but that breaks the way `prophId` works in `primitive` at the
// moment.
} else if t, ok := types.Unalias(curType).(*types.Named); ok {
var typeName = ctx.qualifiedName(t.Obj())
fmt.Println(typeName)
m := glang.TypeMethod(typeName, t.Method(fnIndex).Name())

var f glang.Expr
Expand Down
3 changes: 1 addition & 2 deletions testdata/examples/unittest/proph.go
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,7 @@ import "github.com/goose-lang/primitive"

func Oracle() {
p := primitive.NewProph()
p.ResolveBool(false)
p.ResolveU64(0)
p = p
}

type typing struct {
Expand Down
6 changes: 2 additions & 4 deletions testdata/examples/unittest/strings.go
Original file line number Diff line number Diff line change
@@ -1,9 +1,7 @@
package unittest

import "github.com/goose-lang/primitive"

func stringAppend(s string, x uint64) string {
return "prefix " + s + " " + primitive.UInt64ToString(x)
func stringAppend(s string) string {
return "prefix " + s + " "
}

func stringLength(s string) uint64 {
Expand Down
18 changes: 7 additions & 11 deletions testdata/examples/unittest/unittest.gold.v
Original file line number Diff line number Diff line change
Expand Up @@ -1475,10 +1475,8 @@ Definition Oracle : val :=
exception_do (let: "p" := (ref_ty ptrT (zero_val ptrT)) in
let: "$r0" := (primitive.NewProph #()) in
do: ("p" <-[ptrT] "$r0");;;
do: (let: "$a0" := #false in
(primitive.prophId__ResolveBool (![ptrT] "p")) "$a0");;;
do: (let: "$a0" := #0 in
(primitive.prophId__ResolveU64 (![ptrT] "p")) "$a0")).
let: "$r0" := (![ptrT] "p") in
do: ("p" <-[ptrT] "$r0")).

Definition typing : go_type := structT [
"proph" :: ptrT
Expand Down Expand Up @@ -1849,15 +1847,13 @@ Definition loopSpawn : val :=
do: ("dummy" <-[boolT] "$r0");;;
continue: #()))).

(* go: strings.go:5:6 *)
(* go: strings.go:3:6 *)
Definition stringAppend : val :=
rec: "stringAppend" "s" "x" :=
exception_do (let: "x" := (ref_ty uint64T "x") in
let: "s" := (ref_ty stringT "s") in
return: (((#(str "prefix ") + (![stringT] "s")) + #(str " ")) + (let: "$a0" := (![uint64T] "x") in
primitive.UInt64ToString "$a0"))).
rec: "stringAppend" "s" :=
exception_do (let: "s" := (ref_ty stringT "s") in
return: ((#(str "prefix ") + (![stringT] "s")) + #(str " "))).

(* go: strings.go:9:6 *)
(* go: strings.go:7:6 *)
Definition stringLength : val :=
rec: "stringLength" "s" :=
exception_do (let: "s" := (ref_ty stringT "s") in
Expand Down

0 comments on commit 8c1c96f

Please sign in to comment.