/*
 * Solaris X consolidation configuration for Parfait static analysis
 * This file provides additional information about functions that Parfait
 * can use to make more accurate analysis.
 */

/*
 * Copyright (c) 2012, 2015, Oracle and/or its affiliates. All rights reserved.
 *
 * Permission is hereby granted, free of charge, to any person obtaining a
 * copy of this software and associated documentation files (the "Software"),
 * to deal in the Software without restriction, including without limitation
 * the rights to use, copy, modify, merge, publish, distribute, sublicense,
 * and/or sell copies of the Software, and to permit persons to whom the
 * Software is furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice (including the next
 * paragraph) shall be included in all copies or substantial portions of the
 * Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL
 * THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 * DEALINGS IN THE SOFTWARE.
 */

include 'std.conf';

/* Define custom bug types for common precondition assertions */
bugtype "null-pointer-deref-call-X"(ptr) : "null-pointer-deref" {
   name="Null Pointer Dereference in X function";
   priority="error";
   enabled="true";
   message="Null pointer dereference in call to ", callee_name(), ". Pointer ", name(ptr), " may be dereferenced";
}
bugtype "unchecked-result-call-X"(val) : "unchecked-result" {
   name="Unchecked result";
   priority="error";
   enabled="true";
   message="Unchecked return value from call to ", callee_name(), ". Value " , name(val), " must be checked to ensure this function was successful.";
}
bugtype "pointer-size-mismatch-kernel"(ptr,size) {
   name="Pointer size mismatch in kernel function";
   priority="error";
   enabled="true";
   message="Incorrect pointer size in call to ", callee_name(), ". Pointer ", name(ptr), " given as size ", size;
}


/*************************************************************************
 * Client side functions
 */

/** libX11 **/
bugtype "X-resource-leak"(xid) {
    name="X Resource Leak";
    priority="error";
    enabled="true";
    message="Leaked X Resource ", name(xid);
}

resource <x-resource> {
    name="X Resource";
    "X-resource-leak"(resource): noleak(resource);
    resource == 0 => !isa(resource);
}

/* Listed pretty much in same order as <X11/Xlib.h> */

/* Todo: XLoadQueryFont...XNewModifiermap */

XCreateImage(const display, v, dp, f, o, data, w, h, bp, bpl) {
    "null-pointer-deref-call-X"(display) : display != 0;
    if (result != 0) {
        result == new(undefined);
        may_write(result);
        escape(data);
    }
}
XDestroyImage(p) { /* actually in <X11/Xutil.h> */
    "null-pointer-deref-call-X"(p) : p != 0;
    delete(p);
}
/* Todo: XInitImage, XGetImage, XGetSubImage */

XOpenDisplay(const d) : noescape {
    "unchecked-result-call-X"(result): is_checked(result);
    if (result != 0) {
        result == new(size(*result));
        may_write(result);
    }
}

XFetchBuffer(d, n, b) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    "null-pointer-deref-call-X"(n) : n != 0;
    if (result != 0) {
        *n == size(result);
        result == new(*n);
        may_write(result);
    }
}
XFetchBytes(d, n) : XFetchBuffer(d, n, 0);

XGetAtomName(d, a) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    if (result != 0) {
        result == new(undefined);
        may_write(result);
    }
}
/* Todo: XGetAtomNames, XGetDefault, XDisplayName, XKeysymToString,
   XInternAtom, XInternAtoms */

XCopyColormapAndFree(d, c) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    result != 0;
    init<x-resource>(result);
}
XCreateColormap(d, w, v, a) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    result != 0;
    init<x-resource>(result);
}
XCreatePixmapCursor(d, s, m, fg, bg, x, y) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    result != 0;
    init<x-resource>(result);
}
XCreateGlyphCursor(d, sf, mf, sc, mc, fg, bg) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    result != 0;
    init<x-resource>(result);
}
XCreateFontCursor(d, s) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    result != 0;
    init<x-resource>(result);
}
XLoadFont(d, const c) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    result != 0;
    init<x-resource>(result);
}

XCreateGC(d, dr, const vm, v) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    if (result != 0) {
        result == new(112); /* sizeof(struct _XGC) */
        may_write(result);
    } else {
        @errno != 0;
    }
}
/* Todo: XGContextFromGC, XFlushGC */

