From d4d60a67e77b6edf6a9e9f1b897739f4790ee141 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Thu, 2 Apr 2015 11:46:33 +0200 Subject: [PATCH] PetScan::extract_argument: mark non-const pointer arguments as potential writes The initial version of pet followed the convention that if a function takes a pointer to const that then the passed array is read, while if it takes a pointer to non-const that then the passed array is completely written. This convention has remained even after the introduction of the distinction between may-writes and must-writes. Change it now to only mark the accessed elements as possibly being written to. At the same time, retain the fact that the elements may also be read by the function. These access relations can always be refined by the user by providing a summary function. Signed-off-by: Sven Verdoolaege --- scan.cc | 26 +++++++++++++++++++++++--- tests/QR.scop | 30 ++++++++++++++++++++++++------ tests/arg.scop | 10 ++++++++-- tests/array.scop | 5 ++++- tests/conditional_assignment.scop | 5 ++++- tests/conditional_assignment2.scop | 5 ++++- tests/data_dependent.scop | 5 ++++- tests/struct9.scop | 10 ++++++++-- tests/wdp.scop | 20 ++++++++++++++++---- tests/write.scop | 5 ++++- tests/write2.scop | 5 ++++- 11 files changed, 103 insertions(+), 23 deletions(-) diff --git a/scan.cc b/scan.cc index 67e1180..02b114e 100644 --- a/scan.cc +++ b/scan.cc @@ -640,6 +640,26 @@ static __isl_give pet_expr *mark_write(__isl_take pet_expr *access) return access; } +/* Mark the given (read) access pet_expr as also possibly being written. + * That is, initialize the may write access relation from the may read relation + * and initialize the must write access relation to the empty relation. + */ +static __isl_give pet_expr *mark_may_write(__isl_take pet_expr *expr) +{ + isl_union_map *access; + isl_union_map *empty; + + access = pet_expr_access_get_dependent_access(expr, + pet_expr_access_may_read); + empty = isl_union_map_empty(isl_union_map_get_space(access)); + expr = pet_expr_access_set_access(expr, pet_expr_access_may_write, + access); + expr = pet_expr_access_set_access(expr, pet_expr_access_must_write, + empty); + + return expr; +} + /* Construct a pet_expr representing a unary operator expression. */ __isl_give pet_expr *PetScan::extract_expr(UnaryOperator *expr) @@ -837,8 +857,8 @@ __isl_give pet_expr *PetScan::extract_assume(Expr *expr) * then the function being called may write into the array. * * We assume here that if the function is declared to take a pointer - * to a const type, then the function will perform a read - * and that otherwise, it will perform a write. + * to a const type, then the function may only perform a read + * and that otherwise, it may either perform a read or a write (or both). * We only perform this check if "detect_writes" is set. */ __isl_give pet_expr *PetScan::extract_argument(FunctionDecl *fd, int pos, @@ -872,7 +892,7 @@ __isl_give pet_expr *PetScan::extract_argument(FunctionDecl *fd, int pos, } parm = fd->getParamDecl(pos); if (!const_base(parm->getType())) - res = mark_write(res); + res = mark_may_write(res); } if (is_addr) diff --git a/tests/QR.scop b/tests/QR.scop index a6bf97c..1f69a02 100644 --- a/tests/QR.scop +++ b/tests/QR.scop @@ -89,25 +89,34 @@ statements: operation: '&' arguments: - type: access + may_read: '[N, K] -> { S_2[k, j] -> R[j, j] }' + may_write: '[N, K] -> { S_2[k, j] -> R[j, j] }' + must_write: '[N, K] -> { }' index: '[N, K] -> { S_2[k, j] -> R[(j), (j)] }' reference: __pet_ref_4 - read: 0 + read: 1 write: 1 - type: op operation: '&' arguments: - type: access + may_read: '[N, K] -> { S_2[k, j] -> X[k, j] }' + may_write: '[N, K] -> { S_2[k, j] -> X[k, j] }' + must_write: '[N, K] -> { }' index: '[N, K] -> { S_2[k, j] -> X[(k), (j)] }' reference: __pet_ref_5 - read: 0 + read: 1 write: 1 - type: op operation: '&' arguments: - type: access + may_read: '[N, K] -> { S_2[k, j] -> t[] }' + may_write: '[N, K] -> { S_2[k, j] -> t[] }' + must_write: '[N, K] -> { }' index: '[N, K] -> { S_2[k, j] -> t[] }' reference: __pet_ref_6 - read: 0 + read: 1 write: 1 - line: 29 domain: '[N, K] -> { S_3[k, j, i] : k <= -1 + K and i <= -1 + N and j >= 0 and i @@ -137,25 +146,34 @@ statements: operation: '&' arguments: - type: access + may_read: '[N, K] -> { S_3[k, j, i] -> R[j, i] }' + may_write: '[N, K] -> { S_3[k, j, i] -> R[j, i] }' + must_write: '[N, K] -> { }' index: '[N, K] -> { S_3[k, j, i] -> R[(j), (i)] }' reference: __pet_ref_10 - read: 0 + read: 1 write: 1 - type: op operation: '&' arguments: - type: access + may_read: '[N, K] -> { S_3[k, j, i] -> X[k, i] }' + may_write: '[N, K] -> { S_3[k, j, i] -> X[k, i] }' + must_write: '[N, K] -> { }' index: '[N, K] -> { S_3[k, j, i] -> X[(k), (i)] }' reference: __pet_ref_11 - read: 0 + read: 1 write: 1 - type: op operation: '&' arguments: - type: access + may_read: '[N, K] -> { S_3[k, j, i] -> t[] }' + may_write: '[N, K] -> { S_3[k, j, i] -> t[] }' + must_write: '[N, K] -> { }' index: '[N, K] -> { S_3[k, j, i] -> t[] }' reference: __pet_ref_12 - read: 0 + read: 1 write: 1 - line: 34 domain: '[N, K] -> { S_4[j, i] : i >= j and i <= -1 + N and j >= 0 }' diff --git a/tests/arg.scop b/tests/arg.scop index 2a69453..53d42b2 100644 --- a/tests/arg.scop +++ b/tests/arg.scop @@ -35,9 +35,12 @@ statements: operation: '&' arguments: - type: access + may_read: '{ S_0[i] -> a[] }' + may_write: '{ S_0[i] -> a[] }' + must_write: '{ }' index: '{ S_0[i] -> a[] }' reference: __pet_ref_1 - read: 0 + read: 1 write: 1 - line: 12 domain: '{ S_1[i] : i >= 0 and i <= 9 }' @@ -59,7 +62,10 @@ statements: operation: '&' arguments: - type: access + may_read: '{ S_1[i] -> b[1 + i] }' + may_write: '{ S_1[i] -> b[1 + i] }' + must_write: '{ }' index: '{ S_1[i] -> b[(1 + i)] }' reference: __pet_ref_3 - read: 0 + read: 1 write: 1 diff --git a/tests/array.scop b/tests/array.scop index 134f515..a656250 100644 --- a/tests/array.scop +++ b/tests/array.scop @@ -28,8 +28,11 @@ statements: read: 1 write: 0 - type: access + may_read: '{ S_0[] -> B[o0] }' + may_write: '{ S_0[] -> B[o0] }' + must_write: '{ }' index: '{ S_0[] -> B[] }' depth: 1 reference: __pet_ref_1 - read: 0 + read: 1 write: 1 diff --git a/tests/conditional_assignment.scop b/tests/conditional_assignment.scop index d467f54..4df228e 100644 --- a/tests/conditional_assignment.scop +++ b/tests/conditional_assignment.scop @@ -107,10 +107,13 @@ statements: read: 1 write: 0 - type: access + may_read: '[N, M] -> { S_2[i] -> A[i, o1] }' + may_write: '[N, M] -> { S_2[i] -> A[i, o1] }' + must_write: '[N, M] -> { }' index: '[N, M] -> { S_2[i] -> A[(i)] }' depth: 2 reference: __pet_ref_6 - read: 0 + read: 1 write: 1 - line: 26 domain: '[N, M] -> { S_3[] }' diff --git a/tests/conditional_assignment2.scop b/tests/conditional_assignment2.scop index ecbabe1..2efc84b 100644 --- a/tests/conditional_assignment2.scop +++ b/tests/conditional_assignment2.scop @@ -123,10 +123,13 @@ statements: read: 1 write: 0 - type: access + may_read: '[M, N] -> { S_3[i] -> A[i, o1] }' + may_write: '[M, N] -> { S_3[i] -> A[i, o1] }' + must_write: '[M, N] -> { }' index: '[M, N] -> { S_3[i] -> A[(i)] }' depth: 2 reference: __pet_ref_7 - read: 0 + read: 1 write: 1 - line: 28 domain: '[M, N] -> { S_4[] }' diff --git a/tests/data_dependent.scop b/tests/data_dependent.scop index b75ba86..fd50079 100644 --- a/tests/data_dependent.scop +++ b/tests/data_dependent.scop @@ -106,10 +106,13 @@ statements: read: 1 write: 0 - type: access + may_read: '[N, M] -> { S_2[i] -> A[i, o1] }' + may_write: '[N, M] -> { S_2[i] -> A[i, o1] }' + must_write: '[N, M] -> { }' index: '[N, M] -> { S_2[i] -> A[(i)] }' depth: 2 reference: __pet_ref_6 - read: 0 + read: 1 write: 1 - line: 28 domain: '[N, M] -> { S_3[] }' diff --git a/tests/struct9.scop b/tests/struct9.scop index ec2ffb0..6fa98a6 100644 --- a/tests/struct9.scop +++ b/tests/struct9.scop @@ -53,10 +53,13 @@ statements: name: f2 arguments: - type: access + may_read: '{ S_1[i, j, k, l] -> s_a[s[i, j] -> a[k, o3]] }' + may_write: '{ S_1[i, j, k, l] -> s_a[s[i, j] -> a[k, o3]] }' + must_write: '{ }' index: '{ S_1[i, j, k, l] -> s_a[s[(i), (j)] -> a[(k)]] }' depth: 4 reference: __pet_ref_1 - read: 0 + read: 1 write: 1 - line: 20 domain: '{ S_2[i, j, k, l] : i >= 0 and i <= 9 and j >= 0 and j <= 19 and k >= 0 @@ -68,8 +71,11 @@ statements: name: f3 arguments: - type: access + may_read: '{ S_2[i, j, k, l] -> s_a[s[i, j] -> a[o2, o3]] }' + may_write: '{ S_2[i, j, k, l] -> s_a[s[i, j] -> a[o2, o3]] }' + must_write: '{ }' index: '{ S_2[i, j, k, l] -> s_a[s[(i), (j)] -> a[]] }' depth: 4 reference: __pet_ref_2 - read: 0 + read: 1 write: 1 diff --git a/tests/wdp.scop b/tests/wdp.scop index 8005687..aac9341 100644 --- a/tests/wdp.scop +++ b/tests/wdp.scop @@ -66,17 +66,23 @@ statements: operation: '&' arguments: - type: access + may_read: '[N] -> { S_1[i] -> y[i] }' + may_write: '[N] -> { S_1[i] -> y[i] }' + must_write: '[N] -> { }' index: '[N] -> { S_1[i] -> y[(i)] }' reference: __pet_ref_1 - read: 0 + read: 1 write: 1 - type: op operation: '&' arguments: - type: access + may_read: '[N] -> { S_1[i] -> t[i] }' + may_write: '[N] -> { S_1[i] -> t[i] }' + must_write: '[N] -> { }' index: '[N] -> { S_1[i] -> t[(i)] }' reference: __pet_ref_2 - read: 0 + read: 1 write: 1 - line: 25 domain: '[N] -> { S_2[i] : i <= 1 + N and i >= 0 }' @@ -227,15 +233,21 @@ statements: operation: '&' arguments: - type: access + may_read: '[N] -> { S_7[i] -> y[1 + i] }' + may_write: '[N] -> { S_7[i] -> y[1 + i] }' + must_write: '[N] -> { }' index: '[N] -> { S_7[i] -> y[(1 + i)] }' reference: __pet_ref_18 - read: 0 + read: 1 write: 1 - type: op operation: '&' arguments: - type: access + may_read: '[N] -> { S_7[i] -> z[2 + i] }' + may_write: '[N] -> { S_7[i] -> z[2 + i] }' + must_write: '[N] -> { }' index: '[N] -> { S_7[i] -> z[(2 + i)] }' reference: __pet_ref_19 - read: 0 + read: 1 write: 1 diff --git a/tests/write.scop b/tests/write.scop index 1bb6d2d..1515d52 100644 --- a/tests/write.scop +++ b/tests/write.scop @@ -24,8 +24,11 @@ statements: read: 1 write: 0 - type: access + may_read: '[n] -> { S_0[] -> A[o0, o1] }' + may_write: '[n] -> { S_0[] -> A[o0, o1] }' + must_write: '[n] -> { }' index: '[n] -> { S_0[] -> A[] }' depth: 2 reference: __pet_ref_1 - read: 0 + read: 1 write: 1 diff --git a/tests/write2.scop b/tests/write2.scop index 20b8d2a..a15c512 100644 --- a/tests/write2.scop +++ b/tests/write2.scop @@ -24,8 +24,11 @@ statements: read: 1 write: 0 - type: access + may_read: '[n] -> { S_0[] -> A[o0, o1] }' + may_write: '[n] -> { S_0[] -> A[o0, o1] }' + must_write: '[n] -> { }' index: '[n] -> { S_0[] -> A[] }' depth: 2 reference: __pet_ref_1 - read: 0 + read: 1 write: 1 -- 2.11.4.GIT