How to model C char* that can be 0?

[H Zhang]

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]

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

[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.

[Brandon Barker]

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, int numvars,
              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);

[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.com

--
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.

[Brandon Barker]

Also, I pasted the wrong function call.. should be:

 error = GRBnewmodel(env, &model, "mip1", 0, NULL, NULL, NULL, NULL, NULL);

Brandon Barker
brandon...@gmail.com

[H Zhang]

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.

[gmhwxi]

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.

[gmhwxi]

This is where ATS can shine.

As we can see, there are so many ambiguities here. For instance.

obj: &double >> _

or

obj: &double? >> _

When calling the function, should obj be initialized or not?

[Brandon Barker]

Presumably (I only have the header and the example), it is going to be either an initialized pointer to doubles ( obj: &double >> _ ), or a NULL pointer. 

I imagine passing a NULL pointer could have strange behavior, but on testing it (passing an unitialized double* in C), it compiled and ran fine (but I guess we can exclude the possibility as it is a bit odd here).

So I wonder if it is advisable to attempt to model a datavtype that is either a  "&double >> _" or a  NULL, or if there's a more straightforward approach.

[gmhwxi]

It is doable (I did it), but it makes things too complicated for the user.

You can use something like:

obj: cPtr0(double)

In general, this is good enough.

[H Zhang]

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)

[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?

[gmhwxi]

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

[gmhwxi]

Semantically, stropt = string + NULL

[H Zhang]

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?

[gmhwxi]

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

[Brandon Barker]

I was about to suggest it might be in string.sats:

symintr stropt_some

castfn stropt0_some (x: SHR(string)): Stropt1

overload stropt_some with stropt0_some of 0

castfn stropt1_some {n:int} (x: SHR(string n)): stropt (n)

overload stropt_some with stropt1_some of 10

I find I have to dig around in a few files sometimes to find what I want.

For instance, just a few minutes ago, I found ptr2cptr in unsafe.sats, and cptr2ptr in pointer.sats (or vice versa).

Brandon Barker
brandon...@gmail.com

--

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/8c5a8198-646f-4767-938e-b03afe345b80%40googlegroups.com.

[gmhwxi]

ptr2cptr is unsafe but cptr2ptr is safe :)

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

[H Zhang]

Thanks. I saw that but I wasn't sure how it could be loaded as I don't explicitly staload string.sats. Then I remembered from digging around the pats src:

....
val () = pervasive_load (PATSHOME, "prelude/SATS/float.sats")
val () = pervasive_load (PATSHOME, "prelude/SATS/memory.sats")
val () = pervasive_load (PATSHOME, "prelude/SATS/string.sats")
val () = pervasive_load (PATSHOME, "prelude/SATS/strptr.sats")
val () = pervasive_load (PATSHOME, "prelude/SATS/tuple.sats")
....

So patsopt automatically load these by default.

[Brandon Barker]

I guess that makes sense: we are not assuming assuming a viewtype in this cast: 

cptr2ptr {a:vt0p}{l:addr} (p: cptr (a, l)):<> ptr (l)

Brandon Barker
brandon...@gmail.com

--

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/748c7b9e-569f-4e74-a31c-42ac7bcd0f37%40googlegroups.com.

[H Zhang]

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

[gmhwxi]

But what does that buy you?

[Brandon Barker]

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
brandon...@gmail.com

--

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/f8988334-3844-42ef-b61e-8bc2faf558ed%40googlegroups.com.

[gmhwxi]

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.

[gmhwxi]

I had the bug this morning (: