How to model C char* that can be 0?

[gmhwxi]

When using these types, please get the ‘cast’ function ready
Proving stuff at this level may not be what you want to do right now.On Thursday, January 23, 2014 5:46:13 PM UTC-5, gmhwxi wrote:

Take a look at ‘stropt’ (functional) or ‘strptr’ (linear).

On Thursday, January 23, 2014 5:34:48 PM UTC-5, H Zhang wrote:

Some C library functions use zero valued pointer for special meaning.
What is the best way to model this? I would like to use string to model
char*, but then I can’t assign the value zero to a variable of type string.

[gmhwxi]

ptr2cptr is unsafe but cptr2ptr is safe :)On Thursday, January 23, 2014 5:34:48 PM UTC-5, H Zhang wrote:

Some C library functions use zero valued pointer for special meaning. What
is the best way to model this? I would like to use string to model char*,
but then I can’t assign the value zero to a variable of type string.

[Brandon_Barker]

Interestingly, as a side note, it seems a bit odd that 0 is passed as the
third argument: already dependent types could be useful in this scenario,
since in their example, the number of variables (which I assume should be
numvars) should be 3.

Brandon Barker
brandon…@gmail.comOn Thu, Jan 23, 2014 at 5:54 PM, Brandon Barker brandon...@gmail.comwrote:

Relatedly, I was actually about to ask a similar question. How to do this
in general (not just for char*)?

currently I was thinking of implementing a datavtype that is very similar
to an option_vt but is either sometype or NULL (instead of sometype or
void), where NULL is:

macdef NULL = $extype(ptr, “0”)

For context, I have a C function that looks like this:

GRBnewmodel(GRBenv *env, GRBmodel **modelP, const char *Pname, intnumvars
,
double *obj, double *lb, double *ub, char *vtype,
char **varnames);

Where an example call looks like this:

error = GRBaddvars(model, 3, 0, NULL, NULL, NULL, obj, NULL, NULL, vtype
,
NULL);

On Thursday, January 23, 2014 5:48:46 PM UTC-5, gmhwxi wrote:

When using these types, please get the ‘cast’ function ready
Proving stuff at this level may not be what you want to do right now.

On Thursday, January 23, 2014 5:46:13 PM UTC-5, gmhwxi wrote:

Take a look at ‘stropt’ (functional) or ‘strptr’ (linear).

On Thursday, January 23, 2014 5:34:48 PM UTC-5, H Zhang wrote:

Some C library functions use zero valued pointer for special meaning.
What is the best way to model this? I would like to use string to model
char*, but then I can’t assign the value zero to a variable of type string.

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/678eb1df-cd7e-4e65-a422-80fcfe21c743%40googlegroups.com
.

[gmhwxi]

I had the bug this morning (:On Friday, January 24, 2014 1:27:17 AM UTC-5, gmhwxi wrote:

Dataviewtypes are good stuff.

When there are proofs of views involved, casting is tricky. I actually had
a bug due to casting that forced me to read source code of cairo. In
general, I use casting lightly unless I expect my code to be thoroughly
tested.

On Friday, January 24, 2014 12:55:35 AM UTC-5, Brandon Barker wrote:

I was really having similar thoughts earlier today, except I was thinking
of entire data(v)types, not just a single constructor. Though I haven’t
tried it, i guess it is better to avoid having to constantly and
unnecessarily work with constructors and pattern matching at the user
level, and just stick with a few simple pointer casts at the lower level.

Brandon Barker
brand...@gmail.com

On Fri, Jan 24, 2014 at 12:49 AM, gmhwxi gmh...@gmail.com wrote:

But what does that buy you?

On Friday, January 24, 2014 12:40:18 AM UTC-5, H Zhang wrote:

Ah, now I see. I was briefly excited thinking that we could put a boxed
type constructor directly onto a C function call

On Thursday, January 23, 2014 9:18:27 PM UTC-8, gmhwxi wrote:

stropt_some is not a constructor; it is a no-op cast function.
In mathematics, this is called embedding (since stropt = string +
NULL).

On Friday, January 24, 2014 12:11:30 AM UTC-5, H Zhang wrote:

That is great, but how is stropt defined? In basics_sta.sats:

abstype
stropt_int_type (n:int) = ptr
stadef stropt = stropt_int_type

How does it know about the constructor stropt_some?

On Thursday, January 23, 2014 8:34:42 PM UTC-8, gmhwxi wrote:

val library = dlopen(stropt_some"testdll.dll", RTLD_GLOBAL)

On Thursday, January 23, 2014 11:31:16 PM UTC-5, H Zhang wrote:

Explict cast to stropt fixes the compile, but in terms of semantics
if something can be assigned to string then it should also be assigned to
stropt?

On Thursday, January 23, 2014 8:27:57 PM UTC-8, H Zhang wrote:

However if I use stropt I seem to get trouble when assigning a
string literal to it:

/home/haitao/pugi-store/pl_dlcall.dats: 894(line=31, offs=24) –
907(line=31, offs=37): error(3): [/home/hwxi/research/Postiats/
git/src/pats_trans3_util.dats]: d3exp_trdn: the dynamic
expression cannot be assigned the type [S2Eexi(n(231); ; S2Eapp(S2Ecst(stropt_int_type); S2Evar(n(231))))].
/home/haitao/pugi-store/pl_dlcall.dats: 894(line=31, offs=24) –
907(line=31, offs=37): error(3): mismatch of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(string_int_type); S2Eint(11))
The needed term is: S2Eapp(S2Ecst(stropt_int_type); S2EVar(3509))
/home/haitao/pugi-store/pl_dlcall.dats: 894(line=31, offs=24) –
907(line=31, offs=37): error(3): mismatch of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(string_int_type); S2Eint(11))
The needed term is: S2Eexi(n(231); ; S2Eapp(S2Ecst(stropt_int_type);
S2Evar(n(231))))