XCreatePixmap(d, dr, w, h, dp) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    result != 0;
    init<x-resource>(result);
}
XCreateBitmapFromData(d, dr, dt, w, h) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    if (result != 0) {
        init<x-resource>(result);
    } else {
        @errno != 0;
    }
}
XCreatePixmapFromBitmapData(d, dr, dt, w, h, fg, bg, dp) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    if (result != 0) {
        init<x-resource>(result);
    } else {
        @errno != 0;
    }
}
XCreateSimpleWindow(d,p,x,y,w,h,bw,b,bg) {
    "null-pointer-deref-call-X"(d) : d != 0;
    result != 0;
    init<x-resource>(result);
}
/* Todo: XGetSelectionOwner */
XCreateWindow(d,p,x,y,w,h,bw,dp,c,v,const vm,a) {
    "null-pointer-deref-call-X"(d) : d != 0;
    result != 0;
    init<x-resource>(result);
}
/* Todo: XListInstalledColormaps, XListFonts, XListFontsWithInfo, XGetFontPath */

XListExtensions(d, n) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    "null-pointer-deref-call-X"(n) : n != 0;
    if (result != 0) {
        result == new(undefined); /* n * char* + extension strings */
        may_write(n);
        may_write(result);
    }
}
XListProperties(d, w, n) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    if (result != 0) {
        result == new(n * 4);
        may_write(n);
        may_write(result);
    }
}
XListHosts(d, n, enabled) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    if (result != 0) {
        result == new(undefined); /* n * char* + host strings */
        may_write(n);
        may_write(enabled);
        may_write(result);
    }
}

XKeycodeToKeysym(d, k, i) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
}
XLookupKeysym(e, const i) : noescape {
    "null-pointer-deref-call-X"(e) : e != 0;
}
XGetKeyboardMapping(d, fk, kc, ks) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    "null-pointer-deref-call-X"(ks) : ks != 0;
    if (result != 0) {
        result == new(kc * ks);
        may_write(ks);
        may_write(result);
    }
}
XStringToKeysym(const s) : noescape {
    "null-pointer-deref-call-X"(s) : s != 0;
}
XMaxRequestSize(const d) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
}
XExtendedMaxRequestSize(const d) : XMaxRequestSize(d);
XScreenResourceString(const s) : noescape {
    "null-pointer-deref-call-X"(s) : s != 0;
}
XDisplayMotionBufferSize(const d) : XMaxRequestSize(d);
XVisualIdFromVisual(v) : noescape {
    /* Todo: visual resource id? */
    "null-pointer-deref-call-X"(v) : v != 0;
}

XLockDisplay(d) : XMaxRequestSize(d);
XUnlockDisplay(d) : XMaxRequestSize(d);

XAddExtension(d) {
    "null-pointer-deref-call-X"(d) : d != 0;
    if (result != 0) {
        result == new(size(*result));
        may_write(result);
        escape(result);
    }
}
XInitExtension(d, const n) : XAddExtension(d);
XFindOnExtensionList(s, n) {
    "null-pointer-deref-call-X"(s) : s != 0;
}

/* these are routines for which there are also macros */
XDefaultRootWindow(const d) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
}
XRootWindow(const d, const n) : XDefaultRootWindow(d);
XRootWindowOfScreen(const s) : XDefaultRootWindow(s);
XDefaultVisual(const d, const n) : XDefaultRootWindow(d);
XDefaultVisualOfScreen(const s) : XDefaultRootWindow(s);
XDefaultGC(const d, const n) : XDefaultRootWindow(d);
XDefaultGCOfScreen(const s) : XDefaultRootWindow(s);
XBlackPixel(const d, const n) : XDefaultRootWindow(d);
XWhitePixel(const d, const n) : XDefaultRootWindow(d);
XBlackPixelOfScreen(const s) : XDefaultRootWindow(s);
XWhitePixelOfScreen(const s) : XDefaultRootWindow(s);
XNextRequest(const d) : XDefaultRootWindow(d);
XLastKnownRequestProcessed(const d) : XDefaultRootWindow(d);
XServerVendor(const d) : XDefaultRootWindow(d);
XDisplayString(const d) : XDefaultRootWindow(d);

XDefaultColormap(const d, const n) : noescape {
    /* Todo: colormap resource id? */
    "null-pointer-deref-call-X"(d) : d != 0;
}
XDefaultColormapOfScreen(const s) : XDefaultColormap(s, 0);

XDisplayOfScreen(const s) : XDefaultRootWindow(s);
XScreenOfDisplay(const d, const n) : XDefaultRootWindow(d);
XDefaultScreenOfDisplay(const d) : XDefaultRootWindow(d);
XEventMaskOfScreen(const s) : XDefaultRootWindow(s);
XScreenNumberOfScreen(const s) : XDefaultRootWindow(s);

/* Todo: XSetErrorHandler, XSetIOErrorHandler */

XListPixmapFormats(d, c) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    "null-pointer-deref-call-X"(c) : c != 0;
    if (result != 0) {
        result == new(c * 12);  /* sizeof(XPixmapFormatValues) */
        may_write(c);
        may_write(result);
    } else {
        @errno != 0;
    }
}
XListDepths(d, s, c) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    "null-pointer-deref-call-X"(c) : c != 0;
    if (result != 0) {
        result == new(c * 4);  /* sizeof(int) */
        may_write(c);
        may_write(result);
    } else {
        @errno != 0;
    }
}
/* Todo: ICCCM routines - XReconfigureWMWindow...XSetWMColormapWindows,
   XSetTransientForHint */
