Merge pull request #182 from nikhilc1527/new

translation bug for ref into slice

Author: upamanyus

goose.go

@@ -717,12 +717,6 @@ func (ctx *Ctx) unaryExpr(e *ast.UnaryExpr, multipleBindings bool) glang.Expr {
 		return glang.NotExpr{X: ctx.expr(e.X)}
 	}
 	if e.Op == token.AND {
-		if x, ok := e.X.(*ast.IndexExpr); ok {
-			// e is &a[b] where x is a.b
-			return glang.NewCallExpr(glang.VerbatimExpr("IndexRef"),
-				ctx.glangType(e, ctx.typeOf(x)),
-				glang.TupleExpr{ctx.expr(x.X), ctx.expr(x.Index)})
-		}
 		if cl, ok := e.X.(*ast.CompositeLit); ok {
 			// e is &T{...} (a composite literal)
 			sl := ctx.compositeLiteral(cl)

testdata/examples/semantics/generated_test.go

@@ -411,6 +411,8 @@ Definition testSliceLiteral {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_
 
 Definition testSliceAppend {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/semantics.testSliceAppend"%go.
 
+Definition testSliceRef {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/semantics.testSliceRef"%go.
+
 Definition testFooBarMutation {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/semantics.testFooBarMutation"%go.
 
 Definition NewS {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/semantics.NewS"%go.
@@ -2402,7 +2404,7 @@ Definition testSliceOpsⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext
     Slice (go.SliceType go.uint64) ("$s", #(W64 0), #(W64 3))) in
     do:  ("v3" <-[go.SliceType go.uint64] "$r0");;;
     let: "v4" := (GoAlloc (go.PointerType go.uint64) (GoZeroVal (go.PointerType go.uint64) #())) in
-    let: "$r0" := (IndexRef go.uint64 (![go.SliceType go.uint64] "x", #(W64 2))) in
+    let: "$r0" := (IndexRef (go.SliceType go.uint64) (![go.SliceType go.uint64] "x", #(W64 2))) in
     do:  ("v4" <-[go.PointerType go.uint64] "$r0");;;
     let: "ok" := (GoAlloc go.bool (GoZeroVal go.bool #())) in
     let: "$r0" := #true in
@@ -2563,6 +2565,19 @@ Definition testSliceAppendⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalCont
     do:  ("ok" <-[go.bool] "$r0");;;
     return: (![go.bool] "ok")).
 
+(* go: slices.go:100:6 *)
+Definition testSliceRefⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
+  λ: <>,
+    exception_do (let: "sl" := (GoAlloc (go.SliceType go.uint64) (GoZeroVal (go.SliceType go.uint64) #())) in
+    let: "$r0" := ((FuncResolve go.make2 [go.SliceType go.uint64] #()) #(W64 5)) in
+    do:  ("sl" <-[go.SliceType go.uint64] "$r0");;;
+    let: "ptr" := (GoAlloc (go.PointerType go.uint64) (GoZeroVal (go.PointerType go.uint64) #())) in
+    let: "$r0" := (IndexRef (go.SliceType go.uint64) (![go.SliceType go.uint64] "sl", #(W64 0))) in
+    do:  ("ptr" <-[go.PointerType go.uint64] "$r0");;;
+    let: "$r0" := #(W64 1) in
+    do:  ((![go.PointerType go.uint64] "ptr") <-[go.uint64] "$r0");;;
+    return: ((![go.uint64] (IndexRef (go.SliceType go.uint64) (![go.SliceType go.uint64] "sl", #(W64 0)))) =⟨go.uint64⟩ #(W64 1))).
+
 (* go: struct_pointers.go:14:17 *)
 Definition Bar__mutateⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
   λ: "bar" <>,
@@ -4486,6 +4501,7 @@ Class Assumptions `{!GoGlobalContext} `{!GoLocalContext} `{!GoSemanticsFunctions
   #[global] testOverwriteArray_unfold :: FuncUnfold testOverwriteArray [] (testOverwriteArrayⁱᵐᵖˡ);
   #[global] testSliceLiteral_unfold :: FuncUnfold testSliceLiteral [] (testSliceLiteralⁱᵐᵖˡ);
   #[global] testSliceAppend_unfold :: FuncUnfold testSliceAppend [] (testSliceAppendⁱᵐᵖˡ);
+  #[global] testSliceRef_unfold :: FuncUnfold testSliceRef [] (testSliceRefⁱᵐᵖˡ);
   #[global] testFooBarMutation_unfold :: FuncUnfold testFooBarMutation [] (testFooBarMutationⁱᵐᵖˡ);
   #[global] NewS_unfold :: FuncUnfold NewS [] (NewSⁱᵐᵖˡ);
   #[global] testStructUpdates_unfold :: FuncUnfold testStructUpdates [] (testStructUpdatesⁱᵐᵖˡ);

testdata/examples/semantics/semantics.gold.v

@@ -96,3 +96,10 @@ func testSliceAppend() bool {
 	ok = ok && bytes[2] == byte(3)
 	return ok
 }
+
+func testSliceRef() bool {
+	var sl = make([]uint64, 5)
+	var ptr = &sl[0]
+	*ptr = 1
+	return (sl[0] == 1)
+}

testdata/examples/semantics/slices.go

@@ -697,7 +697,7 @@ Definition usesArrayElemRefⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalCon
     do:  ("x" <-[go.ArrayType 2 go.string] "$r0");;;
     let: "$r0" := #"c"%go in
     do:  ((IndexRef (go.ArrayType 2 go.string) (![go.ArrayType 2 go.string] "x", #(W64 1))) <-[go.string] "$r0");;;
-    do:  (let: "$a0" := (IndexRef go.string (![go.ArrayType 2 go.string] "x", #(W64 1))) in
+    do:  (let: "$a0" := (IndexRef (go.ArrayType 2 go.string) (![go.ArrayType 2 go.string] "x", #(W64 1))) in
     (FuncResolve takesPtr [] #()) "$a0");;;
     return: #()).
 
@@ -2690,7 +2690,7 @@ Definition sliceOpsⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} :
     Slice (go.SliceType go.uint64) ("$s", #(W64 0), #(W64 3))) in
     do:  ("v3" <-[go.SliceType go.uint64] "$r0");;;
     let: "v4" := (GoAlloc (go.PointerType go.uint64) (GoZeroVal (go.PointerType go.uint64) #())) in
-    let: "$r0" := (IndexRef go.uint64 (![go.SliceType go.uint64] "x", #(W64 2))) in
+    let: "$r0" := (IndexRef (go.SliceType go.uint64) (![go.SliceType go.uint64] "x", #(W64 2))) in
     do:  ("v4" <-[go.PointerType go.uint64] "$r0");;;
     return: ((((((![go.uint64] "v1") +⟨go.uint64⟩ (![go.uint64] (IndexRef (go.SliceType go.uint64) (![go.SliceType go.uint64] "v2", #(W64 0))))) +⟨go.uint64⟩ (![go.uint64] (IndexRef (go.SliceType go.uint64) (![go.SliceType go.uint64] "v3", #(W64 1))))) +⟨go.uint64⟩ (![go.uint64] (![go.PointerType go.uint64] "v4"))) +⟨go.uint64⟩ (Convert go.int go.uint64 (let: "$a0" := (![go.SliceType go.uint64] "x") in
      (FuncResolve go.len [go.SliceType go.uint64] #()) "$a0"))) +⟨go.uint64⟩ (Convert go.int go.uint64 (let: "$a0" := (![go.SliceType go.uint64] "x") in
@@ -2708,7 +2708,7 @@ Definition sliceOfThings__getThingRefⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : G
   λ: "ts" "i",
     exception_do (let: "ts" := (GoAlloc sliceOfThings "ts") in
     let: "i" := (GoAlloc go.uint64 "i") in
-    return: (IndexRef thing (![go.SliceType thing] (StructFieldRef sliceOfThings "things"%go "ts"), ![go.uint64] "i"))).
+    return: (IndexRef (go.SliceType thing) (![go.SliceType thing] (StructFieldRef sliceOfThings "things"%go "ts"), Convert go.uint64 go.int (![go.uint64] "i")))).
 
 (* go: slices.go:30:6 *)
 Definition makeAliasⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=