And line 31 is:
val library = dlopen(“testdll.dll”, RTLD_GLOBAL)

On Thursday, January 23, 2014 5:33:16 PM UTC-8, gmhwxi wrote:

string is a boxed type (that is, void*).

So $UN.cast{string}(0) essentially gives you the null pointer.

However,

length($UN.cast{string}(0)) segfaults.

Using stropt is a type-safe solution.

On Thursday, January 23, 2014 6:31:27 PM UTC-5, H Zhang wrote:

I used $UN.cast{string}(0) and that made the type checker happy.
Checking the gcc -E output shows that the translated C code is as expected.
It does read a little funny since it is not obvious at first sight that
string is actually a ptr, so one may wonder how 0 is converted to a string.

On Thursday, January 23, 2014 2:48:46 PM UTC-8, gmhwxi wrote:

When using these types, please get the ‘cast’ function ready
Proving stuff at this level may not be what you want to do
right now.

On Thursday, January 23, 2014 5:46:13 PM UTC-5, gmhwxi wrote:

Take a look at ‘stropt’ (functional) or ‘strptr’ (linear).

On Thursday, January 23, 2014 5:34:48 PM UTC-5, H Zhang wrote:

Some C library functions use zero valued pointer for special
meaning. What is the best way to model this? I would like to use string to
model char*, but then I can’t assign the value zero to a variable of type
string.

–
You received this message because you are subscribed to the Google
Groups “ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send
an email to ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/f8988334-3844-42ef-b61e-8bc2faf558ed%40googlegroups.com
.

[gmhwxi]

Semantically, stropt = string + NULLOn Thursday, January 23, 2014 11:31:16 PM UTC-5, H Zhang wrote:

Explict cast to stropt fixes the compile, but in terms of semantics if
something can be assigned to string then it should also be assigned to
stropt?

On Thursday, January 23, 2014 8:27:57 PM UTC-8, H Zhang wrote:

However if I use stropt I seem to get trouble when assigning a string
literal to it:

/home/haitao/pugi-store/pl_dlcall.dats: 894(line=31, offs=24) –
907(line=31, offs=37): error(3):
[/home/hwxi/research/Postiats/git/src/pats_trans3_util.dats]: d3exp_trdn:
the dynamic expression cannot be assigned the type [S2Eexi(n(231); ; S2Eapp(S2Ecst(stropt_int_type); S2Evar(n(231))))].
/home/haitao/pugi-store/pl_dlcall.dats: 894(line=31, offs=24) –
907(line=31, offs=37): error(3): mismatch of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(string_int_type); S2Eint(11))
The needed term is: S2Eapp(S2Ecst(stropt_int_type); S2EVar(3509))
/home/haitao/pugi-store/pl_dlcall.dats: 894(line=31, offs=24) –
907(line=31, offs=37): error(3): mismatch of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(string_int_type); S2Eint(11))
The needed term is: S2Eexi(n(231); ; S2Eapp(S2Ecst(stropt_int_type);
S2Evar(n(231))))