XFreeStringList(l) : free(l);

XActivateScreenSaver(d) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
}
XAddHost(d, const h) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    "null-pointer-deref-call-X"(h) : h != 0;
}
XAddHosts(d, const h, const n) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    "null-pointer-deref-call-X"(h) : h != 0;
}
/* Todo: XAddToExtensionList...XClearWindow */
XCloseDisplay(d) {
    "null-pointer-deref-call-X"(d) : d != 0;
    delete(d);
}
/* Todo: XConfigureWindow...XDeleteProperty */
XDestroyWindow(d, w) {
    "null-pointer-deref-call-X"(d) : d != 0;
    destroy<x-resource>(w);
}
XDestroySubwindows(d, w) : XDestroyWindow(d, w); /* Todo: subwindows? */
/* Todo: XDoesBackingStore...XDisplayHeightMM */
XDisplayKeycodes(d, min, max) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    may_write(min);
    may_write(max);
    min >= 8;
    max <= 255;
}
/* Todo: XDisplayPlanes...XEventsQueued */
XFetchName(d, w, name) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    may_write(name);
    (result == 0) => (name == 0);
    if (name != 0) {
        name == new(undefined);
        may_write(result);
        result == 1;
    }
}
/* Todo: XFillArcs...XForceScreenSaver */
XFree(p) : free(p);
XFreeColormap(d, c) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    destroy<x-resource>(c);
}
/* Todo: XFreeColors */
XFreeCursor(d, c) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    destroy<x-resource>(c);
}
XFreeExtensionList(l) : free(l);
XFreeFont(d, f) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    destroy<x-resource>(f);
}
XFreeFontInfo(names, info, count) : noescape {
    /* Todo: free contents of names & info */
    (names != 0) => delete(names);
    (info != 0) => delete(info);
}
XFreeFontNames(l) : free(l);
XFreeFontPath(l) : free(l);
XFreeGC(d, gc) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    destroy<x-resource>(gc);
    delete(gc);
}
XFreeModifierMap(m) : free(m);
XFreePixmap(d, p) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    destroy<x-resource>(p);
}
/* Todo: XGeometry...XGetGeometry */
XGetIconName(d, w, name) : XFetchName(d, w, name);
/* Todo: XGetInputFocus...XGetTransientForHint */
XGetWindowProperty(d, w, p, lo, ll, del, rt, at, af, n, bar, prop) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    "unchecked-result-call-X"(result): is_checked(result);
    result == 0 => prop != 0;
    prop == 0 => result != 0;
    if (result == 0) {
        may_write(at);
        may_write(af);
        may_write(n);
        may_write(bar);
        may_write(prop);
    }
    if (prop != 0) {
        prop == new(undefined);
        may_write(prop);
        result == 0;
    }
}
/* Todo: XGetWindowAttributes...XQueryColors */
XQueryExtension(d, const n, op, ev, er) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    may_write(op);
    may_write(ev);
    may_write(er);
    if (result != 0) {
       op >= 128;
       op <= 255;
    }
}
/* Todo: XQueryKeymap...XQueryTextExtents16 */
XQueryTree(d, w, r, p, c, nc) : noescape {
    "null-pointer-deref-call-X"(d) : d != 0;
    "null-pointer-deref-call-X"(c) : c != 0;
    may_write(r);
    may_write(p);
    may_write(c);
    may_write(nc);
    if (result != 0) {
        c == new(nc * size(w));
    }
}
/* Todo: XRaiseWindow...XRemoveFromSaveSet */
XRemoveHost(d, const h) : XAddHost(d, h);
XRemoveHosts(d, const h, const n) : XAddHosts(d, h, n);
/* Todo: XReparentWindow...XFreeEventData */

/* Allocation functions from <X11/Xutil.h> */
XAllocClassHint() : calloc(1, size(*result));
XAllocIconSize() : calloc(1, size(*result));
XAllocSizeHints() : calloc(1, size(*result));
XAllocStandardColormap() : calloc(1, size(*result));
XAllocWMHints() : calloc(1, size(*result));

/** libXt
 * Functions from Xt's Alloc.c - like libc ones, except exit on failure,
 * instead of return NULL
 */
XtAsprintf(p,const fmt,args...) : printf(fmt,args), noescape {
    *p == new(result + 1);
    strlen(*p) == result;
    may_write(*p);
}

XtMalloc(s) {
    result == new(s);
}

