Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] String results in logical specifications

  • Subject: [Frama-c-discuss] String results in logical specifications
  • From: amdunn at gmail.com (Alan Dunn)
  • Date: Wed, 13 May 2009 07:33:22 -0400
I'm trying to write out an ACSL specification to some functions in
Linux-PAM (rewriting as necessary to ensure no use of function
pointers, which are unsupported at this time if I understand
correctly). I am in the beginning stages, but already encountering one
issue I would like to understand better: I would like to have logical
functions describing certain functionality within the program that I
can later build on or use elsewhere (although given the axiomatic
nature of the requirements, the specification will clearly not be
provable currently).

I would like something along the lines of:

/*@ axiomatic Passwords {
  @   predicate user_has_password(char *user);
  @   logic char *password_of(char *user);
  @   logic char *get_user(pam_handle_t *pamh);
  @   logic char *get_password(pam_handle_t *pamh);
  @   logic char *hash_of(char *input);
  @ }
  @*/

/*@ requires \valid(pamh);
  @ ensures \result == PAM_SUCCESS ==> (user_has_password(get_user(pamh)) &&
  @
strcmp(hash_of(password_of(get_user(pamh))),hash_of(get_password(pamh)))
== 0);
  @*/
PAM_EXTERN int pam_sm_authenticate(pam_handle_t * pamh, int flags
                                   ,int argc, const char **argv)
{
...
}

It seems that in the ACSL documentation there is no way to actually
create a logical function that returns something like a (char *) (only
a "type var" should be allowed, though I suppose a logical "string"
type would be equally acceptable). Indeed, running the previous
through frama-c produces:

[adunn at localhost pam_unix]$ frama-c -cpp-extra-args '-I../..
-I../../libpam/include' -jessie-analysis -jessie-behavior default
-jessie-gen-goals pam_unix_auth.c
Parsing
[preprocessing] running gcc -C -E -I. -include
/usr/share/frama-c/jessie/jessie_prolog.h -I../..
-I../../libpam/include -dD pam_unix_auth.c
/tmp/ppannot6da23b.c:352:1: warning: "NULL" redefined
/tmp/ppannot6da23b.c:117:1: warning: this is the location of the
previous definition
/tmp/ppannot4be1d7.c:352:1: warning: "NULL" redefined
/tmp/ppannot4be1d7.c:117:1: warning: this is the location of the
previous definition
pam_unix_auth.c:196: Warning: Body of function pam_sm_authenticate
falls-through. Adding a return statement

Cleaning unused parts
Symbolic link
Starting semantical analysis
Starting Jessie translation
No code for function dgettext, default assigns generated
No code for function malloc, default assigns generated
No code for function free, default assigns generated
No code for function pam_set_data, default assigns generated
No code for function pam_get_data, default assigns generated
No code for function pam_get_user, default assigns generated
No code for function _set_ctrl, default assigns generated
No code for function _unix_blankpasswd, default assigns generated
No code for function _unix_verify_password, default assigns generated
No code for function _unix_read_password, default assigns generated
Producing Jessie files in subdir pam_unix_auth.jessie
File pam_unix_auth.jessie/pam_unix_auth.jc written.
File pam_unix_auth.jessie/pam_unix_auth.cloc written.
Calling Jessie tool in subdir pam_unix_auth.jessie
Generating Why function setcred_free
Generating Why function pam_sm_authenticate
Generating Why function pam_sm_setcred
Calling VCs generator.
why --multi-why [...] why/pam_unix_auth.why
File "why/pam_unix_auth.why", line 6090, characters 25-50:
Unbound variable char_P_char_M_hash_of_141
make: *** [why/pam_unix_auth_ctx.why] Error 1
Jessie subprocess failed: make -f pam_unix_auth.makefile goals

which seems to be due to

let pam_sm_authenticate_ensures_default =
 fun (pamh_5_0 : char_xP pointer) (flags_0 : int32) (argc_0 : int32)
(argv_0 : char_const___xP pointer) (char_xP_pamh_5_83_alloc_table :
cha\
r_xP alloc_table) ->
  { ...}
...
  { (JC_2406:
    (eq_int(integer_of_int32(result), (0)) ->
     (user_has_password(get_user(pamh_5_0))
     and eq_int(strcmp(hash_of(password_of(get_user(pamh_5_0))),
                hash_of(get_password(pamh_5_0)), char_P_char_M_hash_of_141,
                char_P_char_M_hash_of_139),
         (0))))) }

wherein  char_P_char_M_hash_of_141 and ..._139 are not defined within
the postcondition (as they are in a let inside the main body instead).

Is there currently a good way of handling this? I can see either:
1) Defining a "string" axiomatic type
2) Folding all of my char * returning logical functions into
predicates on two (char *)'s eg:

logic char *hash_of(char *input)

becomes

predicate hash_of_input_is(char *input, char *hash)

that implies the desired result is in the two parameters when the
statement given from the predicate is true.

(I thought this might be good to report at minimum since would be good
to give an error message that (char *) is not an allowed type for a
logical function if this isn't supported, no?)

I hope this isn't answered somewhere else, and if my questions
indicate that there's something I'm missing/some resources that could
be helpful to me, please point them out.

Thanks,
- Alan