And line 31 is:
val library = dlopen(“testdll.dll”, RTLD_GLOBAL)

On Thursday, January 23, 2014 5:33:16 PM UTC-8, gmhwxi wrote:

string is a boxed type (that is, void*).

So $UN.cast{string}(0) essentially gives you the null pointer.

However,

length($UN.cast{string}(0)) segfaults.

Using stropt is a type-safe solution.

On Thursday, January 23, 2014 6:31:27 PM UTC-5, H Zhang wrote:

I used $UN.cast{string}(0) and that made the type checker happy.
Checking the gcc -E output shows that the translated C code is as expected.
It does read a little funny since it is not obvious at first sight that
string is actually a ptr, so one may wonder how 0 is converted to a string.

On Thursday, January 23, 2014 2:48:46 PM UTC-8, gmhwxi wrote:

When using these types, please get the ‘cast’ function ready
Proving stuff at this level may not be what you want to do right now.

On Thursday, January 23, 2014 5:46:13 PM UTC-5, gmhwxi wrote:

Take a look at ‘stropt’ (functional) or ‘strptr’ (linear).

On Thursday, January 23, 2014 5:34:48 PM UTC-5, H Zhang wrote:

Some C library functions use zero valued pointer for special
meaning. What is the best way to model this? I would like to use string to
model char*, but then I can’t assign the value zero to a variable of type
string.

[H_Zhang]

Explict cast to stropt fixes the compile, but in terms of semantics if
something can be assigned to string then it should also be assigned to
stropt?On Thursday, January 23, 2014 8:27:57 PM UTC-8, H Zhang wrote:

However if I use stropt I seem to get trouble when assigning a string
literal to it:

/home/haitao/pugi-store/pl_dlcall.dats: 894(line=31, offs=24) –
907(line=31, offs=37): error(3):
[/home/hwxi/research/Postiats/git/src/pats_trans3_util.dats]: d3exp_trdn:
the dynamic expression cannot be assigned the type [S2Eexi(n(231); ; S2Eapp(S2Ecst(stropt_int_type); S2Evar(n(231))))].
/home/haitao/pugi-store/pl_dlcall.dats: 894(line=31, offs=24) –
907(line=31, offs=37): error(3): mismatch of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(string_int_type); S2Eint(11))
The needed term is: S2Eapp(S2Ecst(stropt_int_type); S2EVar(3509))
/home/haitao/pugi-store/pl_dlcall.dats: 894(line=31, offs=24) –
907(line=31, offs=37): error(3): mismatch of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(string_int_type); S2Eint(11))
The needed term is: S2Eexi(n(231); ; S2Eapp(S2Ecst(stropt_int_type);
S2Evar(n(231))))

And line 31 is:
val library = dlopen(“testdll.dll”, RTLD_GLOBAL)

On Thursday, January 23, 2014 5:33:16 PM UTC-8, gmhwxi wrote:

string is a boxed type (that is, void*).

So $UN.cast{string}(0) essentially gives you the null pointer.

However,

length($UN.cast{string}(0)) segfaults.

Using stropt is a type-safe solution.

On Thursday, January 23, 2014 6:31:27 PM UTC-5, H Zhang wrote:

I used $UN.cast{string}(0) and that made the type checker happy.
Checking the gcc -E output shows that the translated C code is as expected.
It does read a little funny since it is not obvious at first sight that
string is actually a ptr, so one may wonder how 0 is converted to a string.

On Thursday, January 23, 2014 2:48:46 PM UTC-8, gmhwxi wrote:

When using these types, please get the ‘cast’ function ready
Proving stuff at this level may not be what you want to do right now.

On Thursday, January 23, 2014 5:46:13 PM UTC-5, gmhwxi wrote:

Take a look at ‘stropt’ (functional) or ‘strptr’ (linear).

On Thursday, January 23, 2014 5:34:48 PM UTC-5, H Zhang wrote:

Some C library functions use zero valued pointer for special meaning.
What is the best way to model this? I would like to use string to model
char*, but then I can’t assign the value zero to a variable of type string.