XtRealloc(p,s) {
    delete(p);
    result == new(s);
    result[0..(size(PRE p) < s ? size(PRE p) : s)] == PRE p[0..(size(PRE p) < s ? size(PRE p) : s)];
}

XtCalloc(n,s) {
    result == new(n*s);
    result[0 .. (n * s)] == bytes(0, (n * s));
}

XtFree(p) : free(p);

/* libXcursor private function */
XcursorScanTheme(theme, name) : noescape {
   (theme == 0 || name == 0) => result == 0;
   (result != 0 && result != 1) => init<file-ptr>(result);
}

/*************************************************************************
 * Server side functions
 */

/* include/misc.h: byte swapping */
          /* XXX - does not work! */
bugtype "wrong-size-swap"(ptr,funcsize) {
    name="Wrong size Xserver swap function used";
    priority="error";
    enabled="true";
    message="Wrong size swap function used: ", callee_name(), " expects ", funcsize, "-byte variable, got ", size(ptr),"-byte ", name(ptr), " instead.";
}

swap_uint32(x) : noescape {
    "wrong-size-swap"(x,4): size(*x) == 4;
}
swap_uint16(x) : noescape {
    "wrong-size-swap"(x,2): size(*x) == 4;
}
SwapLongs(x,count) : noescape {
    "wrong-size-swap"(x,4): size(x) == 4;
}
SwapShorts(x,count) : noescape {
    "wrong-size-swap"(x,2): size(x) == 4;
}

/* dix/atom.c */
MakeAtom(string, len, makeit) : noescape {
    "null-pointer-deref-call-X"(string): string != 0;
    "buffer-overflow-call-stdc-str"(string): len <= strlen(string);
}

/* os/log.c: logging functions */
LogWrite(verb, const fmt, args...) : printf(fmt, args), noescape;
LogMessageVerb(type, verb, const fmt, args...) : printf(fmt, args), noescape;
LogMessage(type, const fmt, args...) : printf(fmt, args), noescape;
FatalError(const fmt, args...) : printf(fmt, args), noescape, exit;
ErrorF(const fmt, args...) : printf(fmt, args), noescape;
AbortServer(): exit;

/* os/utils.c: allocation & other helpers */
Xalloc(s) : malloc(s);
XNFalloc(s) {
    result == new(s);
}
Xcalloc(s) : calloc(1,s);
XNFcalloc(s) {
    result == new(s);
    result[0 .. s] == bytes(0, s);
}
Xrealloc(p, s) : realloc(p, s);
XNFrealloc(p, s) : realloc(p, s);
Xfree(p) : free(p);
Xstrdup(const s) : noescape {
    if ( s == 0 ) {
        result == 0;
    } else {
        if ( result != 0 ) {
            result == new(strlen(s)+1);
            strlen(result) == strlen(s);
            result[0..strlen(result)] == PRE s[0..strlen(s)];
        }
    }
}
XNFstrdup(const s) : noescape {
    if ( s == 0 ) {
        result == 0;
    } else {
        result == new(strlen(s)+1);
        strlen(result) == strlen(s);
    }
}
OsAbort() : abort();
Fopen(f, m) : fopen(f, m);
Fclose(p) : fclose(p);

/* os/xprintf.c: allocating printf wrappers/variants */
Xvasprintf(p, fmt, va) : vasprintf(p, fmt, va);
Xasprintf(p, fmt, args...) : asprintf(p, fmt, args);
XNFvasprintf(p, fmt, va) : noescape {
    *p == new(result);
    may_write(*p);
}
XNFasprintf(p, fmt, args...) : noescape, printf(fmt, args) {
    *p == new(result);
    may_write(*p);
}
Xvprintf(fmt, va) : noescape {
    if (result != 0) {
        result == new(undefined);
        may_write(result);
    }
}
Xprintf(fmt, args...) : noescape, printf(fmt, args) {
    if (result != 0) {
        result == new(undefined);
        may_write(result);
    }
}
XNFvprintf(fmt, va) : noescape {
    result == new(undefined);
    may_write(result);
}
XNFprintf(fmt, args...) : noescape, printf(fmt, args) {
    result == new(undefined);
    may_write(result);
}

/*************************************************************************
 * Kernel modules
 */

@if (file=="kernel/*") {

    include 'onnv.conf';

    /* graphics driver porting layer: open-src/kernel/drm/src/drm_memory.c */
    drm_alloc(s, a) : calloc(1, s);
    drm_calloc(n, s, a) : calloc(n, s);
    drm_realloc(pp, ps, s, a) : realloc(pp, s) {
        "pointer-size-mismatch-kernel"(pp,ps) : ps == size(pp);
    }
    drm_free(p, s, a) {  /* unlike kmem_free, accepts/ignores NULL pointers */
        "pointer-size-mismatch-kernel"(p,s) : s == size(p);
        delete(p);
    }
}
