/*
 *      Copyright (c) 2023, an unpublished work by CodeSecure, Inc.
 *                      ALL RIGHTS RESERVED
 *
 *      Copyright (c) 2014-2023, an unpublished work by GrammaTech, Inc.
 *                      ALL RIGHTS RESERVED
 *
 *      This software is furnished under a license and may be used and
 *      copied only in accordance with the terms of such license and the       
 *      inclusion of the above copyright notice.  This software or any
 *      other copies thereof may not be provided or otherwise made
 *      available to any other person.  Title to and ownership of the
 *      software is retained by CodeSecure, Inc.
 */

/* check_iolibrary.c
 *
 * Contains CodeSonar models and checks for the functions in iolibrary.h.
 */


#ifdef __CODESONAR__


/* All files that use the Extension API must include csonar.h and
 * stdlib.h. */
#include <stdlib.h>
#include <stdio.h>

#include "csonar.h"
#include "iolibrary.h"


/* We define a new \link C_Module/LibraryModels/TaintKinds.html taint
 * kind\endlink to track taint entering the program through functions
 * in this library. See documentation for \link
 * Extensions/Prototypes.html#CSONAR_DEFINE_TAINT_SOURCE
 * CSONAR_DEFINE_TAINT_SOURCE\endlink. */
CSONAR_DEFINE_TAINT_SOURCE(iolibrary);


#define __CSURF_MARKER_LIBRARY_FUNCTION__ 1

/* Some of the library functions are defined (in iolibrary.c) in terms
 * of libc functions that already have CodeSonar models.  The
 * following functions do not require additional modeling work because
 * all necessary checking and taint handling is already accomplished
 * by the libc models.
 *
 *  +-------------------------+------------+
 *  | iolibrary function      | libc model |
 *  +-------------------------+------------+
 *  | open_a_file()           | fopen()    |
 *  | close_a_file()          | fclose()   | 
 *  | write_string_to_file()  | fputs()    |
 *  +-------------------------+------------+
 */ 


/* The specially-named \link Extensions/Prototypes.html#csonar_replace
 * csonar_replace_open_a_file()\endlink will intercept 
 * all calls to open_a_file (and similarly for all other
 * procedures with names of the form csonar_replace_functionname).
 *
 * Note that the symbol \link
 * Extensions/Prototypes.html#csurf_marker_library_function
 * __CSURF_MARKER_LIBRARY_FUNCTION__ \endlink is defined
 * (as 1) before the definitions of the csonar_replace_*
 * functions. This marks them as LIBRARY FUNCTIONS: any warnings
 * triggered inside a replacement function will be reported at the
 * appropriate call site to that function, not inside the function
 * itself.
 *
 * Our replacement for read_string_from_file() calls the actual
 * read_string_from_file() function so that its implementation can be
 * checked by CodeSonar.  Additionally, it specifies that the string
 * read from the file has all of the taint determined by analyzing 
 * read_string_from_file(), plus taint of kind 'iolibrary'. 
 */
char * csonar_replace_read_string_from_file(char *dest, 
    size_t numchars,
    FILE *src){
   char * retval;
   size_t len;
   int taintunion;
   retval = read_string_from_file(dest, numchars, src);
   if (retval && CSM_UNKNOWN_INTEGER()){
     /* We want this code to be visible to the taint analysis phase
      * only. If it were analyzed during other phases it could cause
      * CodeSonar to become confused about the size of the buffer.
      */
     csonar_assert_taint_enabled();
     
     /* Construct a value with "iolibrary" taint plus all the taint
      * previously associated with dest. */
     taintunion = csonar_taint_union2(csonar_string_taint(dest), 
      csonar_taint_source_iolibrary());

     /* Model taint on the contents of the string. */
     *dest = taintunion;

     /* Model taint on the length of the string.*/
     len = csonar_bounded_value(taintunion, 
                                0, 
                                numchars - 1 );
     dest[len] = '\0';
   }
   return retval;
}


/* We model sanitized_size() to call the actual sanitized_size()
 * function so that its implementation can be checked by
 * CodeSonar. The model uses analysis 'assertions' to inform the
 * CodeSonar analysis that the return must be either -1, or at least
 * as large as the length of 'raw'.
 * The model cleanses all taint from the return value before returning
 * it: the sanitized size is derived from the size of the 'raw'
 * string, but we have determined it to be safe.
 */
int csonar_replace_sanitized_size(char *raw){
  int retval;
  retval = sanitized_size(raw);
  if (retval < strlen(raw)){
    if (retval != -1){ abort(); }
  }
  csonar_taint_clear_int(&retval);

  return retval;
}

   
/* We model sanitize_file_string() to call the actual
 * sanitize_file_string() function so that its implementation can be
 * checked by CodeSonar. Additionally, the model uses \link
 * Extensions/Prototypes.html#csonar_taint_clear
 * csonar_taint_clear_*\endlink to specify that the resulting string
 * has no taint.
 * - The "int" attribute of an address is an alias for the memory contents
 *   at that address.
 * - The "term" attribute of an address is an alias for the distance 
 *   (in bits) between that address and the null sentinel.
 */
int csonar_replace_sanitize_file_string(char *raw, char *sanitized){
  int retval;
  retval = sanitize_file_string(raw, sanitized);
  csonar_taint_clear_int(sanitized);
  csonar_taint_clear_term(sanitized);
  return retval;
}


/* If a tainted string is passed to print_important_data(), we want to
 * issue a warning. csonar_taint_sink() performs the taint check and
 * specifies the warning class to use. In this case, we specify a
 * custom warning class.
 */
int csonar_replace_print_important_data(char *str){
  csonar_taint_sink(csonar_taint_source_any(),
                    *str, 
                    "Tainted Input to print_important_data", 
                    "CWE:20",
                    csws_security);
  return print_important_data(str);
}

#endif